Isometries of integral lattices

An isometry of integral lattices is a rational linear isometry of their ambient bilinear spaces which maps one integral carrier onto the other. This is stronger than an additive or linear equivalence of the carriers: the rational form-preservation equation is part of the data.

This file provides the identity, inverse, and composition isometries, restricts an isometry to an integral linear equivalence of carriers, and extends every form-preserving carrier equivalence uniquely to the rational ambient spaces. It also transports an integral lattice along an ambient linear equivalence and records the canonical isometry to the transported lattice.

The isometry API (coercions, EquivLike/LinearEquivClass instances, and identity, inverse, and composition) follows Mathlib's LinearMap.BilinForm.IsometryEquiv API in Mathlib/LinearAlgebra/BilinearForm/IsometryEquiv.lean.

Main definitions

• TauCeti.IntegralLattice.Isometry: a form-preserving rational linear equivalence mapping one integral carrier onto another.
• TauCeti.IntegralLattice.Isometry.ambientEquiv: the ambient equivalence of an isometry, read over ℤ.
• TauCeti.IntegralLattice.Isometry.carrierEquiv: restriction of an isometry to the carriers.
• TauCeti.IntegralLattice.Isometry.carrierBasisEquiv: transport of carrier bases along an isometry.
• TauCeti.IntegralLattice.Isometry.ofCarrierEquiv: rational extension of a form-preserving integral linear equivalence of carriers.
• TauCeti.IntegralLattice.transport: transport of a lattice along a rational linear equivalence.
• TauCeti.IntegralLattice.transportIsometry: the canonical isometry to a transported lattice.

Main results

• TauCeti.IntegralLattice.Isometry.carrierEquiv_ofCarrierEquiv and TauCeti.IntegralLattice.Isometry.ofCarrierEquiv_carrierEquiv: the two round trips between ambient isometries and form-preserving carrier equivalences.
• TauCeti.IntegralLattice.Isometry.carrierEquiv_injective: an isometry is determined by its restriction to the carriers.
• TauCeti.IntegralLattice.Isometry.finrank_carrier_eq: invariance of the carrier rank.
• TauCeti.IntegralLattice.transport_refl: transporting along the identity changes no lattice.

References

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

structure TauCeti.IntegralLattice.Isometry {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (M : IntegralLattice W) extends L.form.IsometryEquiv M.form : Type (max u v)

An isometry of integral lattices is an isometry of their ambient rational bilinear spaces which maps the first carrier onto the second.

• toFun : V → W
• map_add' (x y : V) : (↑self.toLinearEquiv).toFun (x + y) = (↑self.toLinearEquiv).toFun x + (↑self.toLinearEquiv).toFun y
• map_smul' (m : ℚ) (x : V) : (↑self.toLinearEquiv).toFun (m • x) = (RingHom.id ℚ) m • (↑self.toLinearEquiv).toFun x
• invFun : W → V
• left_inv : Function.LeftInverse self.invFun (↑self.toLinearEquiv).toFun
• right_inv : Function.RightInverse self.invFun (↑self.toLinearEquiv).toFun
• map_app' (n m : V) : (M.form ((↑self.toLinearEquiv).toFun n)) ((↑self.toLinearEquiv).toFun m) = (L.form n) m
• map_carrier : Submodule.map (↑(LinearEquiv.restrictScalars ℤ self.toLinearEquiv)) L.carrier = M.carrier

  The ambient equivalence maps the source lattice carrier onto the target carrier.

@[instance_reducible]

instance TauCeti.IntegralLattice.Isometry.instCoeOutLinearEquivRatId {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} : CoeOut (L.Isometry M) (V ≃ₗ[ℚ] W)

An integral-lattice isometry coerces to its ambient rational linear equivalence.

Equations

• TauCeti.IntegralLattice.Isometry.instCoeOutLinearEquivRatId = { coe := fun (e : L.Isometry M) => e.toLinearEquiv }

@[instance_reducible]

instance TauCeti.IntegralLattice.Isometry.instEquivLike {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} : EquivLike (L.Isometry M) V W

An integral-lattice isometry acts on the ambient rational vector spaces.

Equations

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

instance TauCeti.IntegralLattice.Isometry.instLinearEquivClassRat {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} : LinearEquivClass (L.Isometry M) ℚ V W

Integral-lattice isometries are rational linear equivalences.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_toLinearEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : ⇑e.toLinearEquiv = ⇑e

Coercion of an isometry to a linear equivalence acts the same as the isometry.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_toIsometryEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : ⇑e.toIsometryEquiv = ⇑e

Coercion of the underlying bilinear-form isometry acts the same as the lattice isometry.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.map_app {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x y : V) : (M.form (e x)) (e y) = (L.form x) y

An integral-lattice isometry preserves the ambient bilinear forms.

def TauCeti.IntegralLattice.Isometry.ambientEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : V ≃ₗ[ℤ] W

The ambient rational equivalence of an integral-lattice isometry, read as an equivalence of the underlying ℤ-modules. Carriers, dual carriers, and every submodule between them are transported along this equivalence.

Equations

• e.ambientEquiv = LinearEquiv.restrictScalars ℤ e.toLinearEquiv

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ambientEquiv_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : V) : e.ambientEquiv x = e x

