Some results on the opposite vector space #
This file contains the construction of the basis of an opposite space; and the construction of the opposite inner product space.
noncomputable
def
basis.mul_opposite
{R : Type u_1}
{H : Type u_2}
[ring R]
[add_comm_group H]
[module R H]
{ι : Type u_3}
[fintype ι]
(b : basis ι R H) :
Equations
- b.mul_opposite = basis.mk _ _
theorem
basis.mul_opposite_apply
{R : Type u_1}
{H : Type u_2}
[ring R]
[add_comm_group H]
[module R H]
{ι : Type u_3}
[fintype ι]
(b : basis ι R H)
(i : ι) :
⇑(b.mul_opposite) i = mul_opposite.op (⇑b i)
theorem
basis.mul_opposite_repr_eq
{R : Type u_1}
{H : Type u_2}
[ring R]
[add_comm_group H]
[module R H]
{ι : Type u_3}
[fintype ι]
(b : basis ι R H) :
theorem
basis.mul_opposite_repr_apply
{R : Type u_1}
{H : Type u_2}
[ring R]
[add_comm_group H]
[module R H]
{ι : Type u_3}
[fintype ι]
(b : basis ι R H)
(x : Hᵐᵒᵖ) :
⇑(b.mul_opposite.repr) x = ⇑(b.repr) (mul_opposite.unop x)
@[instance]
theorem
mul_opposite_finite_dimensional
{R : Type u_1}
{H : Type u_2}
[division_ring R]
[add_comm_group H]
[module R H]
[finite_dimensional R H] :
@[instance]
def
mul_opposite.has_inner
{𝕜 : Type u_1}
{H : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[inner_product_space 𝕜 H] :
Equations
- mul_opposite.has_inner = {inner := λ (x y : Hᵐᵒᵖ), has_inner.inner (mul_opposite.unop x) (mul_opposite.unop y)}
@[instance, reducible]
def
mul_opposite.inner_product_space
{𝕜 : Type u_1}
{H : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[inner_product_space 𝕜 H] :
Equations
- mul_opposite.inner_product_space = {to_normed_space := mul_opposite.normed_space inner_product_space.to_normed_space, to_has_inner := mul_opposite.has_inner _inst_7, norm_sq_eq_inner := _, conj_symm := _, add_left := _, smul_left := _}
theorem
mul_opposite.inner_eq
{𝕜 : Type u_1}
{H : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[inner_product_space 𝕜 H]
(x y : Hᵐᵒᵖ) :
theorem
mul_opposite.inner_eq'
{𝕜 : Type u_1}
{H : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[inner_product_space 𝕜 H]
(x y : H) :
has_inner.inner (mul_opposite.op x) (mul_opposite.op y) = has_inner.inner x y
theorem
basis.mul_opposite_is_orthonormal_iff
{𝕜 : Type u_1}
{H : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[inner_product_space 𝕜 H]
{ι : Type u_3}
[fintype ι]
(b : basis ι 𝕜 H) :
orthonormal 𝕜 ⇑b ↔ orthonormal 𝕜 ⇑(b.mul_opposite)
noncomputable
def
orthonormal_basis.mul_opposite
{𝕜 : Type u_1}
{H : Type u_2}
[is_R_or_C 𝕜]
[normed_add_comm_group H]
[inner_product_space 𝕜 H]
{ι : Type u_3}
[fintype ι]
(b : orthonormal_basis ι 𝕜 H) :
orthonormal_basis ι 𝕜 Hᵐᵒᵖ
Equations
@[protected, instance]
def
mul_opposite.star_module
{R : Type u_1}
{H : Type u_2}
[has_star R]
[has_smul R H]
[has_star H]
[star_module R H] :
star_module R Hᵐᵒᵖ