Scaling and negating integral lattices

Multiplying the form of an integral lattice by an integer leaves its carrier fixed and preserves integrality. This file equips integral lattices with that scalar action and computes the induced integral form, Gram matrix, determinant, discriminant, radical, and signature. Positive scaling preserves the positive and negative indices of inertia, while negative scaling exchanges them; negating the form is the special case -1.

The scalar is integral because arbitrary rational scaling need not preserve an integral form. A later development may admit rational scalars together with the necessary integrality hypothesis; the canonical operation internal to integral lattices is the integer action defined here.

Main definitions and results

• TauCeti.IntegralLattice.scale: multiply the rational form by an integer while keeping the carrier fixed.
• TauCeti.IntegralLattice.instMulActionInt: the integer multiplicative action on integral lattices.
• TauCeti.IntegralLattice.instInvolutiveNeg: form negation, defined as scaling by -1.
• TauCeti.IntegralLattice.isEven_neg_iff: form negation preserves evenness.
• TauCeti.IntegralLattice.gramMatrix_smul: scaling multiplies every Gram-matrix entry.
• TauCeti.IntegralLattice.determinant_smul: the determinant is multiplied by the scalar to the lattice rank.
• TauCeti.IntegralLattice.discriminant_smul: the discriminant is multiplied by the absolute scalar to the lattice rank.
• TauCeti.IntegralLattice.signature_smul_of_pos and TauCeti.IntegralLattice.signature_smul_of_neg: scaling preserves or exchanges the two non-null indices according to the sign.
• TauCeti.IntegralLattice.discriminant_neg: form negation preserves the discriminant.
• TauCeti.IntegralLattice.signature_neg: form negation exchanges the positive and negative indices and preserves the null index.

References

• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layer 1, form scaling and negation.

Integer scaling

@[reducible]

def TauCeti.IntegralLattice.scale {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : IntegralLattice V

Scale the form of an integral lattice by an integer, leaving its carrier unchanged.

Integer scaling preserves integrality because an integer multiple of every integral pairing is again integral. The scalar acts on the rational form through the canonical map ℤ → ℚ.

The definition is marked @[reducible] because the carriers (scale n L).carrier and L.carrier are definitionally equal, so a Basis ι ℤ L is definitionally a Basis ι ℤ (scale n L) and instance search requires reducible unfolding to elaborate statements without boilerplate transports.

Equations

• TauCeti.IntegralLattice.scale n L = { carrier := L.carrier, form := ↑n • L.form, isLattice := ⋯, isSymm := ⋯, le_dual := ⋯ }

@[instance_reducible]

instance TauCeti.IntegralLattice.instMulActionInt {V : Type u} [AddCommGroup V] [Module ℚ V] : MulAction ℤ (IntegralLattice V)

Integral lattices carry the canonical multiplicative action which scales their forms by integers.

Equations

• TauCeti.IntegralLattice.instMulActionInt = { smul := TauCeti.IntegralLattice.scale, mul_smul := ⋯, one_smul := ⋯ }

theorem TauCeti.IntegralLattice.smul_def {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : n • L = scale n L

Definitional bridge between scalar multiplication and scale.

@[simp]

theorem TauCeti.IntegralLattice.smul_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : (n • L).carrier = L.carrier

@[simp]

theorem TauCeti.IntegralLattice.smul_form {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : (n • L).form = ↑n • L.form

@[simp]

theorem TauCeti.IntegralLattice.finrank_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : Module.finrank ℤ ↥(n • L).carrier = Module.finrank ℤ ↥L.carrier

Scaling the form does not change the rank of the carrier.

theorem TauCeti.IntegralLattice.integralForm_smul_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) (x y : ↥L.carrier) : ((n • L).integralForm x) y = n * (L.integralForm x) y

The integral form of a scaled lattice is the corresponding integer multiple of the original integral form.

@[simp]

theorem TauCeti.IntegralLattice.integralForm_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : (n • L).integralForm = n • L.integralForm

Scaling commutes with the construction of the restricted integral form.

Gram matrices and invariants

@[simp]

theorem TauCeti.IntegralLattice.gramMatrix_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) {ι : Type v} (e : Module.Basis ι ℤ ↥L.carrier) : (n • L).gramMatrix e = n • L.gramMatrix e

Scaling a lattice multiplies every entry of every Gram matrix by the scalar.

@[simp]

theorem TauCeti.IntegralLattice.gramDet_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : (n • L).gramDet e = n ^ Fintype.card ι * L.gramDet e

The Gram determinant of a scaled lattice is multiplied by the scalar to the size of the basis.

@[simp]

theorem TauCeti.IntegralLattice.determinant_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : (n • L).determinant = n ^ Module.finrank ℤ ↥L.carrier * L.determinant

Scaling multiplies the signed determinant by the scalar to the rank of the lattice.

theorem TauCeti.IntegralLattice.nondegenerate_smul_iff {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : n ≠ 0) (L : IntegralLattice V) : (n • L).form.Nondegenerate ↔ L.form.Nondegenerate

Scaling by a nonzero integer preserves nondegeneracy of the rational form.

This is a named API lemma rather than a simp lemma: simplification already derives it from smul_form and the corresponding bilinear-form result.

Radical and signature

@[simp]

theorem TauCeti.IntegralLattice.radical_smul {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : n ≠ 0) (L : IntegralLattice V) : (n • L).radical = L.radical

Scaling by a nonzero integer preserves the radical.

@[simp]

theorem TauCeti.IntegralLattice.sigNull_smul {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : n ≠ 0) (L : IntegralLattice V) : (n • L).sigNull = L.sigNull

Scaling by a nonzero integer preserves the null index.

@[simp]

theorem TauCeti.IntegralLattice.sigPos_smul_of_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : 0 < n) (L : IntegralLattice V) : (n • L).sigPos = L.sigPos

