Rationalizing an integral lattice form

Let L be a full integral lattice in a rational vector space V. The carrier's canonical base-change equivalence identifies V with the scalar extension ℚ ⊗[ℤ] L. This file proves that this equivalence identifies the scalar extension of L.integralForm with the ambient rational form L.form.

Conversely, an integral symmetric form on a finite free ℤ-module M defines an integral lattice in ℚ ⊗[ℤ] M. Its carrier consists exactly of the unit pure tensors 1 ⊗ₜ m, so that TensorProduct.unitTmulEquiv identifies M with it, and its restricted integral form recovers the original form. Base-changing that carrier equivalence and then rationalizing is the identity on ℚ ⊗[ℤ] M; at the level of forms the two models are related by the isometries rationalizationIsometry and carrierIsometry.

Mathlib already supplies LinearMap.BilinForm.baseChange; the point here is to connect that abstract tensor-product construction to the embedded-carrier model used by integral lattices. The lattice ofIntegralForm is built from an arbitrary chosen basis of M, but no choice of basis appears in the resulting equivalences or in the equations characterizing them.

Main results

• TauCeti.IntegralLattice.form_rationalizationEquiv: the base-changed integral form equals the ambient form under the equivalence.
• TauCeti.IntegralLattice.rationalizationIsometry: this equivalence is an isometry from L.integralForm.baseChange ℚ to L.form.
• TauCeti.IntegralLattice.ofIntegralForm: the integral lattice obtained by rationalizing an abstract finite free integral form.
• TauCeti.IntegralLattice.mem_ofIntegralForm_carrier_iff: its carrier consists exactly of the unit pure tensors.
• TauCeti.IntegralLattice.ofIntegralForm.carrierEquiv: the original module identified with the embedded carrier.
• TauCeti.IntegralLattice.ofIntegralForm.carrierIsometry: that equivalence as an isometry of integral forms.
• TauCeti.IntegralLattice.ofIntegralForm.carrierEquiv_baseChange_trans_rationalizationEquiv: base-changing the carrier equivalence and then rationalizing is the identity.

References

This is the rational-extension target in Layer 1 of TauCetiRoadmap/IntegralLattices/README.md. See W. Ebeling, Lattices and Codes, Chapter 1.

@[simp]

theorem TauCeti.IntegralLattice.form_rationalizationEquiv {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x y : TensorProduct ℤ ℚ ↥L.carrier) : (L.form (L.carrier.rationalizationEquiv x)) (L.carrier.rationalizationEquiv y) = ((LinearMap.BilinForm.baseChange ℚ L.integralForm) x) y

The scalar extension of the carrier's integral form is the ambient rational form under the canonical rationalization equivalence.

noncomputable def TauCeti.IntegralLattice.rationalizationIsometry {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (LinearMap.BilinForm.baseChange ℚ L.integralForm).IsometryEquiv L.form

The canonical rationalization is an isometry from the base-changed integral form to the ambient rational form.

@[simp]

theorem TauCeti.IntegralLattice.rationalizationIsometry_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : TensorProduct ℤ ℚ ↥L.carrier) : L.rationalizationIsometry x = L.carrier.rationalizationEquiv x

Evaluating the rationalization isometry on a tensor product element coincides with the rationalization equivalence.

@[simp]

theorem TauCeti.IntegralLattice.rationalizationIsometry_symm_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (y : V) : L.rationalizationIsometry.symm y = L.carrier.rationalizationEquiv.symm y

Evaluating the inverse rationalization isometry coincides with the inverse rationalization equivalence.

noncomputable def TauCeti.IntegralLattice.ofIntegralForm {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) : IntegralLattice (TensorProduct ℤ ℚ M)

Rationalizing an integral symmetric form on a finite free ℤ-module produces an integral lattice in its scalar extension to ℚ.

@[simp]

theorem TauCeti.IntegralLattice.ofIntegralForm_form {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) : (ofIntegralForm B hB).form = LinearMap.BilinForm.baseChange ℚ B

The ambient rational form of a rationalized integral form is the base change to ℚ.

