Discriminant forms under orthogonal sums and negation

The dual carrier of an orthogonal sum is the product of the two dual carriers. Passing the embedded original carriers through this equivalence and then quotienting gives the canonical equivalence

A_(L ⊥ M) ≃ A_L × A_M.

This file proves that the equivalence is an isometry for both discriminant pairings and, when the lattices are even, their half-norm quadratic forms. It also identifies the discriminant form of the form-negated lattice -L: the quotient group is unchanged, while both its bilinear and quadratic forms are negated.

Main declarations

• TauCeti.IntegralLattice.discriminantGroupOrthogonalSumEquiv: the discriminant group of an orthogonal sum is the product of the discriminant groups.
• TauCeti.IntegralLattice.discriminantBilinearIsometryOrthogonalSum: the preceding equivalence preserves the product discriminant pairing.
• TauCeti.IntegralLattice.discriminantQuadraticIsometryOrthogonalSum: the corresponding isometry of half-norm discriminant quadratic modules.
• TauCeti.IntegralLattice.discriminantBilinearIsometryNeg and TauCeti.IntegralLattice.discriminantQuadraticIsometryNeg: form negation negates the discriminant pairing and quadratic map.

References

• V. V. Nikulin, Integral symmetric bilinear forms and some of their applications, §1.1.
• W. Ebeling, Lattices and Codes, Chapter 1.
• TauCetiRoadmap/IntegralLattices/README.md, Layers 2 and 3.

Orthogonal sums

theorem TauCeti.IntegralLattice.mem_dualCarrier_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (x : V × W) : x ∈ (L.orthogonalSum M).dualCarrier ↔ x.1 ∈ L.dualCarrier ∧ x.2 ∈ M.dualCarrier

Membership in the dual carrier of an orthogonal sum is componentwise membership in the two dual carriers.

@[simp]

theorem TauCeti.IntegralLattice.dualCarrier_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) : (L.orthogonalSum M).dualCarrier = L.dualCarrier.prod M.dualCarrier

The dual carrier of an orthogonal sum is the product of the two dual carriers.

def TauCeti.IntegralLattice.orthogonalSumDualCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) : ↥(L.orthogonalSum M).dualCarrier ≃ₗ[ℤ] ↥L.dualCarrier × ↥M.dualCarrier

The dual carrier of an orthogonal sum is canonically the product of the dual carriers.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.IntegralLattice.orthogonalSumDualCarrierEquiv_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (x : ↥(L.orthogonalSum M).dualCarrier) : (L.orthogonalSumDualCarrierEquiv M) x = (⟨(↑x).1, ⋯⟩, ⟨(↑x).2, ⋯⟩)

The dual-carrier product equivalence acts by taking the two ambient coordinates.

@[simp]

theorem TauCeti.IntegralLattice.coe_orthogonalSumDualCarrierEquiv_symm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (x : ↥L.dualCarrier × ↥M.dualCarrier) : ↑((L.orthogonalSumDualCarrierEquiv M).symm x) = (↑x.1, ↑x.2)

The inverse dual-carrier product equivalence acts by assembling the two ambient coordinates.

theorem TauCeti.IntegralLattice.map_carrierInDual_orthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) : Submodule.map (↑(L.orthogonalSumDualCarrierEquiv M)) (L.orthogonalSum M).carrierInDual = L.carrierInDual.prod M.carrierInDual

Under the dual-carrier product equivalence, the embedded carrier of an orthogonal sum is the product of the two embedded carriers.

def TauCeti.IntegralLattice.discriminantGroupOrthogonalSumEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) : (L.orthogonalSum M).DiscriminantGroup ≃ₗ[ℤ] L.DiscriminantGroup × M.DiscriminantGroup

The discriminant group of an orthogonal sum is canonically the product of the discriminant groups of its summands.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.IntegralLattice.discriminantGroupOrthogonalSumEquiv_mk {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) (x : ↥(L.orthogonalSum M).dualCarrier) : (L.discriminantGroupOrthogonalSumEquiv M) (Submodule.Quotient.mk x) = (Submodule.Quotient.mk ((L.orthogonalSumDualCarrierEquiv M) x).1, Submodule.Quotient.mk ((L.orthogonalSumDualCarrierEquiv M) x).2)

The orthogonal-sum discriminant-group equivalence maps a representative to the pair of its component classes.

noncomputable def TauCeti.IntegralLattice.discriminantBilinearIsometryOrthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] : (L.orthogonalSum M).discriminantBilinearModule.Isometry (L.discriminantBilinearModule.prod M.discriminantBilinearModule)

