The real model of a positive definite rational lattice

Let M be a positive definite integral lattice in a rational vector space V. Extending scalars to ℝ, the form of M becomes a positive definite symmetric bilinear form on ℝ ⊗[ℚ] V, hence an inner product. The space ℝ ⊗[ℚ] V with this inner product is the Euclidean space TauCeti.IntegralLattice.RealModelSpace, and the image 1 ⊗ M of the carrier is the real model TauCeti.IntegralLattice.realModel of M: a full integral ℤ-lattice in it.

This is the converse of the rational model ZLattice.ratModel of an integral lattice in a real inner product space, and the two constructions are mutually inverse up to isometry:

• the rational model of the real model of M is isometric to M (TauCeti.IntegralLattice.ratModelRealModelIsometry);
• the real model of the rational model of an integral full lattice L ⊆ E is carried onto L by a linear isometry equivalence of its real model space with E (ZLattice.realModelRatModelIsometry).

The rational embedding also identifies the dual carrier with the dual real lattice (realModelDualEquiv) and the discriminant groups (realModelDiscriminantGroupEquiv). The latter preserves the discriminant pairing and, for even lattices, the half-norm quadratic map, read through ZLattice.ratModelDiscriminantGroupEquiv. Thus discriminant-form computations on the rational lattice apply to the real model without introducing another discriminant form.

Moreover a real linear isometry carrying one real model onto another induces an isometry of the rational lattices (TauCeti.IntegralLattice.Isometry.ofRealModel), so that facts proved about isometry classes of rational lattices, such as non-isometry, transfer to the real models.

Main definitions

• TauCeti.IntegralLattice.RealModelSpace M hM: the real inner product space ℝ ⊗[ℚ] V.
• TauCeti.IntegralLattice.realModelMap M hM: the rational embedding V → ℝ ⊗[ℚ] V.
• TauCeti.IntegralLattice.realModel M hM: the real model of M, a full lattice.
• TauCeti.IntegralLattice.realModelCarrierEquiv M hM: the carrier of M is identified with its real model.
• TauCeti.IntegralLattice.ratModelRealModelIsometry M hM: the isometry from M to the rational model of its real model.
• ZLattice.realModelRatModelIsometry hL: the linear isometry from the real model space of the rational model of L onto E.
• TauCeti.IntegralLattice.Isometry.ofRealModel: the isometry of rational lattices induced by an isometry of real models.

Main results

• TauCeti.IntegralLattice.inner_realModelMap: the inner product extends the rational form.
• TauCeti.IntegralLattice.isIntegral_realModel: the real model is an integral lattice.
• TauCeti.IntegralLattice.isEven_realModel_iff and TauCeti.IntegralLattice.isUnimodular_realModel_iff: the real model is even, resp. unimodular, exactly when M is.
• TauCeti.IntegralLattice.RealModelSpace.finrank_eq: the real model space has the rank of M.
• TauCeti.IntegralLattice.det_realModel, TauCeti.IntegralLattice.natCard_discriminantGroup_realModel, and TauCeti.IntegralLattice.IsPosDef.determinant_eq_card_discriminantGroup: the real model has the determinant of M, its discriminant group has the order of that of M, and M.determinant = |M.DiscriminantGroup|.
• ZLattice.map_realModel_realModelRatModelIsometry: the isometry carries the real model of the rational model onto L.
• TauCeti.IntegralLattice.Isometry.realModelMap_ofRealModel_apply: the induced isometry agrees with the real isometry on the rational vectors.
• TauCeti.IntegralLattice.map_realModel_ne_realModel: if two positive definite rational lattices are not isometric, no real linear isometry carries the real model of one onto that of the other.

References

• W. Ebeling, Lattices and Codes, Chapter 1.

