Documentation

TauCeti.RepresentationTheory.Spin.Polarization.DegreeScaling

Rescaling the spinor module of a polarization #

For a polarization V = W ⊕ W' ⊕ L of a quadratic space and a unit r of the base ring, the degree scaling T_r of ⋀ W, which multiplies the p-th exterior power by r ^ p, conjugates the spinor representation TauCeti.spinAction into another representation of the same Clifford algebra on the same carrier. In it a vector x of W acts by r times exterior multiplication, a vector y of W' by r⁻¹ times contraction, and a vector of the remainder as before.

This is how the normalization of a Fock action is changed. The native action contracts against the polar form QuadraticMap.polar Q; when Q is the negative -g of a metric, this is -2 g, and the degree scaling by √2 turns the native action into the symmetric √2-normalized one, in which creation and contraction against g carry the same factor.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.SpinPolarizationData.scaledSpinAction {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (r : Kˣ) :
CliffordAlgebra Q →ₐ[K] Module.End K (ExteriorAlgebra K ↥P.W)

The rescaled spinor representation: the conjugate of the spinor representation TauCeti.spinAction Q P by the degree scaling of ⋀ W by the unit r. A vector of W acts by r times exterior multiplication, a vector of W' by r⁻¹ times contraction, and a vector of the orthogonal remainder by the unchanged parity operator.

Instances For
    source
    theorem TauCeti.SpinPolarizationData.scaledSpinAction_apply {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (r : Kˣ) (a : CliffordAlgebra Q) (s : ExteriorAlgebra K ↥P.W) :
    ((P.scaledSpinAction r) a) s = (ExteriorAlgebra.degreeScaling r) (((spinAction Q P) a) ((ExteriorAlgebra.degreeScaling r⁻¹) s))

    The rescaled spinor representation is the conjugate of the spinor representation by the degree scaling.

    source
    theorem TauCeti.SpinPolarizationData.degreeScaling_comp_spinAction {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (r : Kˣ) (a : CliffordAlgebra Q) :
    (ExteriorAlgebra.degreeScaling r).toLinearMap ∘ₗ (spinAction Q P) a = (P.scaledSpinAction r) a ∘ₗ (ExteriorAlgebra.degreeScaling r).toLinearMap

    The degree scaling intertwines the spinor representation with its rescaled form: T_r ∘ spinAction a = scaledSpinAction r a ∘ T_r.

    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.scaledSpinAction_one {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) :
    P.scaledSpinAction 1 = spinAction Q P

    The rescaling by the unit 1 is the spinor representation itself.

    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.scaledSpinAction_ι_coe_W {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (r : Kˣ) (x : ↥P.W) :
    (P.scaledSpinAction r) ((CliffordAlgebra.ι Q) ↑x) = ↑r • P.wedge x

    In the rescaled spinor representation a vector of W acts by r times exterior multiplication.

    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.scaledSpinAction_ι_coe_W' {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (r : Kˣ) (y : ↥P.W') :
    (P.scaledSpinAction r) ((CliffordAlgebra.ι Q) ↑y) = ↑r⁻¹ • P.contract y

    In the rescaled spinor representation a vector of W' acts by r⁻¹ times contraction.

    source
    @[simp]
    theorem TauCeti.SpinPolarizationData.scaledSpinAction_ι_coe_line {K : Type u} [CommRing K] {V : Type v} [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (P : SpinPolarizationData Q) (r : Kˣ) (z : ↥P.line) :
    (P.scaledSpinAction r) ((CliffordAlgebra.ι Q) ↑z) = P.lineOperator z

    In the rescaled spinor representation a vector of the orthogonal remainder still acts by its scalar coordinate times the parity operator.