Documentation

TauCeti.Analysis.Normed.Module.Alternating.TopDegree

Scalar coordinates for top-degree continuous alternating forms #

Over a complete nontrivially normed field, evaluation on a basis identifies the space of top-degree forms with the scalar field as a continuous linear equivalence. Its inverse multiplies the continuous determinant form of that basis, so these forms make up a line (Module.Basis.finrank_continuousAlternatingMap_eq_one). This construction needs only a Hausdorff topological vector space, with no choice of norm or inner product.

source
noncomputable def Module.Basis.continuousDet {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Basis ι 𝕜 E) :
E [⋀^ι]→L[𝕜] 𝕜

The determinant form of a basis as a continuous alternating map.

Instances For
    source
    @[simp]
    theorem Module.Basis.continuousDet_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Basis ι 𝕜 E) (v : ι → E) :
    b.continuousDet v = b.det v
    source
    @[simp]
    theorem Module.Basis.continuousDet_toAlternatingMap {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Basis ι 𝕜 E) :
    b.continuousDet.toAlternatingMap = b.det
    source
    noncomputable def Module.Basis.topFormEquiv {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Basis ι 𝕜 E) :
    E [⋀^ι]→L[𝕜] 𝕜 ≃L[𝕜] 𝕜

    Evaluation on a basis is a continuous linear equivalence from top-degree forms to scalars. The inverse sends c to c times the determinant form of the basis.

    Instances For
      source
      @[simp]
      theorem Module.Basis.topFormEquiv_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Basis ι 𝕜 E) (ω : E [⋀^ι]→L[𝕜] 𝕜) :
      b.topFormEquiv ω = ω ⇑b
      source
      theorem Module.Basis.topFormEquiv_symm_eq_smul {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Basis ι 𝕜 E) (c : 𝕜) :
      b.topFormEquiv.symm c = c • b.continuousDet

      The inverse scalar coordinate map multiplies the continuous determinant form.

      source
      @[simp]
      theorem Module.Basis.topFormEquiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Fintype ι] [DecidableEq ι] (b : Basis ι 𝕜 E) (c : 𝕜) (v : ι → E) :
      (b.topFormEquiv.symm c) v = c * b.det v
      source
      theorem Module.Basis.finrank_continuousAlternatingMap_eq_one {𝕜 : Type u_1} {E : Type u_2} {ι : Type u_3} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [IsTopologicalAddGroup E] [T2Space E] [ContinuousSMul 𝕜 E] [Finite ι] (b : Basis ι 𝕜 E) :
      finrank 𝕜 (E [⋀^ι]→L[𝕜] 𝕜) = 1

      The top-degree scalar-valued continuous alternating forms on a space with a finite basis form a line.