Definition of lattices

Let K be a field and R a subring. Then an R-submodule M of ι → K is a lattice, if M is finitely generated and it spans ι → K as a K-module.

If R is a principal ideal domain, any lattice is a free R-module of rank cardinality of ι.

class IsLattice {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (M : Submodule (↥R) (ι → K)) : Prop

An R-submodule M of ι → K is a lattice if it is finitely generated and spans ι → K as a K-module.

• isFG : M.FG

  M is finitely generated.

• spans : Submodule.span K ↑M = ⊤

  M spans ι → K

instance IsLattice.finite {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (M : Submodule (↥R) (ι → K)) [IsLattice M] : Module.Finite ↥R ↥M

Any R-lattice is finite.

instance IsLattice.smul {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (M : Submodule (↥R) (ι → K)) [IsLattice M] (a : Kˣ) : IsLattice (a • M)

The action of Kˣ on R-submodules of ι → K preserves IsLattice.

theorem IsLattice.of_le_of_isLattice {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsNoetherianRing ↥R] {M L P : Submodule (↥R) (ι → K)} [IsLattice M] [IsLattice P] (hML : M ≤ L) (hLP : L ≤ P) : IsLattice L

instance Matrix.GeneralLinearGroup.toSubmodule_isLattice {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (g : GL ι K) : IsLattice g.toSubmodule

The submodule spanned by the columns of an invertible matrix is a lattice.

instance Matrix.GeneralLinearGroup.instIsLatticeHSMulSubmoduleSubtypeMemSubringForall {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (g : GL ι K) (M : Submodule (↥R) (ι → K)) [IsLattice M] : IsLattice (g • M)

theorem Module.Basis.top_le_submodule_span_of_isLattice {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} {κ : Type u_3} [Finite κ] {M : Submodule (↥R) (ι → K)} (b : Basis κ ↥R ↥M) [IsLattice M] : ⊤ ≤ Submodule.span K (Set.range fun (i : κ) => ↑(b i))

noncomputable def Module.Basis.ofSubmodule {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (b : Basis ι ↥R ↥M) : Basis ι K (ι → K)

Given an R-lattice M of ι → K and an R-basis of M, this basis is also a K basis of ι → K.

Equations

• b.ofSubmodule = Module.Basis.mk ⋯ ⋯

noncomputable def Module.Basis.toGeneralLinearGroup {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι K (ι → K)) : GL ι K

Any K-basis of ι → K defines an element of GL ι K.

Equations

• b.toGeneralLinearGroup = Matrix.GeneralLinearGroup.toLin.symm (LinearMap.GeneralLinearGroup.ofLinearEquiv ((Pi.basisFun K ι).equiv b (Equiv.refl ι)))

@[simp]

theorem Module.Basis.toGeneralLinearGroup_apply {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι K (ι → K)) (i j : ι) : ↑b.toGeneralLinearGroup i j = b j i

noncomputable def Module.Basis.toGL {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] [DecidableEq ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (b : Basis ι ↥R ↥M) : GL ι K

Given an R-lattice M of ι → K and an R-basis b of M, the columns of b form an invertible K-matrix.

Equations

• b.toGL = b.ofSubmodule.toGeneralLinearGroup

@[simp]

theorem Module.Basis.toGL_apply {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] [DecidableEq ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (b : Basis ι ↥R ↥M) (i j : ι) : ↑b.toGL i j = ↑(b j) i

@[simp]

theorem Module.Basis.transpose_toGL {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] [DecidableEq ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (b : Basis ι ↥R ↥M) (i : ι) : (↑b.toGL).transpose i = ↑(b i)

theorem Module.Basis.toGL_toSubmodule {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] [DecidableEq ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (b : Basis ι ↥R ↥M) : b.toGL.toSubmodule = M

Lattices are free

In this section we prove that every lattice is a free R-module of finite rank the cardinality of ι and that every such R-module is a lattice.

instance IsLattice.free {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsPrincipalIdealRing ↥R] (M : Submodule (↥R) (ι → K)) [IsLattice M] : Module.Free ↥R ↥M

Any lattice is a free R-module.

theorem IsLattice.rank' {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [IsPrincipalIdealRing ↥R] [Fintype ι] (M : Submodule (↥R) (ι → K)) [IsLattice M] : Module.rank ↥R ↥M = ↑(Fintype.card ι)

Any lattice has the cardinality of ι as R-rank.

theorem IsLattice.rank {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] [IsPrincipalIdealRing ↥R] {k : ℕ} (M : Submodule (↥R) (Fin k → K)) [IsLattice M] : Module.rank ↥R ↥M = ↑k

Any R-lattice has rank k as an R-module.

theorem IsLattice.finrank {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] [IsPrincipalIdealRing ↥R] {k : ℕ} (M : Submodule (↥R) (Fin k → K)) [IsLattice M] : Module.finrank ↥R ↥M = k

FiniteDimensional.finrank version of IsLattice.rank.

instance IsLattice.sup {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (M N : Submodule (↥R) (ι → K)) [IsLattice M] [IsLattice N] : IsLattice (M ⊔ N)

The supremum of two lattices is a lattice.

theorem Submodule.span_eq_top_of_rank {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] {M : Submodule (↥R) (ι → K)} (h : Module.rank ↥R ↥M = ↑(Fintype.card ι)) : span K ↑M = ⊤

theorem IsLattice.of_rank {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] {M : Submodule (↥R) (ι → K)} (hfg : M.FG) (hr : Module.rank ↥R ↥M = ↑(Fintype.card ι)) : IsLattice M

An R-submodule of ι → K that is finitely generated and has rank the cardinality of ι is a lattice.

theorem IsLattice.intersection {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [IsPrincipalIdealRing ↥R] (M N : Submodule (↥R) (ι → K)) [Finite ι] [IsLattice M] [IsLattice N] : IsLattice (M ⊓ N)

The intersection of two lattices is a lattice.

structure BruhatTits.Lattice {K : Type u_1} [Field K] (R : Subring K) : Type u_1

An R-lattice is a submodule M of Fin 2 → K which satisfies IsLattice.

• M : Submodule (↥R) (Fin 2 → K)

  The underlying submodule of a lattice.

• isLattice : IsLattice self.M

theorem BruhatTits.Lattice.ext_iff {K : Type u_1} {inst✝ : Field K} {R : Subring K} {x y : Lattice R} : x = y ↔ x.M = y.M

theorem BruhatTits.Lattice.ext {K : Type u_1} {inst✝ : Field K} {R : Subring K} {x y : Lattice R} (M : x.M = y.M) : x = y

@[implicit_reducible]

instance BruhatTits.Lattice.instSMulUnits {K : Type u_1} [Field K] (R : Subring K) : SMul Kˣ (Lattice R)

Equations

• BruhatTits.Lattice.instSMulUnits R = { smul := fun (a : Kˣ) (L : BruhatTits.Lattice R) => { M := a • L.M, isLattice := ⋯ } }

@[simp]

theorem BruhatTits.Lattice.smul_module {K : Type u_1} [Field K] (R : Subring K) (a : Kˣ) (L : Lattice R) : (a • L).M = a • L.M

@[implicit_reducible]

instance BruhatTits.Lattice.instMulActionUnits {K : Type u_1} [Field K] (R : Subring K) : MulAction Kˣ (Lattice R)

Kˣ acts on R-lattices by acting on the submodule.

Equations

• BruhatTits.Lattice.instMulActionUnits R = { toSMul := BruhatTits.Lattice.instSMulUnits R, mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance BruhatTits.Lattice.instSMulGeneralLinearGroupFinOfNatNat {K : Type u_1} [Field K] (R : Subring K) : SMul (GL (Fin 2) K) (Lattice R)

Equations

• BruhatTits.Lattice.instSMulGeneralLinearGroupFinOfNatNat R = { smul := fun (g : GL (Fin 2) K) (L : BruhatTits.Lattice R) => { M := g • L.M, isLattice := ⋯ } }

theorem BruhatTits.Lattice.smul_M {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (L : Lattice R) : (g • L).M = g • L.M

@[implicit_reducible]

instance BruhatTits.Lattice.instMulActionGeneralLinearGroupFinOfNatNat {K : Type u_1} [Field K] {R : Subring K} : MulAction (GL (Fin 2) K) (Lattice R)

Equations

• BruhatTits.Lattice.instMulActionGeneralLinearGroupFinOfNatNat = { toSMul := BruhatTits.Lattice.instSMulGeneralLinearGroupFinOfNatNat R, mul_smul := ⋯, one_smul := ⋯ }

theorem BruhatTits.Lattice.embDiagonal_smul_eq_smul {K : Type u_1} [Field K] {R : Subring K} (L : Lattice R) (u : Kˣ) : (Matrix.GeneralLinearGroup.embDiagonal K (Fin 2)) u • L = u • L

noncomputable def BruhatTits.Lattice.basis {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] [IsPrincipalIdealRing ↥R] (L : Lattice R) : Module.Basis (Fin 2) ↥R ↥L.M

Given a lattice, this is an arbitrary choice of a basis.

Equations

• L.basis = Module.finBasisOfFinrankEq ↥R ↥L.M ⋯

def BruhatTits.Lattice.IsSimilar {K : Type u_1} [Field K] (R : Subring K) (L N : Lattice R) : Prop

Two R-lattices L and N are similar, if N is a Kˣ-multiple of L.

Equations

• BruhatTits.Lattice.IsSimilar R L N = ∃ (a : Kˣ), a • L = N

theorem BruhatTits.Lattice.IsSimilar.equivalence {K : Type u_1} [Field K] (R : Subring K) : Equivalence (IsSimilar R)

IsSimilar is an equivalence relation.

theorem BruhatTits.Lattice.isSimilar_smul {K : Type u_1} [Field K] (R : Subring K) (L : Lattice R) (a : Kˣ) : IsSimilar R L (a • L)

theorem BruhatTits.Lattice.smul_isSimilar {K : Type u_1} [Field K] (R : Subring K) (L : Lattice R) (a : Kˣ) : IsSimilar R (a • L) L

@[implicit_reducible]

instance BruhatTits.Lattice.IsSimilar.setoid {K : Type u_1} [Field K] (R : Subring K) : Setoid (Lattice R)

Equations

• BruhatTits.Lattice.IsSimilar.setoid R = { r := BruhatTits.Lattice.IsSimilar R, iseqv := ⋯ }