Scaling by a positive integer preserves the positive index.

@[simp]

theorem TauCeti.IntegralLattice.sigNeg_smul_of_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : 0 < n) (L : IntegralLattice V) : (n • L).sigNeg = L.sigNeg

Scaling by a positive integer preserves the negative index.

@[simp]

theorem TauCeti.IntegralLattice.signature_smul_of_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : 0 < n) (L : IntegralLattice V) : (n • L).signature = L.signature

Scaling by a positive integer preserves the signature.

@[simp]

theorem TauCeti.IntegralLattice.sigPos_smul_of_neg {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : n < 0) (L : IntegralLattice V) : (n • L).sigPos = L.sigNeg

Scaling by a negative integer exchanges the positive and negative indices.

@[simp]

theorem TauCeti.IntegralLattice.sigNeg_smul_of_neg {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : n < 0) (L : IntegralLattice V) : (n • L).sigNeg = L.sigPos

Scaling by a negative integer exchanges the negative and positive indices.

@[simp]

theorem TauCeti.IntegralLattice.signature_smul_of_neg {V : Type u} [AddCommGroup V] [Module ℚ V] {n : ℤ} (hn : n < 0) (L : IntegralLattice V) : (n • L).signature = (L.sigNeg, L.sigNull, L.sigPos)

Scaling by a negative integer exchanges the positive and negative indices and preserves the null index.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_smul {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (L : IntegralLattice V) : (n • L).discriminant = n.natAbs ^ Module.finrank ℤ ↥L.carrier * L.discriminant

Scaling multiplies the discriminant by the absolute scalar to the rank of the lattice.

Form negation

@[instance_reducible]

instance TauCeti.IntegralLattice.instInvolutiveNeg {V : Type u} [AddCommGroup V] [Module ℚ V] : InvolutiveNeg (IntegralLattice V)

Negating an integral lattice negates its form and leaves its carrier fixed.

Equations

• TauCeti.IntegralLattice.instInvolutiveNeg = { neg := fun (L : TauCeti.IntegralLattice V) => -1 • L, neg_neg := ⋯ }

theorem TauCeti.IntegralLattice.neg_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : -L = -1 • L

Definitional bridge between negation and scaling by -1.

@[simp]

theorem TauCeti.IntegralLattice.neg_carrier {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).carrier = L.carrier

@[simp]

theorem TauCeti.IntegralLattice.neg_form {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).form = -L.form

@[simp]

theorem TauCeti.IntegralLattice.finrank_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Module.finrank ℤ ↥(-L).carrier = Module.finrank ℤ ↥L.carrier

Negating the form does not change the rank of the carrier.

theorem TauCeti.IntegralLattice.integralForm_neg_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : ↥L.carrier) : ((-L).integralForm x) y = -(L.integralForm x) y

