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.

@[simp]

theorem star_natCast_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

@[simp]

theorem star_intCast_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

@[simp]

theorem star_inv_natCast_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

@[simp]

theorem star_inv_intCast_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

@[simp]

theorem star_ratCast_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

Per the naming convention, these two lemmas call (q • ·) nnrat_smul and rat_smul respectively, rather than nnqsmul and qsmul because the latter are reserved to the actions coming from DivisionSemiring and DivisionRing. We provide aliases with nnqsmul and qsmul for discoverability.

@[simp]

theorem star_nnrat_smul {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] [Module ℚ≥0 R] (q : ℚ≥0) (x : R) : star (q • x) = q • star x

Note that this lemma holds for an arbitrary ℚ≥0-action, rather than merely one coming from a DivisionSemiring. We keep both the nnqsmul and nnrat_smul naming conventions for discoverability. See star_nnqsmul.

@[simp]

theorem star_rat_smul {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] [Module ℚ R] (q : ℚ) (x : R) : star (q • x) = q • star x

Note that this lemma holds for an arbitrary ℚ-action, rather than merely one coming from a DivisionRing. We keep both the qsmul and rat_smul naming conventions for discoverability. See star_qsmul.

theorem star_nnqsmul {R : Type u_1} [AddCommMonoid R] [StarAddMonoid R] [Module ℚ≥0 R] (q : ℚ≥0) (x : R) : star (q • x) = q • star x

Note that this lemma holds for an arbitrary ℚ≥0-action, rather than merely one coming from a DivisionSemiring. We keep both the nnqsmul and nnrat_smul naming conventions for discoverability. See star_nnrat_smul.

theorem star_qsmul {R : Type u_1} [AddCommGroup R] [StarAddMonoid R] [Module ℚ R] (q : ℚ) (x : R) : star (q • x) = q • star x

Note that this lemma holds for an arbitrary ℚ-action, rather than merely one coming from a DivisionRing. We keep both the qsmul and rat_smul naming conventions for discoverability. See star_rat_smul.

instance StarAddMonoid.toStarModuleNNRat {R : Type u_1} [AddCommMonoid R] [Module ℚ≥0 R] [StarAddMonoid R] : StarModule ℚ≥0 R

instance StarAddMonoid.toStarModuleRat {R : Type u_1} [AddCommGroup R] [Module ℚ R] [StarAddMonoid R] : StarModule ℚ R

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

• starLinearEquiv R = { toFun := star, map_add' := ⋯, map_smul' := ⋯, invFun := starAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯ }

@[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) : (starLinearEquiv R).symm a✝ = starAddEquiv.invFun a✝

@[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✝

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 = { toAddSubmonoid := (selfAdjoint A).toAddSubmonoid, smul_mem' := ⋯ }

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 = { toAddSubmonoid := (skewAdjoint A).toAddSubmonoid, smul_mem' := ⋯ }

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] ↥(selfAdjoint A)

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

Equations

• selfAdjointPart R = { toFun := fun (x : A) => ⟨⅟2 • (x + star x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[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)

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] ↥(skewAdjoint A)

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

Equations

• skewAdjointPart R = { toFun := fun (x : A) => ⟨⅟2 • (x - star x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[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)

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

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

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 = ⟨x, hx⟩

@[simp]

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] : selfAdjointPart R ∘ₗ (selfAdjoint.submodule R A).subtype = LinearMap.id

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

@[simp]

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] : skewAdjointPart R ∘ₗ (selfAdjoint.submodule R A).subtype = 0

@[simp]

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] : selfAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype = 0

@[simp]

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] : skewAdjointPart R ∘ₗ (skewAdjoint.submodule R A).subtype = LinearMap.id

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] ↥(selfAdjoint A) × ↥(skewAdjoint A)

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

Equations

• StarModule.decomposeProdAdjoint R A = LinearEquiv.ofLinear ((selfAdjointPart R).prod (skewAdjointPart R)) ((selfAdjoint.submodule R A).subtype.coprod (skewAdjoint.submodule R A).subtype) ⋯ ⋯

@[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 : ↥(selfAdjoint A) × ↥(skewAdjoint A)) : (decomposeProdAdjoint R A).symm a = (selfAdjoint.submodule R A).subtype a.1 + (skewAdjoint.submodule R A).subtype a.2

@[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) : (decomposeProdAdjoint R A) i = ((selfAdjointPart R) i, (skewAdjointPart R) i)

@[simp]

theorem algebraMap_star_comm {R : Type u_1} {A : Type u_2} [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)

theorem IsSelfAdjoint.algebraMap {R : Type u_1} (A : Type u_2) [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] {r : R} (hr : IsSelfAdjoint r) : IsSelfAdjoint ((algebraMap R A) r)

theorem isSelfAdjoint_algebraMap_iff {R : Type u_1} {A : Type u_2} [CommSemiring R] [StarRing R] [Semiring A] [StarMul A] [Algebra R A] [StarModule R A] {r : R} (h : Function.Injective ⇑(algebraMap R A)) : IsSelfAdjoint ((algebraMap R A) r) ↔ IsSelfAdjoint r

theorem IsIdempotentElem.star_iff {R : Type u_1} [Mul R] [StarMul R] {a : R} : IsIdempotentElem (Star.star a) ↔ IsIdempotentElem a

theorem IsIdempotentElem.star {R : Type u_1} [Mul R] [StarMul R] {a : R} : IsIdempotentElem a → IsIdempotentElem (Star.star a)

Alias of the reverse direction of IsIdempotentElem.star_iff.