The coordinate integral lattice in an exterior algebra

Let b : Basis ι ℚ M. The exterior basis b.ExteriorAlgebra, indexed by finite subsets of ι, defines a canonical integral form of ExteriorAlgebra ℚ M: take the ℤ-span of its basis vectors. This file constructs that lattice and proves that it is closed under the exterior product.

The multiplication statement is the useful point. Products of exterior basis vectors are either zero or another basis vector with sign given by the shuffle permutation, so multiplication does not introduce denominators. In particular, exterior multiplication by any basis vector preserves the lattice. This is the creation-operator half of the integral spinor lattice used to construct the simply connected type-B and type-D Chevalley carriers.

Main definitions and results

• TauCeti.ExteriorAlgebra.integralLattice: the ℤ-span of an exterior basis.
• TauCeti.ExteriorAlgebra.integralLatticeBasis: the exterior basis restricted to ℤ.
• TauCeti.ExteriorAlgebra.map_mem_integralLattice: a linear map preserves the lattice as soon as it preserves it on the exterior basis.
• TauCeti.ExteriorAlgebra.mem_integralLattice_iff: membership means that every exterior-basis coordinate is integral.
• TauCeti.ExteriorAlgebra.mul_mem_integralLattice: the lattice is closed under multiplication.
• TauCeti.ExteriorAlgebra.ι_basis_mul_mem_integralLattice: creation by a basis vector preserves the lattice.
• TauCeti.ExteriorAlgebra.contractLeft_coord_mem_integralLattice: contraction by a dual basis coordinate preserves the lattice.
• TauCeti.ExteriorAlgebra.involute_mem_integralLattice: the grade involution preserves the lattice.

Roadmap

This is the integral-lattice input for the full-weight spin carriers required by Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md. Those type-B and type-D carriers are in turn consumed by milestone L0 of TauCetiRoadmap/CFSGStatement/README.md.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

def TauCeti.ExteriorAlgebra.integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) : Submodule ℤ (ExteriorAlgebra ℚ M)

The coordinate ℤ-lattice in an exterior algebra, spanned by the exterior basis attached to b.

Equations

• TauCeti.ExteriorAlgebra.integralLattice b = Submodule.span ℤ (Set.range ⇑b.ExteriorAlgebra)

theorem TauCeti.ExteriorAlgebra.integralLattice_eq_span {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) : integralLattice b = Submodule.span ℤ (Set.range ⇑b.ExteriorAlgebra)

The coordinate integral lattice is the ℤ-span of the exterior basis, which is the form in which the generic span lemmas about integral spans apply to it. The body of integralLattice is not @[expose]d, so downstream modules cannot reach that span by rw [integralLattice]; this is the accessor they use instead.

theorem TauCeti.ExteriorAlgebra.map_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) (f : ExteriorAlgebra ℚ M →ₗ[ℤ] ExteriorAlgebra ℚ M) (hf : ∀ (s : Finset ι), f (b.ExteriorAlgebra s) ∈ integralLattice b) {x : ExteriorAlgebra ℚ M} (hx : x ∈ integralLattice b) : f x ∈ integralLattice b

A linear map preserves the coordinate integral lattice as soon as it does so on the exterior basis, since that basis spans the lattice. This is the shared induction behind every lattice-preservation statement below.

@[simp]

theorem TauCeti.ExteriorAlgebra.mem_integralLattice_iff {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) {x : ExteriorAlgebra ℚ M} : x ∈ integralLattice b ↔ ∀ (s : Finset ι), ∃ (z : ℤ), ↑z = (b.ExteriorAlgebra.repr x) s

An element belongs to the coordinate integral lattice exactly when all of its exterior-basis coordinates are integers.

theorem TauCeti.ExteriorAlgebra.basis_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) (s : Finset ι) : b.ExteriorAlgebra s ∈ integralLattice b

Every exterior-basis vector belongs to the coordinate integral lattice.

noncomputable def TauCeti.ExteriorAlgebra.integralLatticeBasis {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) : Module.Basis (Finset ι) ℤ ↥(integralLattice b)

The exterior basis, restricted from rational to integer scalars, is a basis of the coordinate integral lattice.

Equations

