The root lattice of type Aₙ and its discriminant form

The positive root lattice of type Aₙ is the rank-n integral lattice whose Gram matrix in the simple-root basis is the Cartan matrix CartanMatrix.A n. This file constructs it inside Fin n → ℚ, proves it even and nondegenerate, with minimum 2 when n ≥ 1, and computes its discriminant form:

det Aₙ = n + 1,   A_{Aₙ} ≃+ ℤ/(n+1),   q(ω₁) = n / (2 (n + 1)),   b(ω₁, ω₁) = n / (n + 1).

The generator is the class of the first fundamental weight ω₁, written in the simple-root coordinates ω₁ = ∑ⱼ ((n - j) / (n + 1)) αⱼ that the inverse Cartan matrix dictates. Those coordinates are verified against the lattice, not assumed: form_typeAFundamentalWeight_simpleRoot proves ⟨ω₁, αᵢ⟩ = δ_{i,0} directly from the row combinations of CartanMatrix.A n, which then gives ⟨ω₁, ω₁⟩ = n / (n + 1) and hence the displayed half-norm value. When n > 0, the class of ω₁ has additive order exactly n + 1 because its last simple-root coordinate is 1 / (n + 1); at rank zero, the order statement is trivial. The discriminant group has that same order, so ω₁ generates.

The half-norm convention is the one fixed by the integral-lattices roadmap: q_L(x) = ⟨x,x⟩ / 2 in ℚ/ℤ. Nikulin's full-norm value for this row is n / (n + 1).

Those values determine the finite quadratic module, not merely the group: since ω₁ generates, the quadratic value k² n / (2 (n + 1)) of k • ω₁ and the pairing j k n / (n + 1) of j • ω₁ with k • ω₁ are recorded for every integer multiple, and the resulting form is identified with the cyclic model TauCeti.IntegralLattice.typeAStandardQuadraticModule on ℤ/(n+1) whose generator carries n / (2 (n + 1)). That identification is an isometry of finite quadratic modules, so it also transports nondegeneracy from the discriminant form of the nondegenerate lattice to the model.

The identification of this simple-root model with the classical coordinate model {x ∈ ℤ^{n+1} | ∑ xᵢ = 0} is in TauCeti.LinearAlgebra.IntegralLattice.RootLattice.TypeA.ZeroSum.

Main declarations

• TauCeti.IntegralLattice.typeARootLattice: the lattice, with Gram matrix CartanMatrix.A n.
• TauCeti.IntegralLattice.form_typeASimpleRoot_typeASimpleRoot: its simple-root Gram matrix is CartanMatrix.A n.
• TauCeti.IntegralLattice.sum_smul_typeASimpleRoot: every vector is the combination of the simple roots with its own coordinates.
• TauCeti.IntegralLattice.typeASimpleRootBasis: the simple roots as a ℤ-basis of the lattice.
• TauCeti.IntegralLattice.isEven_typeARootLattice: it is even.
• TauCeti.IntegralLattice.isPosDef_typeARootLattice: it is positive definite.
• TauCeti.IntegralLattice.determinant_typeARootLattice: its determinant is n + 1.
• TauCeti.IntegralLattice.minimum_typeARootLattice: for n ≥ 1 its minimum is 2.
• TauCeti.IntegralLattice.typeAFundamentalWeight: the first fundamental weight ω₁.
• TauCeti.IntegralLattice.typeAFundamentalWeightClass: its class in the discriminant group.
• TauCeti.IntegralLattice.mk_eq_zsmul_typeAFundamentalWeightClass_iff: a dual vector lies in the class k ω₁ exactly when it differs from k ω₁ by a lattice vector.
• TauCeti.IntegralLattice.form_typeAFundamentalWeight_self: ⟨ω₁, ω₁⟩ = n / (n + 1).
• TauCeti.IntegralLattice.addOrderOf_typeAFundamentalWeightClass: the class of ω₁ has order n + 1.
• TauCeti.IntegralLattice.zmultiples_typeAFundamentalWeightClass: that class generates the discriminant group.
• TauCeti.IntegralLattice.typeADiscriminantGroupEquiv: the resulting isomorphism ZMod (n + 1) ≃+ A_{Aₙ}.
• TauCeti.IntegralLattice.typeADiscriminantGroupEquiv_apply: it carries the label a to the class a.val • ω₁.
• TauCeti.IntegralLattice.discriminantQuadraticMap_typeAFundamentalWeightClass: q(ω₁) = n / (2 (n + 1)).
• TauCeti.IntegralLattice.discriminantPairing_typeAFundamentalWeightClass: b(ω₁, ω₁) = n / (n + 1).
• TauCeti.IntegralLattice.discriminantQuadraticMap_zsmul_typeAFundamentalWeightClass: the quadratic value on every multiple of ω₁.
• TauCeti.IntegralLattice.discriminantPairing_zsmul_typeAFundamentalWeightClass: the pairing on every pair of multiples of ω₁.
• TauCeti.IntegralLattice.typeAStandardQuadraticModule: the cyclic model on ℤ/(n+1).
• TauCeti.IntegralLattice.typeAOneZModStandardIsometry: the identity comparison between the A₁ alphabet and the standard binary quadratic alphabet.
• TauCeti.IntegralLattice.typeAStandardQuadraticModule_one_quadratic: the A₁ quadratic value on each binary residue.
• TauCeti.IntegralLattice.typeADiscriminantQuadraticIsometry: the model is the discriminant quadratic module of the Aₙ root lattice.
• TauCeti.IntegralLattice.isNondegenerate_typeAStandardQuadraticModule: the model is nondegenerate.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §6.1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 5, the Aₙ row of the ADE table.