The product equivalence of discriminant groups is an isometry from the discriminant pairing of an orthogonal sum to the orthogonal product of the two discriminant pairings.

Equations

• L.discriminantBilinearIsometryOrthogonalSum M = { toAddEquiv := (L.discriminantGroupOrthogonalSumEquiv M).toAddEquiv, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryOrthogonalSum_toAddEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] : (L.discriminantBilinearIsometryOrthogonalSum M).toAddEquiv = (L.discriminantGroupOrthogonalSumEquiv M).toAddEquiv

The underlying additive equivalence of the orthogonal-sum discriminant-bilinear isometry is the canonical product equivalence of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryOrthogonalSum_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] (x : (L.orthogonalSum M).DiscriminantGroup) : (L.discriminantBilinearIsometryOrthogonalSum M) x = (L.discriminantGroupOrthogonalSumEquiv M) x

The orthogonal-sum discriminant-bilinear isometry acts through the canonical discriminant-group equivalence.

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryOrthogonalSum_mk {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] (x : ↥(L.orthogonalSum M).dualCarrier) : (L.discriminantBilinearIsometryOrthogonalSum M) (Submodule.Quotient.mk x) = (Submodule.Quotient.mk ((L.orthogonalSumDualCarrierEquiv M) x).1, Submodule.Quotient.mk ((L.orthogonalSumDualCarrierEquiv M) x).2)

The orthogonal-sum discriminant-bilinear isometry maps a representative to the pair of its component classes.

noncomputable def TauCeti.IntegralLattice.discriminantQuadraticIsometryOrthogonalSum {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) (hM : M.IsEven) : ((L.orthogonalSum M).discriminantQuadraticModule ⋯).Isometry ((L.discriminantQuadraticModule hL).prod (M.discriminantQuadraticModule hM))

The product equivalence of discriminant groups is an isometry from the half-norm discriminant quadratic module of an orthogonal sum to the orthogonal product of the two discriminant quadratic modules.

Equations

• L.discriminantQuadraticIsometryOrthogonalSum M hL hM = { toLinearEquiv := L.discriminantGroupOrthogonalSumEquiv M, map_app' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryOrthogonalSum_toAddEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) (hM : M.IsEven) : (L.discriminantQuadraticIsometryOrthogonalSum M hL hM).toAddEquiv = (L.discriminantGroupOrthogonalSumEquiv M).toAddEquiv

The underlying additive equivalence of the orthogonal-sum discriminant-quadratic isometry is the canonical product equivalence of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryOrthogonalSum_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) (hM : M.IsEven) (x : (L.orthogonalSum M).DiscriminantGroup) : (L.discriminantQuadraticIsometryOrthogonalSum M hL hM) x = (L.discriminantGroupOrthogonalSumEquiv M) x

The orthogonal-sum discriminant-quadratic isometry acts through the canonical discriminant-group equivalence.

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryOrthogonalSum_mk {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) (hM : M.IsEven) (x : ↥(L.orthogonalSum M).dualCarrier) : (L.discriminantQuadraticIsometryOrthogonalSum M hL hM) (Submodule.Quotient.mk x) = (Submodule.Quotient.mk ((L.orthogonalSumDualCarrierEquiv M) x).1, Submodule.Quotient.mk ((L.orthogonalSumDualCarrierEquiv M) x).2)

The orthogonal-sum discriminant-quadratic isometry maps a representative to the pair of its component classes.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryOrthogonalSum_toFiniteBilinearModule {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) [L.IsNondegenerate] [M.IsNondegenerate] (hL : L.IsEven) (hM : M.IsEven) : (L.discriminantQuadraticIsometryOrthogonalSum M hL hM).toFiniteBilinearModule = L.discriminantBilinearIsometryOrthogonalSum M

Forgetting the quadratic maps from the orthogonal-sum discriminant isometry recovers the orthogonal-sum discriminant-bilinear isometry.

Form negation

@[simp]

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

Negating a lattice form does not change its dual carrier.

def TauCeti.IntegralLattice.negDualCarrierEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : ↥(-L).dualCarrier ≃ₗ[ℤ] ↥L.dualCarrier

The dual carrier of a form-negated lattice is canonically identified with the original dual carrier by the identity on ambient vectors.

Equations

• L.negDualCarrierEquiv = { toFun := fun (x : ↥(-L).dualCarrier) => ⟨↑x, ⋯⟩, map_add' := ⋯, map_smul' := ⋯, invFun := fun (x : ↥L.dualCarrier) => ⟨↑x, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.coe_negDualCarrierEquiv_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥(-L).dualCarrier) : ↑(L.negDualCarrierEquiv x) = ↑x