def TauCeti.IntegralLattice.RealModelSpace {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (_hM : M.IsPosDef) : Type u_1

The real vector space ℝ ⊗[ℚ] V of a positive definite integral lattice M in V. It carries the inner product extending the form of M (inner_realModelMap).

@[instance_reducible]

noncomputable instance TauCeti.IntegralLattice.RealModelSpace.instAddCommGroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : AddCommGroup (M.RealModelSpace hM)

@[instance_reducible]

noncomputable instance TauCeti.IntegralLattice.RealModelSpace.instModuleReal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : Module ℝ (M.RealModelSpace hM)

@[instance_reducible]

noncomputable instance TauCeti.IntegralLattice.RealModelSpace.instModuleRat {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : Module ℚ (M.RealModelSpace hM)

instance TauCeti.IntegralLattice.RealModelSpace.instIsScalarTowerRatReal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : IsScalarTower ℚ ℝ (M.RealModelSpace hM)

@[instance_reducible]

noncomputable def TauCeti.IntegralLattice.RealModelSpace.core {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : InnerProductSpace.Core ℝ (M.RealModelSpace hM)

The inner product structure on ℝ ⊗[ℚ] V given by the scalar extension of the form of a positive definite lattice.

@[instance_reducible]

noncomputable instance TauCeti.IntegralLattice.RealModelSpace.instNormedAddCommGroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : NormedAddCommGroup (M.RealModelSpace hM)

@[instance_reducible]

noncomputable instance TauCeti.IntegralLattice.RealModelSpace.instInnerProductSpaceReal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : InnerProductSpace ℝ (M.RealModelSpace hM)

theorem TauCeti.IntegralLattice.RealModelSpace.inner_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} (x y : M.RealModelSpace hM) : inner ℝ x y = ((LinearMap.BilinForm.baseChange ℝ M.form) x) y

The inner product of the real model space is the scalar extension of the form.

instance TauCeti.IntegralLattice.RealModelSpace.instFiniteDimensionalReal {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : FiniteDimensional ℝ (M.RealModelSpace hM)

@[simp]

theorem TauCeti.IntegralLattice.RealModelSpace.finrank_eq {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} : Module.finrank ℝ (M.RealModelSpace hM) = Module.finrank ℤ ↥M.carrier

The real model space has the rank of the lattice.

noncomputable def TauCeti.IntegralLattice.realModelMap {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : V →ₗ[ℚ] M.RealModelSpace hM

The rational embedding x ↦ 1 ⊗ x of V into the real model space.

theorem TauCeti.IntegralLattice.realModelMap_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : V) : (M.realModelMap hM) x = 1 ⊗ₜ[ℚ] x

The rational embedding sends x to the pure tensor 1 ⊗ x.

@[simp]

theorem TauCeti.IntegralLattice.inner_realModelMap {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x y : V) : inner ℝ ((M.realModelMap hM) x) ((M.realModelMap hM) y) = ↑((M.form x) y)

The inner product of the real model space extends the rational form of M.

@[simp]

theorem TauCeti.IntegralLattice.norm_sq_realModelMap {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : V) : ‖(M.realModelMap hM) x‖ ^ 2 = ↑(M.norm x)

The squared norm in the real model is the rational lattice norm, cast to ℝ.

theorem TauCeti.IntegralLattice.realModelMap_injective {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : Function.Injective ⇑(M.realModelMap hM)

The rational embedding into the real model space is injective.

noncomputable def TauCeti.IntegralLattice.realModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : Submodule ℤ (M.RealModelSpace hM)

The real model of a positive definite integral lattice M: the image 1 ⊗ M of its carrier in the Euclidean space ℝ ⊗[ℚ] V.

theorem TauCeti.IntegralLattice.mem_realModel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) {y : M.RealModelSpace hM} : y ∈ M.realModel hM ↔ ∃ x ∈ M.carrier, (M.realModelMap hM) x = y

The vectors of the real model are the images 1 ⊗ x of the carrier vectors x.

@[simp]

theorem TauCeti.IntegralLattice.realModelMap_mem_realModel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) {x : V} : (M.realModelMap hM) x ∈ M.realModel hM ↔ x ∈ M.carrier

A rational vector lies in the real model exactly when it lies in the carrier.

instance TauCeti.IntegralLattice.instDiscreteTopologySubtypeRealModelSpaceMemSubmoduleIntRealModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : DiscreteTopology ↥(M.realModel hM)

instance TauCeti.IntegralLattice.instIsZLatticeRealRealModelSpaceRealModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : IsZLattice ℝ (M.realModel hM)

theorem TauCeti.IntegralLattice.isIntegral_realModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : ZLattice.IsIntegral (M.realModel hM)

The real model of a positive definite integral lattice is integral.

noncomputable def TauCeti.IntegralLattice.realModelCarrierEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : ↥M.carrier ≃ₗ[ℤ] ↥(M.realModel hM)

The identification of the carrier of M with its real model, x ↦ 1 ⊗ x.

@[simp]

theorem TauCeti.IntegralLattice.coe_realModelCarrierEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : ↥M.carrier) : ↑((M.realModelCarrierEquiv hM) x) = (M.realModelMap hM) ↑x

The carrier identification sends x to 1 ⊗ x.

@[simp]

theorem TauCeti.IntegralLattice.integralForm_realModelCarrierEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x y : ↥M.carrier) : (⋯.integralForm ((M.realModelCarrierEquiv hM) x)) ((M.realModelCarrierEquiv hM) y) = (M.integralForm x) y