The lattice

noncomputable def TauCeti.IntegralLattice.typeARootLattice (n : ℕ) : IntegralLattice (Fin n → ℚ)

The positive root lattice of type Aₙ: the rank-n integral lattice on Fin n → ℚ whose Gram matrix in the standard basis of simple roots is CartanMatrix.A n.

theorem TauCeti.IntegralLattice.isPosDef_typeARootLattice (n : ℕ) : (typeARootLattice n).IsPosDef

The type Aₙ root lattice is positive definite, its Gram matrix being the positive definite Cartan matrix of the type.

noncomputable def TauCeti.IntegralLattice.typeASimpleRoot (n : ℕ) (i : Fin n) : Fin n → ℚ

The i-th simple root of the type Aₙ root lattice, as a vector of the ambient space.

This is sealed rather than an abbrev: reducibility would let Pi.basisFun_apply rewrite underneath it, taking the Gram-matrix and pairing lemmas below out of simp normal form.

@[simp]

theorem TauCeti.IntegralLattice.typeASimpleRoot_apply (n : ℕ) (i j : Fin n) : typeASimpleRoot n i j = if j = i then 1 else 0

The i-th simple root is the i-th standard coordinate vector.

theorem TauCeti.IntegralLattice.sum_smul_typeASimpleRoot {n : ℕ} (x : Fin n → ℚ) : ∑ j : Fin n, x j • typeASimpleRoot n j = x

Every vector of the ambient space is the combination of the simple roots with its own coordinates as coefficients.

theorem TauCeti.IntegralLattice.typeARootLattice_form_apply (n : ℕ) (x y : Fin n → ℚ) : ((typeARootLattice n).form x) y = ∑ i : Fin n, ∑ j : Fin n, x i * ↑(CartanMatrix.A n i j) * y j

The form of the type Aₙ root lattice, expanded in the standard coordinates.

theorem TauCeti.IntegralLattice.typeARootLattice_form_simpleRoot (n : ℕ) (x : Fin n → ℚ) (i : Fin n) : ((typeARootLattice n).form x) (typeASimpleRoot n i) = ∑ k : Fin n, x k * ↑(CartanMatrix.A n k i)

Pairing an arbitrary vector against a simple root collapses the double sum to a single one.

@[simp]

theorem TauCeti.IntegralLattice.form_typeASimpleRoot_typeASimpleRoot (n : ℕ) (i j : Fin n) : ((typeARootLattice n).form (typeASimpleRoot n i)) (typeASimpleRoot n j) = ↑(CartanMatrix.A n i j)

The Gram matrix of the type Aₙ root lattice in its simple-root basis is the Cartan matrix CartanMatrix.A n.

@[simp]

theorem TauCeti.IntegralLattice.mem_typeARootLattice_carrier_iff (n : ℕ) (x : Fin n → ℚ) : x ∈ (typeARootLattice n).carrier ↔ ∀ (i : Fin n), ∃ (z : ℤ), ↑z = x i

A vector belongs to the type Aₙ root lattice exactly when all of its simple-root coordinates are integers.

noncomputable def TauCeti.IntegralLattice.typeASimpleRootBasis (n : ℕ) : Module.Basis (Fin n) ℤ ↥(typeARootLattice n).carrier

The simple roots, as a ℤ-basis of the type Aₙ root lattice.

@[simp]

theorem TauCeti.IntegralLattice.coe_typeASimpleRootBasis_apply (n : ℕ) (i : Fin n) : ↑((typeASimpleRootBasis n) i) = typeASimpleRoot n i

@[simp]