• TauCeti.ExteriorAlgebra.integralLatticeBasis b = Module.Basis.restrictScalars ℤ b.ExteriorAlgebra

@[simp]

theorem TauCeti.ExteriorAlgebra.coe_integralLatticeBasis {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) (s : Finset ι) : ↑((integralLatticeBasis b) s) = b.ExteriorAlgebra s

A vector of the integral-lattice basis is the corresponding rational exterior-basis vector.

instance TauCeti.ExteriorAlgebra.instFreeIntSubtypeExteriorAlgebraRatMemSubmoduleIntegralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) : Module.Free ℤ ↥(integralLattice b)

theorem TauCeti.ExteriorAlgebra.span_integralLattice_eq_top {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) : Submodule.span ℚ ↑(integralLattice b) = ⊤

The rational span of the coordinate integral lattice is the whole exterior algebra.

@[instance_reducible]

noncomputable def TauCeti.ExteriorAlgebra.finiteIndexFintype {ι : Type u_1} [Finite ι] : Fintype ι

The finite type structure on the index type used within this section.

Equations

• TauCeti.ExteriorAlgebra.finiteIndexFintype = Fintype.ofFinite ι

instance TauCeti.ExteriorAlgebra.instFiniteIntSubtypeExteriorAlgebraRatMemSubmoduleIntegralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) [Finite ι] : Module.Finite ℤ ↥(integralLattice b)

@[simp]

theorem TauCeti.ExteriorAlgebra.finrank_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) [Finite ι] : Module.finrank ℤ ↥(integralLattice b) = 2 ^ Nat.card ι

The coordinate integral lattice has rank 2 ^ card ι.

instance TauCeti.ExteriorAlgebra.instIsLatticeIntRatExteriorAlgebraIntegralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) [Finite ι] : Submodule.IsLattice ℚ (integralLattice b)

theorem TauCeti.ExteriorAlgebra.one_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) : 1 ∈ integralLattice b

The unit of the exterior algebra belongs to the coordinate integral lattice.

theorem TauCeti.ExteriorAlgebra.basis_mul_basis_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) (s t : Finset ι) : b.ExteriorAlgebra s * b.ExteriorAlgebra t ∈ integralLattice b

The product of two exterior-basis vectors belongs to the coordinate integral lattice.

theorem TauCeti.ExteriorAlgebra.mul_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) {x y : ExteriorAlgebra ℚ M} (hx : x ∈ integralLattice b) (hy : y ∈ integralLattice b) : x * y ∈ integralLattice b

The coordinate integral lattice is closed under the exterior-algebra multiplication.

theorem TauCeti.ExteriorAlgebra.ι_basis_mul_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) (i : ι) {x : ExteriorAlgebra ℚ M} (hx : x ∈ integralLattice b) : (ExteriorAlgebra.ι ℚ) (b i) * x ∈ integralLattice b

Exterior multiplication by a basis vector preserves the coordinate integral lattice.

theorem TauCeti.ExteriorAlgebra.involute_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) {x : ExteriorAlgebra ℚ M} (hx : x ∈ integralLattice b) : CliffordAlgebra.involute x ∈ integralLattice b

The grade involution preserves the coordinate integral lattice: it rescales each exterior-basis vector by the sign of the parity of its index set.

theorem TauCeti.ExteriorAlgebra.contractLeft_coord_basis_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) (i : ι) (s : Finset ι) : (CliffordAlgebra.contractLeft (b.coord i)) (b.ExteriorAlgebra s) ∈ integralLattice b

Contracting an exterior-basis vector by a dual basis coordinate gives an element of the coordinate integral lattice.

theorem TauCeti.ExteriorAlgebra.contractLeft_coord_mem_integralLattice {M : Type u} [AddCommGroup M] [Module ℚ M] {ι : Type u_1} [LinearOrder ι] (b : Module.Basis ι ℚ M) (i : ι) {x : ExteriorAlgebra ℚ M} (hx : x ∈ integralLattice b) : (CliffordAlgebra.contractLeft (b.coord i)) x ∈ integralLattice b

Contraction by a dual basis coordinate preserves the coordinate integral lattice. This is the annihilation-operator counterpart of ι_basis_mul_mem_integralLattice.