Distance on lattices and vertices

In this file we define the distance function dist on lattices. For this we apply the Cartan decomposition to bring every pair of lattices M and L into a standard form:

There exists a basis bM of M and a basis bL of L such that bLᵢ = ϖ ^ fᵢ • bMᵢ for i = 1,2 and integers fᵢ. If we fix the order of fᵢ to be f₁ ≥ f₂, the fᵢ are unique, i.e. don't depend on ϖ, bM or bL.

We then say that the distance of M and L is f₁ - f₂ which is ≥ 0 by our assumption on the fᵢ.

One then verifies that the difference f₁ - f₂ is invariant under multiplying M or L with units of K and hence we obtain a distance function inv on the vertices of the Bruhat-Tits graph.

Main definitions

• BruhatTits.dist L M: The distance between two latticesL and M.

Main results

• BruhatTits.exists_normal_basis: Given two lattices, we can find good bases using the Cartan decomposition.
• BruhatTits.dist_symm: The distance function is symmetric.
• BruhatTits.dist_inv_isSimilar: The distance function is invariant under homothety.

theorem BruhatTits.smulBasis_apply_of_isLattice {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (g : GL ι ↥R) (b : Module.Basis ι ↥R ↥M) (i j : ι) : ↑((g.smulBasis b) i) j = ↑(b.toGL * «GL».map R.subtype g) j i

instance BruhatTits.instIsPretransitiveGeneralLinearGroupFinOfNatNatLattice {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] : MulAction.IsPretransitive (GL (Fin 2) K) (Lattice R)

GL₂(K) acts transitively on R-lattices.

theorem BruhatTits.basis_smul_def_of_isLattice {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (g : GL ι ↥R) (b : Module.Basis ι ↥R ↥M) (i j : ι) : ↑((MulOpposite.op g • b) i) j = ↑(b.toGL * «GL».map R.subtype g) j i

theorem BruhatTits.basis_smul_toGL {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] {ι : Type u_2} [DecidableEq ι] [Fintype ι] {M : Submodule (↥R) (ι → K)} [IsLattice M] (g : GL ι ↥R) (b : Module.Basis ι ↥R ↥M) : (MulOpposite.op g • b).toGL = b.toGL * «GL».map R.subtype g

theorem BruhatTits.exists_normal_basis {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (ϖ : ↥R) (hϖ : Irreducible ϖ) (M L : Lattice R) : ∃ (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M) (f : Fin 2 → ℤ), Antitone f ∧ ∀ (i : Fin 2), ↑(bL i) = ↑ϖ ^ f i • ↑(bM i)

Given two R-lattices M and L, there exists a basis bM of M and a basis bL of L such that bLᵢ = ϖ ^ fᵢ • bMᵢ for i = 1,2 and integers fᵢ. If we fix the order of fᵢ to be f₁ ≥ f₂, the fᵢ are unique, i.e. don't depend on ϖ, bM or bL.

theorem BruhatTits.exists_normal_basis_uniformizer {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : ∃ (ϖ : ↥R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M) (f : Fin 2 → ℤ), Irreducible ϖ ∧ Antitone f ∧ ∀ (i : Fin 2), ↑(bL i) = ↑ϖ ^ f i • ↑(bM i)

A variant of BruhatTits.exists_normal_basis where also a uniformizer is provided.

theorem BruhatTits.signature_unique {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {M L : Lattice R} {ϖ ϖ' : ↥R} (hϖ : Irreducible ϖ) (hϖ' : Irreducible ϖ') {bM bM' : Module.Basis (Fin 2) ↥R ↥M.M} {bL bL' : Module.Basis (Fin 2) ↥R ↥L.M} {f f' : Fin 2 → ℤ} (hf : Antitone f) (hf' : Antitone f') (h : ∀ (i : Fin 2), ↑(bL i) = ↑ϖ ^ f i • ↑(bM i)) (h' : ∀ (i : Fin 2), ↑(bL' i) = ↑ϖ' ^ f' i • ↑(bM' i)) : f = f'

The integers fᵢ of BruhatTits.exists_normal_basis are unique. More precisely, given two lattices M and L, uniformizers ϖ, ϖ', basis bM, bM' of M and bL, bL' of L and integers fᵢ, fᵢ' such that bLᵢ = ϖ ^ fᵢ • bMᵢ and bL'ᵢ = ϖ' ^ f'ᵢ • bM'ᵢ and with f₂ ≥ f₁, f'₁ ≥ f'₂, then fᵢ = fᵢ'. This unique pair of integers fᵢ is called the signature of L and M.

Choice of signature

In this section for every pair of lattices M and L, we fix arbitrarily chosen basis bM of M and bL of L and the (antitone) signature fᵢ such that bLᵢ = ϖ ^ fᵢ • bMᵢ.

noncomputable def BruhatTits.signatureϖ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : ↥R

A choice of uniformizer.

Equations

• BruhatTits.signatureϖ M L = ⋯.choose

theorem BruhatTits.signatureϖ_irreducible {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : Irreducible (signatureϖ M L)

The chosen uniformizer is irreducible.

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

A choice of basis for M.

Equations

• BruhatTits.signatureBasisSource M L = ⋯.choose

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

A choice of basis for L.

Equations

• BruhatTits.signatureBasisTarget M L = ⋯.choose

noncomputable def BruhatTits.signature {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : Fin 2 → ℤ

The unique (antitone) signature of M and L.

Equations

• BruhatTits.signature M L = ⋯.choose

theorem BruhatTits.signature_antitone {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : Antitone (signature M L)

theorem BruhatTits.signatureBasisTarget_eq {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) (i : Fin 2) : ↑((signatureBasisTarget M L) i) = ↑(signatureϖ M L) ^ signature M L i • ↑((signatureBasisSource M L) i)

theorem BruhatTits.eq_signature_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) (f : Fin 2 → ℤ) (hf : Antitone f) : signature M L = f ↔ ∃ (ϖ : ↥R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M), Irreducible ϖ ∧ ∀ (i : Fin 2), ↑(bL i) = ↑ϖ ^ f i • ↑(bM i)

To show that an antitone pair of integers fᵢ is the signature of M and L it suffices to find basis that satisfy the defining property of the signature.

noncomputable def BruhatTits.dist {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : ℕ

We define the distance between lattices M and L to be f₁ - f₂ where fᵢ is the (antitone) signature. This is always ≥ 0, because f₁ ≥ f₂.

Equations

• BruhatTits.dist M L = (BruhatTits.signature M L 0 - BruhatTits.signature M L 1).toNat

theorem BruhatTits.signature_diff_eq_dist {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : signature M L 0 - signature M L 1 = ↑(dist M L)

theorem BruhatTits.eq_dist_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) (n : ℕ) : dist M L = n ↔ ∃ (ϖ : ↥R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M) (f : Fin 2 → ℤ), Irreducible ϖ ∧ Antitone f ∧ (∀ (i : Fin 2), ↑(bL i) = ↑ϖ ^ f i • ↑(bM i)) ∧ f 0 - f 1 = ↑n

A rephrasing of uniqueness of signatures in terms of the distance of lattices.

theorem BruhatTits.eq_dist_iff₂ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) (n : ℕ) : dist M L = n ↔ ∃ (ϖ : ↥R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M) (a : ℤ) (b : ℤ), Irreducible ϖ ∧ b ≤ a ∧ ↑(bL 0) = ↑ϖ ^ a • ↑(bM 0) ∧ ↑(bL 1) = ↑ϖ ^ b • ↑(bM 1) ∧ a - b = ↑n

Variant of BruhatTits.eq_dist_iff where the signature is unwrapped as two integers a and b.

theorem BruhatTits.eq_dist_iff_monotone {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) (n : ℕ) : dist M L = n ↔ ∃ (ϖ : ↥R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M) (f : Fin 2 → ℤ), Irreducible ϖ ∧ Monotone f ∧ (∀ (i : Fin 2), ↑(bL i) = ↑ϖ ^ f i • ↑(bM i)) ∧ f 1 - f 0 = ↑n

Monotone variant of BruhatTits.eq_dist_iff.

theorem BruhatTits.exists_repr_dist {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : ∃ (ϖ : ↥R) (bM : Module.Basis (Fin 2) ↥R ↥M.M) (bL : Module.Basis (Fin 2) ↥R ↥L.M) (f : Fin 2 → ℤ), Irreducible ϖ ∧ Antitone f ∧ (∀ (i : Fin 2), ↑(bL i) = ↑ϖ ^ f i • ↑(bM i)) ∧ f 0 - f 1 = ↑(dist M L)

theorem BruhatTits.dist_symm {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) : dist M L = dist L M

The distance on lattices is symmetric.

@[simp]

theorem BruhatTits.dist_self {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : dist L L = 0

The distance of a lattice to itself is zero.

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

Transport a basis of a submodule along the action of GL.

Equations

• BruhatTits.mulBasis g b = b.map (g.equivSMulGL M)

def BruhatTits.equivSMul {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (a : Kˣ) (M : Submodule (↥R) (ι → K)) : ↥M ≃ₗ[↥R] ↥(a • M)

The linear equivalence from a submodule to its scalar multiple.

Equations

• BruhatTits.equivSMul a M = (LinearEquiv.restrictScalars (↥R) (LinearEquiv.smulOfUnit a)).submoduleMap M

noncomputable def BruhatTits.mulBasisScalar {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (a : Kˣ) {M : Lattice R} (b : Module.Basis ι ↥R ↥M.M) : Module.Basis ι ↥R ↥(a • M).M

Transport a lattice basis along scalar multiplication.

Equations

• BruhatTits.mulBasisScalar a b = b.map (BruhatTits.equivSMul a M.M)

theorem BruhatTits.mulBasisScalar_apply {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (a : Kˣ) (M : Lattice R) (b : Module.Basis ι ↥R ↥M.M) (i : ι) : ↑((mulBasisScalar a b) i) = ↑a • ↑(b i)

theorem BruhatTits.mulBasis_apply {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : GL ι K) {M : Submodule (↥R) (ι → K)} (b : Module.Basis ι ↥R ↥M) (i : ι) : ↑((mulBasis g b) i) = (↑g).mulVec ↑(b i)

theorem BruhatTits.mulBasisScalar_toGL {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] (a : Kˣ) (M : Lattice R) (b : Module.Basis (Fin 2) ↥R ↥M.M) : (mulBasisScalar a b).toGL = (Matrix.GL.diagonal fun (x : Fin 2) => a) * b.toGL

theorem BruhatTits.unit_smul_eq {K : Type u_1} [Field K] {R : Subring K} (u : (↥R)ˣ) (M : Lattice R) : (Units.map ↑R.subtype) u • M = M

theorem BruhatTits.dist_smul_eq_dist {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L : Lattice R) (a : Kˣ) : dist (a • M) L = dist M L

The distance of a lattice M to a given lattice L does not change when M is scaled by some a : Kˣ.

theorem BruhatTits.dist_inv_isSimilar {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (M L M' L' : Lattice R) (hM : Lattice.IsSimilar R M M') (hL : Lattice.IsSimilar R L L') : dist M L = dist M' L'

The distance of lattices is invariant under the equivalence relation IsSimilar.