Documentation

LeanPool.Monlib4.LinearAlgebra.Ips.MulOp

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.

source
@[reducible, inline]
noncomputable abbrev Basis.mulOpposite {R : Type u_1} {H : Type u_2} [Ring R] [AddCommGroup H] [Module R H] {ι : Type u_3} (b : Module.Basis ι R H) :
Module.Basis ι R Hᵐᵒᵖ

Compatibility alias for the basis on a multiplicative opposite space.

Equations
Instances For
    source
    theorem Basis.mulOpposite_apply {R : Type u_2} {H : Type u_3} [Ring R] [AddCommGroup H] [Module R H] {ι : Type u_1} (b : Module.Basis ι R H) (i : ι) :
    b.mulOpposite i = MulOpposite.op (b i)
    source
    theorem Basis.mulOpposite_repr_eq {R : Type u_2} {H : Type u_3} [Ring R] [AddCommGroup H] [Module R H] {ι : Type u_1} (b : Module.Basis ι R H) :
    b.mulOpposite.repr = (MulOpposite.opLinearEquiv R).symm ≪≫ₗ b.repr
    source
    theorem Basis.mulOpposite_repr_apply {R : Type u_2} {H : Type u_3} [Ring R] [AddCommGroup H] [Module R H] {ι : Type u_1} (b : Module.Basis ι R H) (x : Hᵐᵒᵖ) :
    b.mulOpposite.repr x = b.repr (MulOpposite.unop x)
    source
    theorem mulOpposite_finiteDimensional {R : Type u_1} {H : Type u_2} [DivisionRing R] [AddCommGroup H] [Module R H] [FiniteDimensional R H] :
    FiniteDimensional R Hᵐᵒᵖ
    source
    @[reducible, inline]
    abbrev MulOpposite.hasInner {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] :
    Inner 𝕜 Hᵐᵒᵖ

    The named inner-product data on a multiplicative opposite space.

    Equations
    Instances For
      source
      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)
      source
      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
      source
      @[reducible, inline]
      abbrev MulOpposite.innerProductSpace {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] :
      InnerProductSpace 𝕜 Hᵐᵒᵖ

      The named inner-product-space structure on a multiplicative opposite space.

      Equations
      Instances For
        source
        theorem Basis.orthonormal_iff_mulOpposite {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} (b : Module.Basis ι 𝕜 H) :
        Orthonormal 𝕜 ⇑b ↔ Orthonormal 𝕜 ⇑b.mulOpposite
        source
        theorem Basis.mulOpposite_is_orthonormal_iff {𝕜 : Type u_1} {H : Type u_2} [RCLike 𝕜] [NormedAddCommGroup H] [InnerProductSpace 𝕜 H] {ι : Type u_3} (b : Module.Basis ι 𝕜 H) :
        Orthonormal 𝕜 ⇑b ↔ Orthonormal 𝕜 ⇑b.mulOpposite
        source
        instance MulOpposite.starModule {R : Type u_1} {H : Type u_2} [Star R] [SMul R H] [Star H] [StarModule R H] :
        StarModule R Hᵐᵒᵖ
        source
        theorem MulOpposite.opContinuousLinearEquiv_adjoint {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [CompleteSpace A] :
        ContinuousLinearMap.adjoint ↑(opContinuousLinearEquiv 𝕜) = ↑(opContinuousLinearEquiv 𝕜).symm
        source
        theorem MulOpposite.opLinearEquiv_adjoint {𝕜 : Type u_1} {A : Type u_2} [RCLike 𝕜] [NormedAddCommGroup A] [InnerProductSpace 𝕜 A] [FiniteDimensional 𝕜 A] :
        LinearMap.adjoint ↑(opLinearEquiv 𝕜) = ↑(opLinearEquiv 𝕜).symm
        source
        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