The integer-valued inner product of the real model is the integral form of M.

noncomputable def TauCeti.IntegralLattice.ratModelRealModelIsometry {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : M.Isometry (ZLattice.ratModel ⋯)

A positive definite integral lattice M is isometric to the rational model of its real model: the isometry sends a lattice vector x to 1 ⊗ (1 ⊗ x).

theorem TauCeti.IntegralLattice.ratModelRealModelIsometry_apply_coe {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : ↥M.carrier) : (M.ratModelRealModelIsometry hM) ↑x = 1 ⊗ₜ[ℤ] (M.realModelCarrierEquiv hM) x

The isometry from M to the rational model of its real model sends a lattice vector to the unit pure tensor of its image in the real model.

theorem TauCeti.IntegralLattice.isEven_realModel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : ZLattice.IsEven (M.realModel hM) ↔ M.IsEven

The real model of M is even exactly when M is even.

theorem TauCeti.IntegralLattice.isUnimodular_realModel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : ZLattice.IsUnimodular (M.realModel hM) ↔ M.IsUnimodular

The real model of M is unimodular exactly when M is unimodular.

Duals and discriminant forms

@[simp]

theorem TauCeti.IntegralLattice.ratModelMap_ratModelRealModelIsometry {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : V) : (ZLattice.ratModelMap (M.realModel hM)) ((M.ratModelRealModelIsometry hM) x) = (M.realModelMap hM) x

The rational-model embedding after the round-trip isometry is the original rational embedding into the real model space.

noncomputable def TauCeti.IntegralLattice.realModelDualEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : ↥M.dualCarrier ≃ₗ[ℤ] ↥(ZLattice.dual (M.realModel hM))

The dual carrier of a positive definite rational lattice identifies with the dual of its real model, by the rational embedding.

@[simp]

theorem TauCeti.IntegralLattice.ratModelDualEquiv_realModelDualEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : ↥M.dualCarrier) : (ZLattice.ratModelDualEquiv ⋯) ((M.realModelDualEquiv hM) x) = (M.ratModelRealModelIsometry hM).dualCarrierEquiv x

The dual identification followed by rationalization is the round-trip isometry on duals.

@[simp]

theorem TauCeti.IntegralLattice.coe_realModelDualEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : ↥M.dualCarrier) : ↑((M.realModelDualEquiv hM) x) = (M.realModelMap hM) ↑x

On dual vectors, the dual identification is the rational embedding.

@[simp]