theorem TauCeti.IntegralLattice.gramMatrix_typeASimpleRootBasis (n : ℕ) : (typeARootLattice n).gramMatrix (typeASimpleRootBasis n) = CartanMatrix.A n

The Gram matrix of the type Aₙ root lattice in its simple-root basis is CartanMatrix.A n.

instance TauCeti.IntegralLattice.instIsNondegenerateTypeARootLattice (n : ℕ) : (typeARootLattice n).IsNondegenerate

theorem TauCeti.IntegralLattice.isEven_typeARootLattice (n : ℕ) : (typeARootLattice n).IsEven

The type Aₙ root lattice is even: every diagonal Cartan entry is 2.

@[simp]

theorem TauCeti.IntegralLattice.determinant_typeARootLattice (n : ℕ) : (typeARootLattice n).determinant = ↑n + 1

The determinant of the type Aₙ root lattice is n + 1.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_typeARootLattice (n : ℕ) : (typeARootLattice n).discriminant = n + 1

The discriminant of the type Aₙ root lattice is n + 1.

@[simp]

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_typeARootLattice (n : ℕ) : Nat.card (typeARootLattice n).DiscriminantGroup = n + 1

The discriminant group of the type Aₙ root lattice has order n + 1.

@[simp]

theorem TauCeti.IntegralLattice.minimum_typeARootLattice (n : ℕ) (hn : n ≠ 0) : (typeARootLattice n).minimum = 2

For n ≥ 1 the minimum of the type Aₙ root lattice is 2: the lattice is even, and a simple root has norm 2.

The first fundamental weight

noncomputable def TauCeti.IntegralLattice.typeAFundamentalWeight (n : ℕ) : Fin n → ℚ

The first fundamental weight of type Aₙ, in simple-root coordinates: ω₁ = ∑ⱼ ((n - j) / (n + 1)) αⱼ.

@[simp]

theorem TauCeti.IntegralLattice.typeAFundamentalWeight_apply (n : ℕ) (j : Fin n) : typeAFundamentalWeight n j = (↑n - ↑↑j) / (↑n + 1)

@[simp]

theorem TauCeti.IntegralLattice.form_typeAFundamentalWeight_simpleRoot (n : ℕ) (i : Fin n) : ((typeARootLattice n).form (typeAFundamentalWeight n)) (typeASimpleRoot n i) = if ↑i = 0 then 1 else 0

The first fundamental weight pairs to 1 with the first simple root and to 0 with the others.

@[simp]

theorem TauCeti.IntegralLattice.form_typeAFundamentalWeight_self (n : ℕ) : ((typeARootLattice n).form (typeAFundamentalWeight n)) (typeAFundamentalWeight n) = ↑n / (↑n + 1)

The self-pairing of the first fundamental weight is n / (n + 1).

The discriminant group

theorem TauCeti.IntegralLattice.typeAFundamentalWeight_mem_dualCarrier (n : ℕ) : typeAFundamentalWeight n ∈ (typeARootLattice n).dualCarrier

The first fundamental weight lies in the dual lattice: it pairs integrally with every simple root, hence with the whole lattice.

noncomputable def TauCeti.IntegralLattice.typeAFundamentalWeightDual (n : ℕ) : ↥(typeARootLattice n).dualCarrier

The first fundamental weight, as a vector of the dual lattice.

@[simp]

theorem TauCeti.IntegralLattice.coe_typeAFundamentalWeightDual (n : ℕ) : ↑(typeAFundamentalWeightDual n) = typeAFundamentalWeight n

noncomputable def TauCeti.IntegralLattice.typeAFundamentalWeightClass (n : ℕ) : (typeARootLattice n).DiscriminantGroup

The discriminant class of the first fundamental weight.

@[simp]

theorem TauCeti.IntegralLattice.mk_typeAFundamentalWeightDual (n : ℕ) : Submodule.Quotient.mk (typeAFundamentalWeightDual n) = typeAFundamentalWeightClass n

The class of the chosen dual fundamental weight is the fundamental-weight class.

theorem TauCeti.IntegralLattice.mk_eq_zsmul_typeAFundamentalWeightClass_iff {n : ℕ} (x : ↥(typeARootLattice n).dualCarrier) (k : ℤ) : Submodule.Quotient.mk x = k • typeAFundamentalWeightClass n ↔ ↑x - k • typeAFundamentalWeight n ∈ (typeARootLattice n).carrier

A dual vector lies in the class k ω₁ exactly when it differs from k ω₁ by a vector of the root lattice.

