The star operation, bundled as a star-linear equiv #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define star_linear_equiv, 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
star_linear_equivfor 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 typeclassis_op R Sand have an instanceis_op R Rfor commutativeR. - Also note that such a definition involving
Rᵐᵒᵖoris_op R Swould require adding the appropriatering_hom_inv_pairinstances to be able to define the semilinear equivalence.
@[simp]
theorem
star_nat_cast_smul
{R : Type u_1}
{M : Type u_2}
[semiring R]
[add_comm_monoid M]
[module R M]
[star_add_monoid M]
(n : ℕ)
(x : M) :
has_star.star (↑n • x) = ↑n • has_star.star x
@[simp]
theorem
star_int_cast_smul
{R : Type u_1}
{M : Type u_2}
[ring R]
[add_comm_group M]
[module R M]
[star_add_monoid M]
(n : ℤ)
(x : M) :
has_star.star (↑n • x) = ↑n • has_star.star x
@[simp]
theorem
star_inv_nat_cast_smul
{R : Type u_1}
{M : Type u_2}
[division_semiring R]
[add_comm_monoid M]
[module R M]
[star_add_monoid M]
(n : ℕ)
(x : M) :
has_star.star ((↑n)⁻¹ • x) = (↑n)⁻¹ • has_star.star x
@[simp]
theorem
star_inv_int_cast_smul
{R : Type u_1}
{M : Type u_2}
[division_ring R]
[add_comm_group M]
[module R M]
[star_add_monoid M]
(n : ℤ)
(x : M) :
has_star.star ((↑n)⁻¹ • x) = (↑n)⁻¹ • has_star.star x
@[simp]
theorem
star_rat_cast_smul
{R : Type u_1}
{M : Type u_2}
[division_ring R]
[add_comm_group M]
[module R M]
[star_add_monoid M]
(n : ℚ)
(x : M) :
has_star.star (↑n • x) = ↑n • has_star.star x
@[simp]
theorem
star_rat_smul
{R : Type u_1}
[add_comm_group R]
[star_add_monoid R]
[module ℚ R]
(x : R)
(n : ℚ) :
has_star.star (n • x) = n • has_star.star x
@[simp]
theorem
star_linear_equiv_symm_apply
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[add_comm_monoid A]
[star_add_monoid A]
[module R A]
[star_module R A]
(ᾰ : A) :
⇑((star_linear_equiv R).symm) ᾰ = star_add_equiv.inv_fun ᾰ
@[simp]
theorem
star_linear_equiv_apply
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[add_comm_monoid A]
[star_add_monoid A]
[module R A]
[star_module R A]
(ᾰ : A) :
⇑(star_linear_equiv R) ᾰ = has_star.star ᾰ
def
star_linear_equiv
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[add_comm_monoid A]
[star_add_monoid A]
[module R A]
[star_module R A] :
If A is a module over a commutative R with compatible actions,
then star is a semilinear equivalence.
Equations
- star_linear_equiv R = {to_fun := has_star.star has_involutive_star.to_has_star, map_add' := _, map_smul' := _, inv_fun := star_add_equiv.inv_fun, left_inv := _, right_inv := _}
def
self_adjoint.submodule
(R : Type u_1)
(A : Type u_2)
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A] :
submodule R A
The self-adjoint elements of a star module, as a submodule.
Equations
- self_adjoint.submodule R A = {carrier := (self_adjoint A).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}
def
skew_adjoint.submodule
(R : Type u_1)
(A : Type u_2)
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A] :
submodule R A
The skew-adjoint elements of a star module, as a submodule.
Equations
- skew_adjoint.submodule R A = {carrier := (skew_adjoint A).carrier, add_mem' := _, zero_mem' := _, smul_mem' := _}
def
self_adjoint_part
(R : Type u_1)
{A : Type u_2}
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2] :
A →ₗ[R] ↥(self_adjoint A)
The self-adjoint part of an element of a star module, as a linear map.
@[simp]
theorem
self_adjoint_part_apply_coe
(R : Type u_1)
{A : Type u_2}
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2]
(x : A) :
↑(⇑(self_adjoint_part R) x) = ⅟ 2 • (x + has_star.star x)
def
skew_adjoint_part
(R : Type u_1)
{A : Type u_2}
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2] :
A →ₗ[R] ↥(skew_adjoint A)
The skew-adjoint part of an element of a star module, as a linear map.
@[simp]
theorem
skew_adjoint_part_apply_coe
(R : Type u_1)
{A : Type u_2}
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2]
(x : A) :
↑(⇑(skew_adjoint_part R) x) = ⅟ 2 • (x - has_star.star x)
theorem
star_module.self_adjoint_part_add_skew_adjoint_part
(R : Type u_1)
{A : Type u_2}
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2]
(x : A) :
↑(⇑(self_adjoint_part R) x) + ↑(⇑(skew_adjoint_part R) x) = x
def
star_module.decompose_prod_adjoint
(R : Type u_1)
(A : Type u_2)
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2] :
A ≃ₗ[R] ↥(self_adjoint A) × ↥(skew_adjoint A)
The decomposition of elements of a star module into their self- and skew-adjoint parts, as a linear equivalence.
Equations
- star_module.decompose_prod_adjoint R A = linear_equiv.of_linear ((self_adjoint_part R).prod (skew_adjoint_part R)) ((self_adjoint.submodule R A).subtype.coprod (skew_adjoint.submodule R A).subtype) _ _
@[simp]
theorem
star_module.decompose_prod_adjoint_apply
(R : Type u_1)
(A : Type u_2)
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2]
(ᾰ : A) :
⇑(star_module.decompose_prod_adjoint R A) ᾰ = (⇑(self_adjoint_part R) ᾰ, ⇑(skew_adjoint_part R) ᾰ)
@[simp]
theorem
star_module.decompose_prod_adjoint_symm_apply
(R : Type u_1)
(A : Type u_2)
[semiring R]
[star_semigroup R]
[has_trivial_star R]
[add_comm_group A]
[module R A]
[star_add_monoid A]
[star_module R A]
[invertible 2]
(ᾰ : ↥(self_adjoint A) × ↥(skew_adjoint A)) :
@[simp]
theorem
algebra_map_star_comm
{R : Type u_1}
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[semiring A]
[star_semigroup A]
[algebra R A]
[star_module R A]
(r : R) :
⇑(algebra_map R A) (has_star.star r) = has_star.star (⇑(algebra_map R A) r)