The integral form of the negated lattice is the negative of the original integral form.

@[simp]

theorem TauCeti.IntegralLattice.integralForm_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).integralForm = -L.integralForm

Form negation commutes with the construction of the restricted integral form.

@[simp]

theorem TauCeti.IntegralLattice.isEven_neg_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).IsEven ↔ L.IsEven

An integral lattice is even if and only if its form negation is even.

@[simp]

theorem TauCeti.IntegralLattice.gramMatrix_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} (e : Module.Basis ι ℤ ↥L.carrier) : (-L).gramMatrix e = -L.gramMatrix e

Negation multiplies every Gram-matrix entry by -1.

@[simp]

theorem TauCeti.IntegralLattice.gramDet_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {ι : Type v} [Fintype ι] [DecidableEq ι] (e : Module.Basis ι ℤ ↥L.carrier) : (-L).gramDet e = (-1) ^ Fintype.card ι * L.gramDet e

Negating the form multiplies a Gram determinant by (-1) to the size of its basis.

@[simp]

theorem TauCeti.IntegralLattice.determinant_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).determinant = (-1) ^ Module.finrank ℤ ↥L.carrier * L.determinant

Negating the form multiplies the signed determinant by (-1) to the lattice rank.

theorem TauCeti.IntegralLattice.nondegenerate_neg_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).form.Nondegenerate ↔ L.form.Nondegenerate

Form negation preserves nondegeneracy.

This is a named API lemma rather than a simp lemma: simplification already derives it from neg_form and the corresponding bilinear-form result.

instance TauCeti.IntegralLattice.instIsNondegenerateNeg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : (-L).IsNondegenerate

Negating the form of a nondegenerate integral lattice preserves nondegeneracy.

@[simp]

theorem TauCeti.IntegralLattice.radical_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).radical = L.radical

Form negation preserves the radical.

@[simp]

theorem TauCeti.IntegralLattice.sigNull_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).sigNull = L.sigNull

Form negation preserves the null index.

@[simp]

theorem TauCeti.IntegralLattice.sigPos_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).sigPos = L.sigNeg

Form negation exchanges the positive and negative indices.

@[simp]

theorem TauCeti.IntegralLattice.sigNeg_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).sigNeg = L.sigPos

Form negation exchanges the negative and positive indices.

@[simp]

theorem TauCeti.IntegralLattice.signature_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).signature = (L.sigNeg, L.sigNull, L.sigPos)

Form negation exchanges the positive and negative indices and preserves the null index.

@[simp]

theorem TauCeti.IntegralLattice.discriminant_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).discriminant = L.discriminant

Form negation preserves the nonnegative discriminant.

Interaction with constructors

@[simp]

theorem TauCeti.IntegralLattice.smul_ofSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) (S : Submodule ℤ V) [hS : Submodule.IsLattice ℚ S] (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hle : S ≤ B.dualSubmodule S) : n • ofSubmodule S B hB hle = ofSubmodule S (↑n • B) ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.neg_ofSubmodule {V : Type u} [AddCommGroup V] [Module ℚ V] (S : Submodule ℤ V) [hS : Submodule.IsLattice ℚ S] (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hle : S ≤ B.dualSubmodule S) : -ofSubmodule S B hB hle = ofSubmodule S (-B) ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.smul_ofBasis {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) : n • ofBasis b B hB hint = ofBasis b (↑n • B) ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.neg_ofBasis {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Finite ι] (b : Module.Basis ι ℚ V) (B : LinearMap.BilinForm ℚ V) (hB : B.IsSymm) (hint : ∀ (i j : ι), (B (b i)) (b j) ∈ 1) : -ofBasis b B hB hint = ofBasis b (-B) ⋯ ⋯

@[simp]

theorem TauCeti.IntegralLattice.smul_ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] (n : ℤ) {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : n • ofGramMatrix b G hG = ofGramMatrix b (n • G) ⋯

@[simp]

theorem TauCeti.IntegralLattice.neg_ofGramMatrix {V : Type u} [AddCommGroup V] [Module ℚ V] {ι : Type u_1} [Fintype ι] (b : Module.Basis ι ℚ V) (G : Matrix ι ι ℤ) (hG : G.IsSymm) : -ofGramMatrix b G hG = ofGramMatrix b (-G) ⋯