theorem TauCeti.IntegralLattice.zsmul_typeAFundamentalWeightClass_eq_zero_iff (n : ℕ) (k : ℤ) : k • typeAFundamentalWeightClass n = 0 ↔ ↑n + 1 ∣ k

An integer multiple of the first fundamental weight lies in the root lattice exactly when n + 1 divides it. For n > 0, this is forced by the last simple-root coordinate 1 / (n + 1) of ω₁; at rank zero, the result is trivial.

@[simp]

theorem TauCeti.IntegralLattice.addOrderOf_typeAFundamentalWeightClass (n : ℕ) : addOrderOf (typeAFundamentalWeightClass n) = n + 1

The class of the first fundamental weight has additive order n + 1.

theorem TauCeti.IntegralLattice.zmultiples_typeAFundamentalWeightClass (n : ℕ) : AddSubgroup.zmultiples (typeAFundamentalWeightClass n) = ⊤

The class of the first fundamental weight generates the discriminant group.

noncomputable def TauCeti.IntegralLattice.typeADiscriminantGroupEquiv (n : ℕ) : ZMod (n + 1) ≃+ (typeARootLattice n).DiscriminantGroup

The discriminant group of the type Aₙ root lattice is cyclic of order n + 1, with the class of the first fundamental weight as the image of 1.

@[simp]

theorem TauCeti.IntegralLattice.typeADiscriminantGroupEquiv_apply_one (n : ℕ) : (typeADiscriminantGroupEquiv n) 1 = typeAFundamentalWeightClass n

theorem TauCeti.IntegralLattice.typeADiscriminantGroupEquiv_apply (n : ℕ) (a : ZMod (n + 1)) : (typeADiscriminantGroupEquiv n) a = a.val • typeAFundamentalWeightClass n

The label a : ZMod (n + 1) names the class a.val • ω₁.

The discriminant form on every class

The class of ω₁ generates, so the two computations below give the discriminant form on the whole of A_{Aₙ} rather than only on the generator.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_zsmul_typeAFundamentalWeightClass (n : ℕ) (k : ℤ) : ((typeARootLattice n).discriminantQuadraticMap ⋯) (k • typeAFundamentalWeightClass n) = ↑(↑k * ↑k * ↑n / (2 * (↑n + 1)))

The discriminant quadratic value of the k-th multiple of the class of ω₁ is k² n / (2 (n + 1)).

theorem TauCeti.IntegralLattice.discriminantPairing_zsmul_typeAFundamentalWeightClass (n : ℕ) (j k : ℤ) : ((typeARootLattice n).discriminantPairing (j • typeAFundamentalWeightClass n)) (k • typeAFundamentalWeightClass n) = ↑(↑j * ↑k * ↑n / (↑n + 1))

The discriminant pairing of the j-th and k-th multiples of the class of ω₁ is j k n / (n + 1).

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_typeAFundamentalWeightClass (n : ℕ) : ((typeARootLattice n).discriminantQuadraticMap ⋯) (typeAFundamentalWeightClass n) = ↑(↑n / (2 * (↑n + 1)))

The discriminant quadratic value of the first fundamental weight is n / (2 (n + 1)), in the half-norm convention.

@[simp]

theorem TauCeti.IntegralLattice.discriminantPairing_typeAFundamentalWeightClass (n : ℕ) : ((typeARootLattice n).discriminantPairing (typeAFundamentalWeightClass n)) (typeAFundamentalWeightClass n) = ↑(↑n / (↑n + 1))

The discriminant bilinear value of the first fundamental weight is n / (n + 1), which is twice the half-norm value, as the polar identity demands.

The cyclic model of the discriminant quadratic module

noncomputable def TauCeti.IntegralLattice.typeAStandardQuadraticModule (n : ℕ) : FiniteQuadraticModule

The cyclic ℤ/(n+1) model of the type Aₙ discriminant form: the generator carries the half-norm value n / (2 (n + 1)) of the first fundamental weight.

@[simp]

theorem TauCeti.IntegralLattice.typeAStandardQuadraticModule_quadratic_intCast (n : ℕ) (k : ℤ) : (typeAStandardQuadraticModule n).quadratic ↑k = ↑(↑k * ↑k * ↑n / (2 * (↑n + 1)))

The quadratic value on the reduction of any integer in the cyclic model.

@[simp]

theorem TauCeti.IntegralLattice.typeAStandardQuadraticModule_pairing_intCast (n : ℕ) (j k : ℤ) : ((typeAStandardQuadraticModule n).pairing ↑j) ↑k = ↑(↑j * ↑k * ↑n / (↑n + 1))

The pairing on the reductions of any two integers in the cyclic model.