theorem TauCeti.IntegralLattice.realModelMap_realModelDualEquiv_symm {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (y : ↥(ZLattice.dual (M.realModel hM))) : (M.realModelMap hM) ↑((M.realModelDualEquiv hM).symm y) = ↑y

The inverse dual identification recovers a real dual vector through the rational embedding.

theorem TauCeti.IntegralLattice.realModelMap_mem_dual_realModel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : V) : (M.realModelMap hM) x ∈ ZLattice.dual (M.realModel hM) ↔ x ∈ M.dualCarrier

A rational vector belongs to the dual of the real model exactly when it belongs to the rational dual carrier.

noncomputable def TauCeti.IntegralLattice.realModelDiscriminantGroupEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : M.DiscriminantGroup ≃ₗ[ℤ] ZLattice.DiscriminantGroup (M.realModel hM)

The discriminant group of a positive definite rational lattice identifies with the (discrete Euclidean) discriminant group of its real model.

@[simp]

theorem TauCeti.IntegralLattice.ratModelDiscriminantGroupEquiv_realModelDiscriminantGroupEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : M.DiscriminantGroup) : (ZLattice.ratModelDiscriminantGroupEquiv ⋯) ((M.realModelDiscriminantGroupEquiv hM) x) = (M.ratModelRealModelIsometry hM).discriminantGroupEquiv x

The discriminant identification followed by rationalization is the round-trip isometry.

@[simp]

theorem TauCeti.IntegralLattice.realModelDiscriminantGroupEquiv_mk {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x : ↥M.dualCarrier) : (M.realModelDiscriminantGroupEquiv hM) (Submodule.Quotient.mk x) = Submodule.Quotient.mk ((M.realModelDualEquiv hM) x)

The discriminant-group identification sends the class of a rational dual vector to the class of its real image.

@[simp]

theorem TauCeti.IntegralLattice.realModelDiscriminantGroupEquiv_symm_mk {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (y : ↥(ZLattice.dual (M.realModel hM))) : (M.realModelDiscriminantGroupEquiv hM).symm (Submodule.Quotient.mk y) = Submodule.Quotient.mk ((M.realModelDualEquiv hM).symm y)

The inverse discriminant identification sends a real dual class to the class of its rational preimage.

@[simp]

theorem TauCeti.IntegralLattice.discriminantPairing_realModelDiscriminantGroupEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (x y : M.DiscriminantGroup) : ((ZLattice.ratModel ⋯).discriminantPairing ((ZLattice.ratModelDiscriminantGroupEquiv ⋯) ((M.realModelDiscriminantGroupEquiv hM) x))) ((ZLattice.ratModelDiscriminantGroupEquiv ⋯) ((M.realModelDiscriminantGroupEquiv hM) y)) = (M.discriminantPairing x) y

The discriminant pairing transported through the real model agrees with the original rational discriminant pairing. The real-model pairing is read through its rational model, so no second discriminant form is introduced.

@[simp]

theorem TauCeti.IntegralLattice.discriminantQuadraticMap_realModelDiscriminantGroupEquiv {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) (hE : M.IsEven) (x : M.DiscriminantGroup) : ((ZLattice.ratModel ⋯).discriminantQuadraticMap ⋯) ((ZLattice.ratModelDiscriminantGroupEquiv ⋯) ((M.realModelDiscriminantGroupEquiv hM) x)) = (M.discriminantQuadraticMap hE) x

For an even lattice, the half-norm discriminant quadratic map transported through the real model agrees with the original quadratic map.

@[simp]

theorem TauCeti.IntegralLattice.natCard_discriminantGroup_realModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) : Nat.card (ZLattice.DiscriminantGroup (M.realModel hM)) = Nat.card M.DiscriminantGroup

The discriminant group of the real model of M has the order of the discriminant group of M.

@[simp]

theorem TauCeti.IntegralLattice.det_realModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] (M : IntegralLattice V) (hM : M.IsPosDef) [MeasurableSpace (M.RealModelSpace hM)] [BorelSpace (M.RealModelSpace hM)] : ZLattice.det (M.realModel hM) = ↑M.determinant