The dual-carrier equivalence for form negation is the identity on ambient vectors.

@[simp]

theorem TauCeti.IntegralLattice.coe_negDualCarrierEquiv_symm_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥L.dualCarrier) : ↑(L.negDualCarrierEquiv.symm x) = ↑x

The inverse dual-carrier equivalence for form negation is also the identity on ambient vectors.

theorem TauCeti.IntegralLattice.map_carrierInDual_neg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Submodule.map (↑L.negDualCarrierEquiv) (-L).carrierInDual = L.carrierInDual

Under the dual-carrier equivalence for form negation, the embedded carrier maps to the original embedded carrier.

def TauCeti.IntegralLattice.discriminantGroupNegEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (-L).DiscriminantGroup ≃ₗ[ℤ] L.DiscriminantGroup

Negating a lattice form leaves its discriminant group canonically unchanged.

Equations

• L.discriminantGroupNegEquiv = Submodule.Quotient.equiv (-L).carrierInDual L.carrierInDual L.negDualCarrierEquiv ⋯

@[simp]

theorem TauCeti.IntegralLattice.discriminantGroupNegEquiv_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : ↥(-L).dualCarrier) : L.discriminantGroupNegEquiv (Submodule.Quotient.mk x) = Submodule.Quotient.mk (L.negDualCarrierEquiv x)

The discriminant-group equivalence for form negation maps every representative to the same ambient representative.

noncomputable def TauCeti.IntegralLattice.discriminantBilinearIsometryNeg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : (-L).discriminantBilinearModule.Isometry L.discriminantBilinearModule.neg

The canonical discriminant-group equivalence is an isometry from the discriminant pairing of the form-negated lattice to the negative of the original discriminant pairing.

Equations

• L.discriminantBilinearIsometryNeg = { toAddEquiv := L.discriminantGroupNegEquiv.toAddEquiv, map_pairing' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryNeg_toAddEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] : L.discriminantBilinearIsometryNeg.toAddEquiv = L.discriminantGroupNegEquiv.toAddEquiv

The underlying additive equivalence of the discriminant-bilinear isometry for form negation is the canonical equivalence of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryNeg_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (x : (-L).DiscriminantGroup) : L.discriminantBilinearIsometryNeg x = L.discriminantGroupNegEquiv x

The discriminant-bilinear isometry for form negation acts through the canonical discriminant-group equivalence.

theorem TauCeti.IntegralLattice.discriminantBilinearIsometryNeg_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (x : ↥(-L).dualCarrier) : L.discriminantBilinearIsometryNeg (Submodule.Quotient.mk x) = Submodule.Quotient.mk (L.negDualCarrierEquiv x)

The discriminant-bilinear isometry for form negation maps every representative to the same ambient representative.

noncomputable def TauCeti.IntegralLattice.discriminantQuadraticIsometryNeg {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : ((-L).discriminantQuadraticModule ⋯).Isometry (L.discriminantQuadraticModule hL).neg

The canonical discriminant-group equivalence is an isometry from the half-norm discriminant quadratic module of a form-negated lattice to the negative of the original discriminant quadratic module.

Equations

• L.discriminantQuadraticIsometryNeg hL = { toLinearEquiv := L.discriminantGroupNegEquiv, map_app' := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryNeg_toAddEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticIsometryNeg hL).toAddEquiv = L.discriminantGroupNegEquiv.toAddEquiv

The underlying additive equivalence of the discriminant-quadratic isometry for form negation is the canonical equivalence of discriminant groups.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryNeg_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (x : (-L).DiscriminantGroup) : (L.discriminantQuadraticIsometryNeg hL) x = L.discriminantGroupNegEquiv x

The discriminant-quadratic isometry for form negation acts through the canonical discriminant-group equivalence.

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryNeg_mk {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) (x : ↥(-L).dualCarrier) : (L.discriminantQuadraticIsometryNeg hL) (Submodule.Quotient.mk x) = Submodule.Quotient.mk (L.negDualCarrierEquiv x)

The discriminant-quadratic isometry for form negation maps every representative to the same ambient representative.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticIsometryNeg_toFiniteBilinearModule {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) [L.IsNondegenerate] (hL : L.IsEven) : (L.discriminantQuadraticIsometryNeg hL).toFiniteBilinearModule = L.discriminantBilinearIsometryNeg

Forgetting the quadratic maps from the discriminant isometry for form negation recovers the corresponding discriminant-bilinear isometry.