noncomputable def TauCeti.IntegralLattice.typeAOneZModStandardIsometry : (typeAStandardQuadraticModule 1).Isometry (FiniteQuadraticModule.zmodStandard 2 ⋯)

The standard A₁ discriminant module is the binary standard quadratic alphabet, by the identity on its carrier ZMod 2. Both use the half-norm convention q(a) = a² / 4.

@[simp]

theorem TauCeti.IntegralLattice.typeAOneZModStandardIsometry_apply (a : ZMod 2) : typeAOneZModStandardIsometry a = a

The binary comparison preserves the residue label.

@[simp]

theorem TauCeti.IntegralLattice.typeAOneZModStandardIsometry_symm_apply (a : ZMod 2) : (QuadraticMap.IsometryEquiv.symm typeAOneZModStandardIsometry) a = a

The inverse binary comparison preserves the residue label.

theorem TauCeti.IntegralLattice.typeAOneZModStandardIsometry_toAddEquiv : typeAOneZModStandardIsometry.toAddEquiv = AddEquiv.refl (ZMod 2)

The additive equivalence underlying the binary comparison is the identity.

theorem TauCeti.IntegralLattice.typeAStandardQuadraticModule_one_quadratic (a : ZMod 2) : (typeAStandardQuadraticModule 1).quadratic a = ↑(↑a.val / 4)

In the standard A₁ discriminant alphabet, a residue has quadratic value one quarter of its canonical representative.

@[simp]

theorem TauCeti.IntegralLattice.typeAStandardQuadraticModule_two_quadratic (a : ZMod 3) : (typeAStandardQuadraticModule 2).quadratic a = ↑((if a ≠ 0 then 1 else 0) / 3)

In the standard A₂ discriminant module, the quadratic value of a symbol is 0 at zero and 1/3 at either nonzero symbol.

@[simp]

theorem TauCeti.IntegralLattice.typeAStandardQuadraticModule_two_pairing (a b : ZMod 3) : ((typeAStandardQuadraticModule 2).pairing a) b = ↑(2 * ↑a.val * ↑b.val / 3)

The polar pairing of arbitrary symbols in the A₂ discriminant form is 2ab/3, using their canonical representatives in {0, 1, 2}.

@[simp]

theorem TauCeti.IntegralLattice.typeAStandardQuadraticModule_quadratic_one (n : ℕ) : (typeAStandardQuadraticModule n).quadratic 1 = ↑(↑n / (2 * (↑n + 1)))

The generator of the cyclic model has quadratic value n / (2 (n + 1)).

@[simp]

theorem TauCeti.IntegralLattice.typeAStandardQuadraticModule_pairing_one_one (n : ℕ) : ((typeAStandardQuadraticModule n).pairing 1) 1 = ↑(↑n / (↑n + 1))

The generator of the cyclic model has self-pairing n / (n + 1).

noncomputable def TauCeti.IntegralLattice.typeADiscriminantQuadraticIsometry (n : ℕ) : (typeAStandardQuadraticModule n).Isometry ((typeARootLattice n).discriminantQuadraticModule ⋯)

The cyclic model is isometric to the discriminant quadratic module of the type Aₙ root lattice, by the identification carrying 1 to the class of the first fundamental weight.

This is the Aₙ row of the ADE table: not only is the discriminant group cyclic of order n + 1, its quadratic form is the displayed one. A single generator value suffices, because an additive equivalence out of a cyclic group is determined by the image of its generator.

@[simp]

theorem TauCeti.IntegralLattice.typeADiscriminantQuadraticIsometry_toAddEquiv (n : ℕ) : (typeADiscriminantQuadraticIsometry n).toAddEquiv = typeADiscriminantGroupEquiv n

The underlying additive equivalence of the type-Aₙ quadratic isometry.

@[simp]

theorem TauCeti.IntegralLattice.typeADiscriminantQuadraticIsometry_apply (n : ℕ) (x : ZMod (n + 1)) : (typeADiscriminantQuadraticIsometry n) x = (typeADiscriminantGroupEquiv n) x

The type-Aₙ quadratic isometry acts through the discriminant-group equivalence.

theorem TauCeti.IntegralLattice.typeADiscriminantQuadraticIsometry_one (n : ℕ) : (typeADiscriminantQuadraticIsometry n) 1 = typeAFundamentalWeightClass n

The type-Aₙ quadratic isometry carries the generator of ℤ/(n+1) to the class of the first fundamental weight.

theorem TauCeti.IntegralLattice.isNondegenerate_typeAStandardQuadraticModule (n : ℕ) : (typeAStandardQuadraticModule n).IsNondegenerate

The cyclic ℤ/(n+1) model is nondegenerate.