The determinant of the real model of M, its squared covolume, is the determinant of M.

noncomputable def TauCeti.IntegralLattice.Isometry.ofRealModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} {W : Type u_2} [AddCommGroup W] [Module ℚ W] {M' : IntegralLattice W} {hM' : M'.IsPosDef} (f : M.RealModelSpace hM ≃ₗᵢ[ℝ] M'.RealModelSpace hM') (hf : Submodule.map (↑(LinearEquiv.restrictScalars ℤ f.toLinearEquiv)) (M.realModel hM) = M'.realModel hM') : M.Isometry M'

A real linear isometry carrying the real model of M onto the real model of M' induces an isometry of the integral lattices M and M'.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.realModelMap_ofRealModel_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} {W : Type u_2} [AddCommGroup W] [Module ℚ W] {M' : IntegralLattice W} {hM' : M'.IsPosDef} (f : M.RealModelSpace hM ≃ₗᵢ[ℝ] M'.RealModelSpace hM') (hf : Submodule.map (↑(LinearEquiv.restrictScalars ℤ f.toLinearEquiv)) (M.realModel hM) = M'.realModel hM') (x : V) : (M'.realModelMap hM') ((ofRealModel f hf) x) = f ((M.realModelMap hM) x)

The isometry induced by a real isometry of real models agrees with it on rational vectors.

theorem TauCeti.IntegralLattice.map_realModel_ne_realModel {V : Type u_1} [AddCommGroup V] [Module ℚ V] {M : IntegralLattice V} {hM : M.IsPosDef} {W : Type u_2} [AddCommGroup W] [Module ℚ W] {N : IntegralLattice W} {hN : N.IsPosDef} (hMN : IsEmpty (M.Isometry N)) (f : M.RealModelSpace hM ≃ₗᵢ[ℝ] N.RealModelSpace hN) : Submodule.map (↑(LinearEquiv.restrictScalars ℤ f.toLinearEquiv)) (M.realModel hM) ≠ N.realModel hN

Non-isometric lattices have non-isometric real models: if the positive definite rational lattices M and N are not isometric, no real linear isometry of the ambient spaces carries the real model of M onto that of N.

theorem TauCeti.IntegralLattice.IsPosDef.determinant_eq_card_discriminantGroup {V : Type u_1} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : L.determinant = ↑(Nat.card L.DiscriminantGroup)

The determinant of a positive definite rational integral lattice is the order of its discriminant group.

noncomputable def ZLattice.realModelRatModelIsometry {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : (ratModel hL).RealModelSpace ⋯ ≃ₗᵢ[ℝ] E

The real model space of the rational model of an integral full lattice L is isometric to E, by the real-linear extension r ⊗ z ↦ r • ratModelMap L z of ratModelMap L. It carries the real model onto L (map_realModel_realModelRatModelIsometry).

@[simp]

theorem ZLattice.realModelRatModelIsometry_tmul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (r : ℝ) (z : TensorProduct ℤ ℚ ↥L) : (realModelRatModelIsometry hL) (r ⊗ₜ[ℚ] z) = r • (ratModelMap L) z

The isometry realModelRatModelIsometry hL sends r ⊗ z to r • ratModelMap L z.

@[simp]

theorem ZLattice.realModelRatModelIsometry_realModelMap {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) (z : TensorProduct ℤ ℚ ↥L) : (realModelRatModelIsometry hL) (((ratModel hL).realModelMap ⋯) z) = (ratModelMap L) z

The isometry realModelRatModelIsometry hL extends ratModelMap L.

theorem ZLattice.map_realModel_realModelRatModelIsometry {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {L : Submodule ℤ E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hL : IsIntegral L) : Submodule.map (↑(LinearEquiv.restrictScalars ℤ (realModelRatModelIsometry hL).toLinearEquiv)) ((ratModel hL).realModel ⋯) = L

The isometry realModelRatModelIsometry hL carries the real model of the rational model of L onto L.