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

We define starLinearEquiv, which is the star operation bundled as a star-linear map. It is defined on a star algebra A over the base ring R.

This file also provides some lemmas that need Algebra.Module.Basic imported to prove.

TODO #

Define starLinearEquiv for noncommutative R. We only the commutative case for now since, in the noncommutative case, the ring hom needs to reverse the order of multiplication. This requires a ring hom of type R →+* Rᵐᵒᵖ, which is very undesirable in the commutative case. One way out would be to define a new typeclass IsOp R S and have an instance IsOp R R for commutative R.
Also note that such a definition involving Rᵐᵒᵖ or is_op R S would require adding the appropriate RingHomInvPair instances to be able to define the semilinear equivalence.

source

@[simp]

theorem star_nat_cast_smul {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [StarAddMonoid M] (n : ℕ) (x : M) :

star (↑n • x) = ↑n • star x

source

@[simp]

theorem star_int_cast_smul {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ℤ) (x : M) :

star (↑n • x) = ↑n • star x

source

@[simp]

theorem star_inv_nat_cast_smul {R : Type u_1} {M : Type u_2} [DivisionSemiring R] [AddCommMonoid M] [Module R M] [StarAddMonoid M] (n : ℕ) (x : M) :

star ((↑n)⁻¹ • x) = (↑n)⁻¹ • star x

source

@[simp]

theorem star_inv_int_cast_smul {R : Type u_1} {M : Type u_2} [DivisionRing R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ℤ) (x : M) :

star ((↑n)⁻¹ • x) = (↑n)⁻¹ • star x

source

@[simp]

theorem star_rat_cast_smul {R : Type u_1} {M : Type u_2} [DivisionRing R] [AddCommGroup M] [Module R M] [StarAddMonoid M] (n : ℚ) (x : M) :

star (↑n • x) = ↑n • star x

source

@[simp]

theorem star_rat_smul {R : Type u_3} [AddCommGroup R] [StarAddMonoid R] [Module ℚ R] (x : R) (n : ℚ) :

star (n • x) = n • star x

source

@[simp]

theorem starLinearEquiv_symm_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] :

∀ (a : A), ↑(LinearEquiv.symm (starLinearEquiv R)) a = Equiv.invFun starAddEquiv.toEquiv a

source

@[simp]

theorem starLinearEquiv_apply (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] :

∀ (a : A), ↑(starLinearEquiv R) a = star a

source

def starLinearEquiv (R : Type u_1) {A : Type u_2} [CommSemiring R] [StarRing R] [AddCommMonoid A] [StarAddMonoid A] [Module R A] [StarModule R A] :

A ≃ₗ⋆[R] A

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

Equations

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

Instances For

source

def selfAdjoint.submodule (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] :

Submodule R A

The self-adjoint elements of a star module, as a submodule.

Equations

selfAdjoint.submodule R A = let src := selfAdjoint A; { toAddSubmonoid := src.toAddSubmonoid, smul_mem' := (_ : ∀ (x : R) (x_1 : A), IsSelfAdjoint x_1 → IsSelfAdjoint (x • x_1)) }

Instances For

source

def skewAdjoint.submodule (R : Type u_1) (A : Type u_2) [Semiring R] [StarMul R] [TrivialStar R] [AddCommGroup A] [Module R A] [StarAddMonoid A] [StarModule R A] :

Submodule R A

The skew-adjoint elements of a star module, as a submodule.

Equations

skewAdjoint.submodule R A = let src := skewAdjoint A; { toAddSubmonoid := src.toAddSubmonoid, smul_mem' := (_ : ∀ (r : R) {x : A}, x ∈ skewAdjoint A → r • x ∈ skewAdjoint A) }

Instances For

source

@[simp]

theorem selfAdjointPart_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] (x : A) :

↑(↑(selfAdjointPart R) x) = ⅟2 • (x + star x)

source

def 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] :

A →ₗ[R] { x // x ∈ selfAdjoint A }

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

Equations

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

Instances For

source

@[simp]

theorem skewAdjointPart_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] (x : A) :

↑(↑(skewAdjointPart R) x) = ⅟2 • (x - star x)

source

def 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] :

A →ₗ[R] { x // x ∈ skewAdjoint A }

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

Equations

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

Instances For

source

theorem StarModule.selfAdjointPart_add_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] (x : A) :

↑(↑(selfAdjointPart R) x) + ↑(↑(skewAdjointPart R) x) = x

source

theorem IsSelfAdjoint.coe_selfAdjointPart_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] {x : A} (hx : IsSelfAdjoint x) :

↑(↑(selfAdjointPart R) x) = x

source

theorem IsSelfAdjoint.selfAdjointPart_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] {x : A} (hx : IsSelfAdjoint x) :

↑(selfAdjointPart R) x = { val := x, property := hx }

source

theorem selfAdjointPart_comp_subtype_selfAdjoint (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] :

LinearMap.comp (selfAdjointPart R) (Submodule.subtype (selfAdjoint.submodule R A)) = LinearMap.id

source

theorem IsSelfAdjoint.skewAdjointPart_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] {x : A} (hx : IsSelfAdjoint x) :

↑(skewAdjointPart R) x = 0

source

theorem skewAdjointPart_comp_subtype_selfAdjoint (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] :

LinearMap.comp (skewAdjointPart R) (Submodule.subtype (selfAdjoint.submodule R A)) = 0

source

theorem selfAdjointPart_comp_subtype_skewAdjoint (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] :

LinearMap.comp (selfAdjointPart R) (Submodule.subtype (skewAdjoint.submodule R A)) = 0

source

theorem skewAdjointPart_comp_subtype_skewAdjoint (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] :

LinearMap.comp (skewAdjointPart R) (Submodule.subtype (skewAdjoint.submodule R A)) = LinearMap.id

source

@[simp]

theorem StarModule.decomposeProdAdjoint_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] (a : { x // x ∈ selfAdjoint A } × { x // x ∈ skewAdjoint A }) :

↑(LinearEquiv.symm (StarModule.decomposeProdAdjoint R A)) a = ↑(Submodule.subtype (selfAdjoint.submodule R A)) a.fst + ↑(Submodule.subtype (skewAdjoint.submodule R A)) a.snd

source

@[simp]

theorem StarModule.decomposeProdAdjoint_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] (i : A) :

↑(StarModule.decomposeProdAdjoint R A) i = (↑(selfAdjointPart R) i, ↑(skewAdjointPart R) i)

source

def StarModule.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] :

A ≃ₗ[R] { x // x ∈ selfAdjoint A } × { x // x ∈ skewAdjoint A }

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

Equations

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

Instances For

source

@[simp]

theorem algebraMap_star_comm {R : Type u_3} {A : Type u_4} [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] (r : R) :

↑(algebraMap R A) (star r) = star (↑(algebraMap R A) r)