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.
theorem
Basis.mulOpposite_apply
{R : Type u_2}
{H : Type u_3}
[Ring R]
[AddCommGroup H]
[Module R H]
{ι : Type u_1}
[Fintype ι]
(b : Basis ι R H)
(i : ι)
:
b.mulOpposite i = MulOpposite.op (b i)
theorem
Basis.mulOpposite_repr_eq
{R : Type u_2}
{H : Type u_3}
[Ring R]
[AddCommGroup H]
[Module R H]
{ι : Type u_1}
[Fintype ι]
(b : Basis ι R H)
:
b.mulOpposite.repr = (MulOpposite.opLinearEquiv R).symm ≪≫ₗ b.repr
theorem
Basis.mulOpposite_repr_apply
{R : Type u_2}
{H : Type u_3}
[Ring R]
[AddCommGroup H]
[Module R H]
{ι : Type u_1}
[Fintype ι]
(b : Basis ι R H)
(x : Hᵐᵒᵖ)
:
b.mulOpposite.repr x = b.repr (MulOpposite.unop x)
theorem
mulOpposite_finiteDimensional
{R : Type u_1}
{H : Type u_2}
[DivisionRing R]
[AddCommGroup H]
[Module R H]
[FiniteDimensional R H]
:
instance
MulOpposite.hasInner
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
:
Equations
- MulOpposite.hasInner = { inner := fun (x y : Hᵐᵒᵖ) => inner (MulOpposite.unop x) (MulOpposite.unop y) }
theorem
MulOpposite.inner_eq
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
(x : Hᵐᵒᵖ)
(y : Hᵐᵒᵖ)
:
inner x y = inner (MulOpposite.unop x) (MulOpposite.unop y)
theorem
MulOpposite.inner_eq'
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
(x : H)
(y : H)
:
inner (MulOpposite.op x) (MulOpposite.op y) = inner x y
@[reducible]
instance
MulOpposite.innerProductSpace
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
:
Equations
- MulOpposite.innerProductSpace = InnerProductSpace.mk ⋯ ⋯ ⋯ ⋯
theorem
Basis.mulOpposite_is_orthonormal_iff
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
{ι : Type u_3}
[Fintype ι]
(b : Basis ι 𝕜 H)
:
Orthonormal 𝕜 ⇑b ↔ Orthonormal 𝕜 ⇑b.mulOpposite
noncomputable def
OrthonormalBasis.mulOpposite
{𝕜 : Type u_1}
{H : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup H]
[InnerProductSpace 𝕜 H]
{ι : Type u_3}
[Fintype ι]
(b : OrthonormalBasis ι 𝕜 H)
:
OrthonormalBasis ι 𝕜 Hᵐᵒᵖ
Equations
- b.mulOpposite = b.toBasis.mulOpposite.toOrthonormalBasis ⋯
Instances For
instance
MulOpposite.starModule
{R : Type u_1}
{H : Type u_2}
[Star R]
[SMul R H]
[Star H]
[StarModule R H]
:
StarModule R Hᵐᵒᵖ
Equations
- ⋯ = ⋯
theorem
MulOpposite.opContinuousLinearEquiv_adjoint
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup A]
[InnerProductSpace 𝕜 A]
[CompleteSpace A]
:
ContinuousLinearMap.adjoint ↑(MulOpposite.opContinuousLinearEquiv 𝕜) = ↑(MulOpposite.opContinuousLinearEquiv 𝕜).symm
theorem
MulOpposite.opLinearEquiv_adjoint
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup A]
[InnerProductSpace 𝕜 A]
[FiniteDimensional 𝕜 A]
:
LinearMap.adjoint ↑(MulOpposite.opLinearEquiv 𝕜) = ↑(MulOpposite.opLinearEquiv 𝕜).symm
theorem
LinearMap.op_adjoint
{𝕜 : Type u_1}
{A : Type u_2}
[RCLike 𝕜]
[NormedAddCommGroup A]
[InnerProductSpace 𝕜 A]
[FiniteDimensional 𝕜 A]
(x : A →ₗ[𝕜] A)
:
LinearMap.adjoint x.op = (LinearMap.adjoint x).op