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
starLinearEquivfor noncommutativeR. 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 typeR →+* Rᵐᵒᵖ, which is very undesirable in the commutative case. One way out would be to define a new typeclassIsOp R Sand have an instanceIsOp R Rfor commutativeR. - Also note that such a definition involving
Rᵐᵒᵖoris_op R Swould require adding the appropriateRingHomInvPairinstances to be able to define the semilinear equivalence.
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[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)
:
@[simp]
theorem
star_rat_smul
{R : Type u_3}
[AddCommGroup R]
[StarAddMonoid R]
[Module ℚ R]
(x : R)
(n : ℚ)
:
@[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 = starAddEquiv.toEquiv.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
starLinearEquiv
(R : Type u_1)
{A : Type u_2}
[CommSemiring R]
[StarRing R]
[AddCommMonoid A]
[StarAddMonoid A]
[Module R A]
[StarModule 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
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
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
@[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)
:
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
- One or more equations did not get rendered due to their size.
Instances For
@[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)
:
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
- One or more equations did not get rendered due to their size.
Instances For
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 = { val := x, property := hx }
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 ∘ₗ Submodule.subtype (selfAdjoint.submodule R A) = 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
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 ∘ₗ Submodule.subtype (selfAdjoint.submodule R A) = 0
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 ∘ₗ Submodule.subtype (skewAdjoint.submodule R A) = 0
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 ∘ₗ Submodule.subtype (skewAdjoint.submodule R A) = LinearMap.id
@[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)
@[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))
:
(LinearEquiv.symm (StarModule.decomposeProdAdjoint R A)) a = (Submodule.subtype (selfAdjoint.submodule R A)) a.1 + (Submodule.subtype (skewAdjoint.submodule R A)) a.2
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
- One or more equations did not get rendered due to their size.
Instances For
@[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