The star operation, bundled as a continuous star-linear equiv

def «term_→L⋆[_]_» : Lean.TrailingParserDescr

Continuous linear maps between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological ring R.

Equations

• One or more equations did not get rendered due to their size.

def «term_≃L⋆[_]_» : Lean.TrailingParserDescr

Continuous linear equivalences between modules. We only put the type classes that are necessary for the definition, although in applications M and M₂ will be topological modules over the topological semiring R.

Equations

• One or more equations did not get rendered due to their size.

def starL (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] : A ≃L⋆[R] A

If A is a topological module over a commutative R with compatible actions, then star is a continuous semilinear equivalence.

Equations

• starL R = { toLinearEquiv := starLinearEquiv R, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem starL_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] : ∀ (a : A), (starL R).symm a = starAddEquiv.symm a

@[simp]

theorem starL_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] : ∀ (a : A), (starL R) a = star a

def starL' (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] : A ≃L[R] A

If A is a topological module over a commutative R with trivial star and compatible actions, then star is a continuous linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem starL'_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] : ∀ (a : A), (starL' R).symm a = (starL R).symm ({ toFun := id, map_add' := ⋯, map_smul' := ⋯, invFun := id, left_inv := ⋯, right_inv := ⋯ }.symm a)

@[simp]

theorem starL'_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [TrivialStar R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] [TopologicalSpace A] [ContinuousStar A] : ∀ (a : A), (starL' R) a = star a

theorem continuous_selfAdjointPart (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] : Continuous ⇑(selfAdjointPart R)

theorem continuous_skewAdjointPart (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] : Continuous ⇑(skewAdjointPart R)

theorem continuous_decomposeProdAdjoint (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] : Continuous ⇑(StarModule.decomposeProdAdjoint R A)

theorem continuous_decomposeProdAdjoint_symm (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] : Continuous ⇑(StarModule.decomposeProdAdjoint R A).symm

def selfAdjointPartL (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] : A →L[R] ↥(selfAdjoint A)

The self-adjoint part of an element of a star module, as a continuous linear map.

Equations

• selfAdjointPartL R A = { toLinearMap := selfAdjointPart R, cont := ⋯ }

@[simp]

theorem selfAdjointPartL_apply_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) : ↑((selfAdjointPartL R A) x) = ⅟2 • x + ⅟2 • star x

@[simp]

theorem selfAdjointPartL_toFun_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousAdd A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) : ↑((selfAdjointPartL R A) x) = ⅟2 • x + ⅟2 • star x

def skewAdjointPartL (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] : A →L[R] ↥(skewAdjoint A)

The skew-adjoint part of an element of a star module, as a continuous linear map.

Equations

• skewAdjointPartL R A = { toLinearMap := skewAdjointPart R, cont := ⋯ }

@[simp]

theorem skewAdjointPartL_toFun_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) : ↑((skewAdjointPartL R A) x) = ⅟2 • (x - star x)

@[simp]

theorem skewAdjointPartL_apply_coe (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [ContinuousSub A] [ContinuousStar A] [ContinuousConstSMul R A] (x : A) : ↑((skewAdjointPartL R A) x) = ⅟2 • (x - star x)

def StarModule.decomposeProdAdjointL (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] : A ≃L[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)

The decomposition of elements of a star module into their self- and skew-adjoint parts, as a continuous linear equivalence.

Equations

• StarModule.decomposeProdAdjointL R A = { toLinearEquiv := StarModule.decomposeProdAdjoint R A, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem StarModule.decomposeProdAdjointL_apply (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] (i : A) : (StarModule.decomposeProdAdjointL R A) i = ((selfAdjointPart R) i, (skewAdjointPart R) i)

@[simp]

theorem StarModule.decomposeProdAdjointL_symm_apply (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] [Invertible 2] [TopologicalSpace A] [TopologicalAddGroup A] [ContinuousStar A] [ContinuousConstSMul R A] (a : ↥(selfAdjoint A) × ↥(skewAdjoint A)) : (StarModule.decomposeProdAdjointL R A).symm a = (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2