Documentation

TauCeti.RepresentationTheory.Spin.Polarization.Complement

Polarizations from complementary isotropic subspaces #

A finite-dimensional nondegenerate quadratic space which is the direct sum of two totally isotropic subspaces W and W' is polarized by them, with no orthogonal remainder: the polar form pairs W' perfectly with W. This file packages that observation as a constructor of TauCeti.SpinPolarizationData, so that a polarization whose two summands are given by a formula (for instance the two eigenspaces of a complexified orthogonal complex structure) can be produced from the isotropy and the complementarity of the summands alone.

The perfect pairing is the only nonformal field. A vector of W' pairing to zero with W also pairs to zero with the isotropic W', hence with all of V = W ⊕ W'; being isotropic, it lies in the radical, which vanishes. So the polar pairing is injective in each variable, the two summands have the same dimension, and the injective map from W' to the dual of W is an isomorphism. No assumption on the characteristic is needed.

Over a general commutative ring the perfect pairing has to be supplied: TauCeti.SpinPolarizationData.ofIsComplOfPairing builds the polarization from two complementary totally isotropic submodules together with a polar identification of W' with the dual of W whose left radical is trivial. Both ofIsCompl and the hyperbolic polarization TauCeti.SpinPolarizationData.hyperbolic are instances of it.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.SpinPolarizationData.ofIsComplOfPairing {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') (e : ↥W' ≃ₗ[K] Module.Dual K ↥W) (he : ∀ (y : ↥W') (x : ↥W), (e y) x = QuadraticMap.polar ⇑Q ↑x ↑y) (hsep : ∀ (x : ↥W), (∀ (y : ↥W'), QuadraticMap.polar ⇑Q ↑x ↑y = 0) → x = 0) :
SpinPolarizationData Q

The polarization by two complementary isotropic submodules with a given pairing. Over a commutative ring, two complementary totally isotropic submodules W and W' of a quadratic space are the two summands of a polarization with no orthogonal remainder, once an identification of W' with the dual of W given by the polar form is supplied, and the polar pairing has trivial left radical.

Instances For
    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.ofIsComplOfPairing_W {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') (e : ↥W' ≃ₗ[K] Module.Dual K ↥W) (he : ∀ (y : ↥W') (x : ↥W), (e y) x = QuadraticMap.polar ⇑Q ↑x ↑y) (hsep : ∀ (x : ↥W), (∀ (y : ↥W'), QuadraticMap.polar ⇑Q ↑x ↑y = 0) → x = 0) :
    (ofIsComplOfPairing hWW' hW hW' e he hsep).W = W
    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.ofIsComplOfPairing_W' {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') (e : ↥W' ≃ₗ[K] Module.Dual K ↥W) (he : ∀ (y : ↥W') (x : ↥W), (e y) x = QuadraticMap.polar ⇑Q ↑x ↑y) (hsep : ∀ (x : ↥W), (∀ (y : ↥W'), QuadraticMap.polar ⇑Q ↑x ↑y = 0) → x = 0) :
    (ofIsComplOfPairing hWW' hW hW' e he hsep).W' = W'
    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.ofIsComplOfPairing_line {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') (e : ↥W' ≃ₗ[K] Module.Dual K ↥W) (he : ∀ (y : ↥W') (x : ↥W), (e y) x = QuadraticMap.polar ⇑Q ↑x ↑y) (hsep : ∀ (x : ↥W), (∀ (y : ↥W'), QuadraticMap.polar ⇑Q ↑x ↑y = 0) → x = 0) :
    (ofIsComplOfPairing hWW' hW hW' e he hsep).line = ⊥
    source
    noncomputable def TauCeti.SpinPolarizationData.ofIsCompl {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} [FiniteDimensional K V] (hQ : QuadraticMap.Nondegenerate) (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') :
    SpinPolarizationData Q

    The polarization of a quadratic space by two complementary isotropic subspaces. If a finite-dimensional quadratic space (V, Q) with nondegenerate Q is the direct sum of two totally isotropic subspaces W and W', then W and W' are the two isotropic summands of a polarization of Q with no orthogonal remainder; the polar form identifies W' with the dual of W.

    Instances For
      source
      @[simp]
      theorem TauCeti.SpinPolarizationData.ofIsCompl_W {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} [FiniteDimensional K V] (hQ : QuadraticMap.Nondegenerate) (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') :
      (ofIsCompl hQ hWW' hW hW').W = W
      source
      @[simp]
      theorem TauCeti.SpinPolarizationData.ofIsCompl_W' {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} [FiniteDimensional K V] (hQ : QuadraticMap.Nondegenerate) (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') :
      (ofIsCompl hQ hWW' hW hW').W' = W'
      source
      @[simp]
      theorem TauCeti.SpinPolarizationData.ofIsCompl_line {K : Type u} [Field K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {W W' : Submodule K V} [FiniteDimensional K V] (hQ : QuadraticMap.Nondegenerate) (hWW' : IsCompl W W') (hW : QuadraticMap.IsTotallyIsotropic Q W) (hW' : QuadraticMap.IsTotallyIsotropic Q W') :
      (ofIsCompl hQ hWW' hW hW').line = ⊥