theorem TauCeti.IntegralLattice.ofIntegralForm_carrier {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) : (ofIntegralForm B hB).carrier = ((TensorProduct.mk ℤ ℚ M) 1).range

The carrier of a rationalized integral form is the lattice of unit pure tensors.

@[simp]

theorem TauCeti.IntegralLattice.mem_ofIntegralForm_carrier_iff {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (x : TensorProduct ℤ ℚ M) : x ∈ (ofIntegralForm B hB).carrier ↔ ∃ (m : M), 1 ⊗ₜ[ℤ] m = x

The carrier of a rationalized integral form consists exactly of the unit pure tensors.

noncomputable def TauCeti.IntegralLattice.ofIntegralForm.carrierEquiv {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) : M ≃ₗ[ℤ] ↥(ofIntegralForm B hB).carrier

The abstract integral module is canonically equivalent to the carrier of its rationalized integral lattice: this is TensorProduct.unitTmulEquiv read through ofIntegralForm_carrier.

@[simp]

theorem TauCeti.IntegralLattice.ofIntegralForm.coe_carrierEquiv_apply {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (x : M) : ↑((carrierEquiv B hB) x) = 1 ⊗ₜ[ℤ] x

The carrier equivalence sends an abstract vector to its unit pure tensor.

@[simp]

theorem TauCeti.IntegralLattice.ofIntegralForm.carrierEquiv_symm_tmul {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (x : M) (h : 1 ⊗ₜ[ℤ] x ∈ (ofIntegralForm B hB).carrier) : (carrierEquiv B hB).symm ⟨1 ⊗ₜ[ℤ] x, h⟩ = x

The inverse carrier equivalence recovers an abstract vector from its unit pure tensor.

@[simp]

theorem TauCeti.IntegralLattice.ofIntegralForm.integralForm_carrierEquiv {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (x y : M) : ((ofIntegralForm B hB).integralForm ((carrierEquiv B hB) x)) ((carrierEquiv B hB) y) = (B x) y

Restricting the rationalized form along the carrier equivalence recovers the original integral form.

noncomputable def TauCeti.IntegralLattice.ofIntegralForm.carrierIsometry {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) : B.IsometryEquiv (ofIntegralForm B hB).integralForm

The carrier equivalence is an isometry from the abstract integral form to the restricted form of its rationalized lattice.

@[simp]

theorem TauCeti.IntegralLattice.ofIntegralForm.carrierIsometry_apply {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (x : M) : (carrierIsometry B hB) x = (carrierEquiv B hB) x

The carrier isometry acts through the canonical carrier equivalence.

@[simp]

theorem TauCeti.IntegralLattice.ofIntegralForm.carrierIsometry_symm_apply {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (y : ↥(ofIntegralForm B hB).carrier) : (carrierIsometry B hB).symm y = (carrierEquiv B hB).symm y

Evaluating the inverse carrier isometry coincides with the inverse carrier equivalence.

@[simp]

theorem TauCeti.IntegralLattice.ofIntegralForm.rationalizationEquiv_baseChange_carrierEquiv {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (x : TensorProduct ℤ ℚ M) : (ofIntegralForm B hB).carrier.rationalizationEquiv ((LinearEquiv.baseChange ℤ ℚ M (↥(ofIntegralForm B hB).carrier) (carrierEquiv B hB)) x) = x

Base-changing the carrier equivalence and then applying the lattice's rationalization equivalence returns the vector one started from.

theorem TauCeti.IntegralLattice.ofIntegralForm.carrierEquiv_baseChange_trans_rationalizationEquiv {M : Type u} [AddCommGroup M] [Module.Free ℤ M] [Module.Finite ℤ M] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) : LinearEquiv.baseChange ℤ ℚ M (↥(ofIntegralForm B hB).carrier) (carrierEquiv B hB) ≪≫ₗ (ofIntegralForm B hB).carrier.rationalizationEquiv = LinearEquiv.refl ℚ (TensorProduct ℤ ℚ M)

The bundled form of rationalizationEquiv_baseChange_carrierEquiv: base-changing the carrier equivalence and then rationalizing is the identity on the original rationalization.