Documentation

TauCeti.LinearAlgebra.ExteriorAlgebra.DegreeScaling

Degree scaling of an exterior algebra #

For a unit r of the base ring, the scalar multiplication r • id induces an algebra automorphism of the exterior algebra ⋀ M, which multiplies the n-th exterior power by r ^ n. Conjugating by it rescales exterior multiplication by ι m by the factor r, rescales every contraction by the factor r⁻¹, and commutes with the grade involution.

These are the operators that change the normalization of a Fock action: conjugating a Clifford action on ⋀ W by a degree scaling replaces its creation operators by r times themselves and its annihilation operators by r⁻¹ times themselves, which preserves every creation–annihilation anticommutator.

Main definitions #

Main results #

source
noncomputable def TauCeti.ExteriorAlgebra.degreeScaling {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (r : Rˣ) :
ExteriorAlgebra R M ≃ₐ[R] ExteriorAlgebra R M

The degree scaling of an exterior algebra by a unit r: the algebra automorphism of ⋀ M induced by the scalar multiplication r • id of M. It multiplies the n-th exterior power by r ^ n (TauCeti.ExteriorAlgebra.degreeScaling_of_mem_exteriorPower).

Instances For
    source
    theorem ExteriorAlgebra.degreeScaling_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (r : Rˣ) (x : ExteriorAlgebra R M) :
    (TauCeti.ExteriorAlgebra.degreeScaling r) x = (map (↑r • LinearMap.id)) x

    The degree scaling is the exterior-algebra map induced by r • id.

    source
    @[simp]
    theorem TauCeti.ExteriorAlgebra.degreeScaling_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (r : Rˣ) (m : M) :
    (degreeScaling r) ((ExteriorAlgebra.ι R) m) = ↑r • (ExteriorAlgebra.ι R) m

    The degree scaling by r multiplies a generator by r.

    source
    @[simp]
    theorem TauCeti.ExteriorAlgebra.degreeScaling_symm {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (r : Rˣ) :
    (degreeScaling r).symm = degreeScaling r⁻¹

    The inverse of the degree scaling by r is the degree scaling by r⁻¹.

    source
    @[simp]
    theorem TauCeti.ExteriorAlgebra.degreeScaling_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] :
    degreeScaling 1 = AlgEquiv.refl

    The degree scaling by the unit 1 is the identity.

    source
    theorem TauCeti.ExteriorAlgebra.degreeScaling_of_mem_exteriorPower {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (r : Rˣ) {n : ℕ} {x : ExteriorAlgebra R M} (hx : x ∈ ⋀[R]^n M) :
    (degreeScaling r) x = ↑r ^ n • x

    The degree scaling acts on the n-th exterior power by r ^ n.

    source
    @[simp]
    theorem TauCeti.ExteriorAlgebra.degreeScaling_basis {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {I : Type u_1} [LinearOrder I] (b : Module.Basis I R M) (r : Rˣ) (s : Finset I) :
    (degreeScaling r) (b.ExteriorAlgebra s) = ↑r ^ s.card • b.ExteriorAlgebra s

    The degree scaling acts on an exterior-basis vector by r to the size of its index set. The basis vector indexed by s lies in the s.card-th exterior power.

    source
    @[simp]
    theorem ExteriorAlgebra.degreeScaling_involute {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (r : Rˣ) (x : ExteriorAlgebra R M) :
    (TauCeti.ExteriorAlgebra.degreeScaling r) (CliffordAlgebra.involute x) = CliffordAlgebra.involute ((TauCeti.ExteriorAlgebra.degreeScaling r) x)

    The degree scaling commutes with the grade involution.

    source
    @[simp]
    theorem ExteriorAlgebra.degreeScaling_contractLeft {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (r : Rˣ) (d : Module.Dual R M) (x : ExteriorAlgebra R M) :
    (TauCeti.ExteriorAlgebra.degreeScaling r) ((CliffordAlgebra.contractLeft d) x) = ↑r⁻¹ • (CliffordAlgebra.contractLeft d) ((TauCeti.ExteriorAlgebra.degreeScaling r) x)

    Conjugating a contraction by the degree scaling by r multiplies it by r⁻¹.