@[simp]

theorem TauCeti.IntegralLattice.Isometry.apply_mem_carrier_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : V) : e x ∈ M.carrier ↔ x ∈ L.carrier

An ambient vector's image belongs to the target carrier if and only if the vector belongs to the source carrier.

theorem TauCeti.IntegralLattice.Isometry.ext {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {e f : L.Isometry M} (h : ∀ (x : V), e x = f x) : e = f

Two lattice isometries agreeing on the ambient space are equal.

theorem TauCeti.IntegralLattice.Isometry.ext_iff {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {e f : L.Isometry M} : e = f ↔ ∀ (x : V), e x = f x

def TauCeti.IntegralLattice.Isometry.refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.Isometry L

The identity isometry of an integral lattice.

Equations

• TauCeti.IntegralLattice.Isometry.refl L = { toIsometryEquiv := LinearMap.BilinForm.IsometryEquiv.refl L.form, map_carrier := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.refl_apply {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (x : V) : (refl L) x = x

Evaluation of the identity isometry on an ambient vector.

def TauCeti.IntegralLattice.Isometry.ofEq {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} (h : L = M) : L.Isometry M

The identity isometry between two equal integral lattices in the same ambient space.

Equations

• TauCeti.IntegralLattice.Isometry.ofEq h = h ▸ TauCeti.IntegralLattice.Isometry.refl L

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ofEq_apply {V : Type u} [AddCommGroup V] [Module ℚ V] {L M : IntegralLattice V} (h : L = M) (x : V) : (ofEq h) x = x

The identity isometry between equal lattices is the identity on the ambient space.

def TauCeti.IntegralLattice.Isometry.symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : M.Isometry L

The inverse of an integral-lattice isometry.

Equations

• e.symm = { toIsometryEquiv := e.symm, map_carrier := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.symm_apply_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : V) : e.symm (e x) = x

@[simp]

theorem TauCeti.IntegralLattice.Isometry.apply_symm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (y : W) : e (e.symm y) = y

@[simp]

theorem TauCeti.IntegralLattice.Isometry.symm_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.symm = e

Inverting an isometry twice yields the original isometry.

def TauCeti.IntegralLattice.Isometry.trans {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : L.Isometry N

Composition of integral-lattice isometries.

Equations

• e.trans f = { toIsometryEquiv := e.trans f.toIsometryEquiv, map_carrier := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.trans_apply {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) (x : V) : (e.trans f) x = f (e x)

@[simp]

theorem TauCeti.IntegralLattice.Isometry.self_trans_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.trans e.symm = refl L

An isometry composed with its inverse is the identity.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.symm_trans_self {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.trans e = refl M

The inverse of an isometry composed with the isometry is the identity.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.symm_trans {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : (e.trans f).symm = f.symm.trans e.symm

The inverse of a composition is the reversed composition of the inverses.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.refl_trans {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : (refl L).trans e = e

@[simp]

theorem TauCeti.IntegralLattice.Isometry.trans_refl {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.trans (refl M) = e

@[simp]

theorem TauCeti.IntegralLattice.Isometry.trans_assoc {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) {X : Type u_1} [AddCommGroup X] [Module ℚ X] {P : IntegralLattice X} (g : N.Isometry P) : (e.trans f).trans g = e.trans (f.trans g)

theorem TauCeti.IntegralLattice.Isometry.coe_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : ⇑e.symm = ⇑e.symm

The inverse lattice isometry acts as the inverse ambient linear equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ambientEquiv_symm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (y : W) : e.ambientEquiv.symm y = e.symm y

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ambientEquiv_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (refl L).ambientEquiv = LinearEquiv.refl ℤ V

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ambientEquiv_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.ambientEquiv = e.ambientEquiv.symm

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ambientEquiv_trans {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : (e.trans f).ambientEquiv = e.ambientEquiv ≪≫ₗ f.ambientEquiv

def TauCeti.IntegralLattice.Isometry.carrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : ↥L.carrier ≃ₗ[ℤ] ↥M.carrier

Restrict an integral-lattice isometry to an integral linear equivalence of its carriers.

Equations

• e.carrierEquiv = e.ambientEquiv.ofSubmodules L.carrier M.carrier ⋯

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_carrierEquiv_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x : ↥L.carrier) : ↑(e.carrierEquiv x) = e ↑x

@[simp]

theorem TauCeti.IntegralLattice.Isometry.coe_carrierEquiv_symm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (y : ↥M.carrier) : ↑(e.carrierEquiv.symm y) = e.symm ↑y

noncomputable def TauCeti.IntegralLattice.Isometry.carrierBasisEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (ι : Type u_1) : Module.Basis ι ℤ ↥L.carrier ≃ Module.Basis ι ℤ ↥M.carrier

An isometry transports bases of its source carrier to bases of its target carrier.

Equations

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

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierBasisEquiv_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {ι : Type u_1} (e : L.Isometry M) (b : Module.Basis ι ℤ ↥L.carrier) : (e.carrierBasisEquiv ι) b = b.map e.carrierEquiv

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierBasisEquiv_symm_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} {ι : Type u_1} (e : L.Isometry M) (b : Module.Basis ι ℤ ↥M.carrier) : (e.carrierBasisEquiv ι).symm b = b.map e.carrierEquiv.symm

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : (refl L).carrierEquiv = LinearEquiv.refl ℤ ↥L.carrier

The carrier restriction of the identity isometry is the identity linear equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_symm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : e.symm.carrierEquiv = e.carrierEquiv.symm

The carrier restriction of an inverse isometry is the inverse of the carrier restriction.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_trans {V : Type u} {W : Type v} {U : Type w} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] [AddCommGroup U] [Module ℚ U] {L : IntegralLattice V} {M : IntegralLattice W} {N : IntegralLattice U} (e : L.Isometry M) (f : M.Isometry N) : (e.trans f).carrierEquiv = e.carrierEquiv ≪≫ₗ f.carrierEquiv

The carrier restriction of a composed isometry is the composition of the carrier restrictions.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_map_integralForm {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (x y : ↥L.carrier) : (M.integralForm (e.carrierEquiv x)) (e.carrierEquiv y) = (L.integralForm x) y

The carrier equivalence preserves the induced integral bilinear forms.

theorem TauCeti.IntegralLattice.Isometry.finrank_carrier_eq {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : Module.finrank ℤ ↥L.carrier = Module.finrank ℤ ↥M.carrier

Isometric integral lattices have carriers of the same rank.

noncomputable def TauCeti.IntegralLattice.Isometry.ofCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : ↥L.carrier ≃ₗ[ℤ] ↥M.carrier) (hform : ∀ (x y : ↥L.carrier), (M.integralForm (e x)) (e y) = (L.integralForm x) y) : L.Isometry M

A form-preserving integral linear equivalence of carriers determines an isometry of the integral lattices.

Equations

• TauCeti.IntegralLattice.Isometry.ofCarrierEquiv e hform = { toIsometryEquiv := TauCeti.IntegralLattice.Isometry.isometryEquivOfCarrierEquiv✝ e hform, map_carrier := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ofCarrierEquiv_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : ↥L.carrier ≃ₗ[ℤ] ↥M.carrier) (hform : ∀ (x y : ↥L.carrier), (M.integralForm (e x)) (e y) = (L.integralForm x) y) (x : V) : (ofCarrierEquiv e hform) x = e.extendOfIsLattice x

@[simp]

theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_ofCarrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : ↥L.carrier ≃ₗ[ℤ] ↥M.carrier) (hform : ∀ (x y : ↥L.carrier), (M.integralForm (e x)) (e y) = (L.integralForm x) y) : (ofCarrierEquiv e hform).carrierEquiv = e

Restricting the isometry constructed from a form-preserving carrier equivalence recovers the original carrier equivalence.

@[simp]

theorem TauCeti.IntegralLattice.Isometry.ofCarrierEquiv_carrierEquiv {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) : ofCarrierEquiv e.carrierEquiv ⋯ = e

Extending the carrier restriction of an isometry recovers the original ambient isometry.

theorem TauCeti.IntegralLattice.Isometry.carrierEquiv_injective {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} : Function.Injective carrierEquiv

An isometry is determined by its restriction to the carriers.

noncomputable def TauCeti.IntegralLattice.transport {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (e : V ≃ₗ[ℚ] W) : IntegralLattice W

Transport an integral lattice along a rational linear equivalence.

The carrier is the image of the original carrier, and the form is pulled back along the inverse equivalence.

Equations

• L.transport e = { carrier := Submodule.map (↑(LinearEquiv.restrictScalars ℤ e)) L.carrier, form := L.form.comp ↑e.symm ↑e.symm, isLattice := ⋯, isSymm := ⋯, le_dual := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.transport_carrier {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (e : V ≃ₗ[ℚ] W) : (L.transport e).carrier = Submodule.map (↑(LinearEquiv.restrictScalars ℤ e)) L.carrier

@[simp]

theorem TauCeti.IntegralLattice.transport_form {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (e : V ≃ₗ[ℚ] W) : (L.transport e).form = L.form.comp ↑e.symm ↑e.symm

noncomputable def TauCeti.IntegralLattice.transportIsometry {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (e : V ≃ₗ[ℚ] W) : L.Isometry (L.transport e)

The canonical isometry from a lattice to its transport along an ambient equivalence.

Equations

• L.transportIsometry e = { toIsometryEquiv := L.form.isometryEquivOfCompLinearEquiv e.symm, map_carrier := ⋯ }

@[simp]

theorem TauCeti.IntegralLattice.transportIsometry_apply {V : Type u} {W : Type v} [AddCommGroup V] [Module ℚ V] [AddCommGroup W] [Module ℚ W] (L : IntegralLattice V) (e : V ≃ₗ[ℚ] W) (x : V) : (L.transportIsometry e) x = e x

@[simp]

theorem TauCeti.IntegralLattice.transport_refl {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : L.transport (LinearEquiv.refl ℚ V) = L