The star operation, bundled as a continuous star-linear equiv #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
@[simp]
theorem
starL_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]
[topological_space A]
[has_continuous_star A]
(ᾰ : A) :
⇑(starL R) ᾰ = has_star.star ᾰ
@[simp]
theorem
starL_to_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]
[topological_space A]
[has_continuous_star A] :
def
starL
(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]
[topological_space A]
[has_continuous_star A] :
If A is a topological module over a commutative R with compatible actions,
then star is a continuous semilinear equivalence.
Equations
- starL R = {to_linear_equiv := star_linear_equiv R _inst_6, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
starL_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]
[topological_space A]
[has_continuous_star A]
(ᾰ : A) :
@[simp]
theorem
starL'_apply
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[has_trivial_star R]
[add_comm_monoid A]
[star_add_monoid A]
[module R A]
[star_module R A]
[topological_space A]
[has_continuous_star A]
(ᾰ : A) :
⇑(starL' R) ᾰ = has_star.star ᾰ
@[simp]
theorem
starL'_symm_apply
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[has_trivial_star R]
[add_comm_monoid A]
[star_add_monoid A]
[module R A]
[star_module R A]
[topological_space A]
[has_continuous_star A]
(ᾰ : A) :
@[simp]
theorem
starL'_to_linear_equiv
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[has_trivial_star R]
[add_comm_monoid A]
[star_add_monoid A]
[module R A]
[star_module R A]
[topological_space A]
[has_continuous_star A] :
def
starL'
(R : Type u_1)
{A : Type u_2}
[comm_semiring R]
[star_ring R]
[has_trivial_star R]
[add_comm_monoid A]
[star_add_monoid A]
[module R A]
[star_module R A]
[topological_space A]
[has_continuous_star 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
- starL' R = (starL R).trans {to_linear_equiv := {to_fun := (add_equiv.refl A).to_fun, map_add' := _, map_smul' := _, inv_fun := (add_equiv.refl A).inv_fun, left_inv := _, right_inv := _}, continuous_to_fun := _, continuous_inv_fun := _}
theorem
continuous_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]
[topological_space A]
[has_continuous_add A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
theorem
continuous_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]
[topological_space A]
[has_continuous_sub A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
theorem
continuous_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]
[topological_space A]
[topological_add_group A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
theorem
continuous_decompose_prod_adjoint_symm
(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]
[topological_space A]
[topological_add_group A] :
@[simp]
theorem
self_adjoint_partL_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]
[topological_space A]
[has_continuous_add A]
[has_continuous_star A]
[has_continuous_const_smul R A]
(x : A) :
↑(⇑(self_adjoint_partL R A) x) = ⅟ 2 • (x + has_star.star x)
def
self_adjoint_partL
(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]
[topological_space A]
[has_continuous_add A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
A →L[R] ↥(self_adjoint A)
The self-adjoint part of an element of a star module, as a continuous linear map.
Equations
- self_adjoint_partL R A = {to_linear_map := self_adjoint_part R _inst_8, cont := _}
@[simp]
theorem
self_adjoint_partL_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]
[topological_space A]
[has_continuous_add A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
↑(self_adjoint_partL R A) = self_adjoint_part R
@[simp]
theorem
skew_adjoint_partL_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]
[topological_space A]
[has_continuous_sub A]
[has_continuous_star A]
[has_continuous_const_smul R A]
(x : A) :
↑(⇑(skew_adjoint_partL R A) x) = ⅟ 2 • (x - has_star.star x)
@[simp]
theorem
skew_adjoint_partL_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]
[topological_space A]
[has_continuous_sub A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
↑(skew_adjoint_partL R A) = skew_adjoint_part R
def
skew_adjoint_partL
(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]
[topological_space A]
[has_continuous_sub A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
A →L[R] ↥(skew_adjoint A)
The skew-adjoint part of an element of a star module, as a continuous linear map.
Equations
- skew_adjoint_partL R A = {to_linear_map := skew_adjoint_part R _inst_8, cont := _}
@[simp]
theorem
star_module.decompose_prod_adjointL_to_linear_equiv
(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]
[topological_space A]
[topological_add_group A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
def
star_module.decompose_prod_adjointL
(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]
[topological_space A]
[topological_add_group A]
[has_continuous_star A]
[has_continuous_const_smul R A] :
A ≃L[R] ↥(self_adjoint A) × ↥(skew_adjoint A)
The decomposition of elements of a star module into their self- and skew-adjoint parts, as a continuous linear equivalence.
Equations
- star_module.decompose_prod_adjointL R A = {to_linear_equiv := star_module.decompose_prod_adjoint R A _inst_8, continuous_to_fun := _, continuous_inv_fun := _}
@[simp]
theorem
star_module.decompose_prod_adjointL_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]
[topological_space A]
[topological_add_group A]
[has_continuous_star A]
[has_continuous_const_smul R A]
(ᾰ : A) :
⇑(star_module.decompose_prod_adjointL R A) ᾰ = (⇑(self_adjoint_part R) ᾰ, ⇑(skew_adjoint_part R) ᾰ)
@[simp]
theorem
star_module.decompose_prod_adjointL_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]
[topological_space A]
[topological_add_group A]
[has_continuous_star A]
[has_continuous_const_smul R A]
(ᾰ : ↥(self_adjoint A) × ↥(skew_adjoint A)) :