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.mulOpposite {R : Type u_1} {H : Type u_2} [Ring R] [AddCommGroup H] [Module R H] {ι : Type u_3} [Fintype ι] (b : Basis ι R H) : Basis ι R Hᵐᵒᵖ

Equations

• b.mulOpposite = Basis.mk ⋯ ⋯

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)

instance mulOpposite_finiteDimensional {R : Type u_1} {H : Type u_2} [DivisionRing R] [AddCommGroup H] [Module R H] [FiniteDimensional R H] : FiniteDimensional R Hᵐᵒᵖ

instance MulOpposite.hasInner {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] : Inner 𝕜 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 y : Hᵐᵒᵖ) : inner x y = inner (unop x) (unop y)

theorem MulOpposite.inner_eq' {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] (x y : H) : inner (op x) (op y) = inner x y

@[reducible]

instance MulOpposite.innerProductSpace {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 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 ⋯

instance MulOpposite.starModule {R : Type u_1} {H : Type u_2} [Star R] [SMul R H] [Star H] [StarModule R H] : StarModule R Hᵐᵒᵖ

theorem MulOpposite.opContinuousLinearEquiv_adjoint {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [CompleteSpace A] : ContinuousLinearMap.adjoint ↑(opContinuousLinearEquiv 𝕜) = ↑(opContinuousLinearEquiv 𝕜).symm

theorem MulOpposite.opLinearEquiv_adjoint {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [FiniteDimensional 𝕜 A] : LinearMap.adjoint ↑(opLinearEquiv 𝕜) = ↑(opLinearEquiv 𝕜).symm

theorem LinearMap.op_adjoint {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [FiniteDimensional 𝕜 A] (x : A →ₗ[𝕜] A) : adjoint x.op = (adjoint x).op