Reflections in roots of integral lattices

A lattice vector of norm two defines a lattice isometry by sₓ(y) = y - B(x, y) • x. Integrality of the pairing ensures that this reflection preserves the integral carrier, and its involutivity makes carrier preservation an equality. These isometries generate the Weyl group TauCeti.IntegralLattice.weylGroup of the lattice, a normal subgroup of its isometry group; comparing the two groups is how root systems enter the study of lattice automorphisms.

The construction works for indefinite and degenerate lattices as well as positive definite ones. We give its ambient and integral action, involutivity, fixed-vector criterion, and transport under lattice isometries. In particular, conjugation carries a root reflection to the reflection in the image root.

The underlying linear equivalence is Mathlib's Module.reflection; preservation of the bilinear form uses LinearMap.IsReflective.isOrthogonal_reflection.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §8.
• W. Ebeling, Lattices and Codes, Chapter 1.

noncomputable def TauCeti.IntegralLattice.rootReflection {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : L.Isometry L

Reflection in an integral vector of norm two, as an automorphism of the lattice.

theorem TauCeti.IntegralLattice.rootReflection_carrierEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : (rootReflection x hx).carrierEquiv = Module.reflection ⋯

The carrier equivalence is the integral module reflection in the root.

theorem TauCeti.IntegralLattice.rootReflection_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) (y : V) : (rootReflection x hx) y = y - (L.form ↑x) y • ↑x

On the rational ambient space, reflection in a root has no denominator.

@[simp]

theorem TauCeti.IntegralLattice.rootReflection_carrierEquiv_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) (y : ↥L.carrier) : (rootReflection x hx).carrierEquiv y = y - (L.integralForm x) y • x

On the integral carrier, the reflection uses the integral pairing as its coefficient.

@[simp]

theorem TauCeti.IntegralLattice.det_rootReflection {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : (Isometry.det L) (rootReflection x hx) = -1

Every root reflection has determinant minus one.

@[simp]

theorem TauCeti.IntegralLattice.rootReflection_apply_self {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : (rootReflection x hx) ↑x = -↑x

Reflection sends its defining root to its negative.

@[simp]

theorem TauCeti.IntegralLattice.rootReflection_mul_self {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : rootReflection x hx * rootReflection x hx = 1

Reflection in a root is an involution in the lattice isometry group.

@[simp]

theorem TauCeti.IntegralLattice.rootReflection_inv {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : (rootReflection x hx)⁻¹ = rootReflection x hx

The inverse of a root reflection is itself.

@[simp]

theorem TauCeti.IntegralLattice.rootReflection_neg {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : rootReflection (-x) ⋯ = rootReflection x hx

Opposite roots define the same reflection.

@[simp]

theorem TauCeti.IntegralLattice.rootReflection_apply_eq_self_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) (y : V) : (rootReflection x hx) y = y ↔ (L.form ↑x) y = 0

A root reflection fixes exactly the vectors orthogonal to its root.

theorem TauCeti.IntegralLattice.Isometry.map_rootReflection {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : ↥L.carrier) (hx : L.integralNorm x = 2) (y : V) : e ((rootReflection x hx) y) = (rootReflection (e.carrierEquiv x) ⋯) (e y)

Lattice isometries intertwine the reflections in a root and in its image.

theorem TauCeti.IntegralLattice.Isometry.mul_rootReflection_mul_inv {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (e : L.Isometry L) (x : ↥L.carrier) (hx : L.integralNorm x = 2) : e * rootReflection x hx * e⁻¹ = rootReflection (e.carrierEquiv x) ⋯

Conjugation by a lattice automorphism carries root reflections to root reflections.

def TauCeti.IntegralLattice.weylGroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Subgroup (L.Isometry L)

The Weyl group of an integral lattice: the subgroup of its isometry group generated by the reflections in its roots, the lattice vectors of norm two.

theorem TauCeti.IntegralLattice.weylGroup_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.weylGroup = Subgroup.closure {g : L.Isometry L | ∃ (x : ↥L.carrier) (hx : L.integralNorm x = 2), rootReflection x hx = g}

The Weyl group is generated by the root reflections.

theorem TauCeti.IntegralLattice.rootReflection_mem_weylGroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (x : ↥L.carrier) (hx : L.integralNorm x = 2) : rootReflection x hx ∈ L.weylGroup

Every root reflection lies in the Weyl group.

theorem TauCeti.IntegralLattice.weylGroup_le_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {H : Subgroup (L.Isometry L)} : L.weylGroup ≤ H ↔ ∀ (x : ↥L.carrier) (hx : L.integralNorm x = 2), rootReflection x hx ∈ H

The Weyl group is the smallest subgroup containing every root reflection.

instance TauCeti.IntegralLattice.weylGroup_normal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} : L.weylGroup.Normal

The Weyl group is normal in the isometry group, since conjugating a root reflection by an isometry gives the reflection in the image root.