The R ⧸ ϖ R-vector space L ⧸ ϖ L

Let L be an R-lattice and ϖ be a uniformiser. In this file we examine the two-dimensional R ⧸ ϖ R-vector space L ⧸ ϖ L.

Main definitions

• Lattice.quotient: L ⧸ ϖ L.
• Basis.toQuotient: If b is an R-basis of the lattice L, this is the induced R ⧸ ϖ R-basis of L ⧸ ϖ L.
• Lattice.mapIntermediate: If L and M are lattices, this is the R ⧸ ϖ R-submodule spanned by the image of M ⊓ L in L ⧸ ϖ L.

Main results

• Lattice.mapIntermediate_inj_of: Lattice.mapIntermediate is injective on lattices between ϖ L and `L``.

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

The R ⧸ ϖ R-module L ⧸ ϖ L. We define this in terms of the maximal ideal of R.

Equations

• L.quotient = (↥L.M ⧸ IsLocalRing.maximalIdeal ↥R • ⊤)

@[implicit_reducible]

noncomputable instance BruhatTits.instAddCommGroupQuotient {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : AddCommGroup L.quotient

Equations

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

@[implicit_reducible]

noncomputable instance BruhatTits.Lattice.quotientModule {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : Module (↥R) L.quotient

Equations

• L.quotientModule = { smul := BruhatTits.Lattice.quotientModule._aux_1 L, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def BruhatTits.Lattice.toQuotient {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : ↥L.M →ₗ[↥R] L.quotient

The natural map L → L ⧸ ϖ L.

Equations

• L.toQuotient = (IsLocalRing.maximalIdeal ↥R • ⊤).mkQ

@[implicit_reducible]

noncomputable instance BruhatTits.instModuleResidueFieldSubtypeMemSubringQuotient {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : Module (IsLocalRing.ResidueField ↥R) L.quotient

Equations

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

@[implicit_reducible, instance 9999999]

noncomputable instance BruhatTits.instSMulSubtypeMemSubringQuotientIdealMaximalIdealLeanPool {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] : SMul (↥R) (↥R ⧸ IsLocalRing.maximalIdeal ↥R)

Equations

• BruhatTits.instSMulSubtypeMemSubringQuotientIdealMaximalIdealLeanPool = Submodule.Quotient.instSMul (IsLocalRing.maximalIdeal ↥R)

@[implicit_reducible, instance 9999999]

noncomputable instance BruhatTits.instSMulQuotientSubtypeMemSubringIdealMaximalIdealForallFinOfNatNatSubmoduleMHSMulTop {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : SMul (↥R ⧸ IsLocalRing.maximalIdeal ↥R) (↥L.M ⧸ IsLocalRing.maximalIdeal ↥R • ⊤)

Equations

• BruhatTits.instSMulQuotientSubtypeMemSubringIdealMaximalIdealForallFinOfNatNatSubmoduleMHSMulTop L = (Module.instQuotientIdealSubmoduleHSMulTop (↥L.M) (IsLocalRing.maximalIdeal ↥R)).toSMul

instance BruhatTits.instIsScalarTowerSubtypeMemSubringResidueFieldQuotient {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) : IsScalarTower (↥R) (IsLocalRing.ResidueField ↥R) L.quotient

theorem BruhatTits.Lattice.quotient_finrank {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : Module.finrank (IsLocalRing.ResidueField ↥R) L.quotient = 2

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

If b is an R-basis of the lattice L, this is the induced R ⧸ ϖ R-basis of L ⧸ ϖ L.

Equations

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

instance BruhatTits.instFreeResidueFieldSubtypeMemSubringQuotientOfIsFractionRing {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : Module.Free (IsLocalRing.ResidueField ↥R) L.quotient

instance BruhatTits.instFiniteResidueFieldSubtypeMemSubringQuotientOfIsFractionRing {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) : Module.Finite (IsLocalRing.ResidueField ↥R) L.quotient

noncomputable def Module.Basis.toQuotient' {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) : Basis (Fin 2) (IsLocalRing.ResidueField ↥R) b.toLattice.quotient

Variant of Basis.toQuotient for the lattice spanned by b.

Equations

• b.toQuotient' = b.restrictToLattice.toQuotient

theorem Module.Basis.toQuotient'_apply {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (i : Fin 2) : b.toQuotient' i = Submodule.Quotient.mk (b.restrict i)

noncomputable def Module.Basis.transvectResidue {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : Basis (Fin 2) (IsLocalRing.ResidueField ↥R) b.toLattice.quotient

Basis.transvect pushed to L ⧸ ϖ L where L is the lattice generated by b.

Equations

• b.transvectResidue x = b.toQuotient'.transvect ((Ideal.Quotient.mk (IsLocalRing.maximalIdeal ↥R)) x)

@[simp]

theorem Module.Basis.transvectResidue_apply₀ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.transvectResidue x) 0 = b.toQuotient' 0

@[simp]

theorem Module.Basis.transvectResidue_apply₁ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.transvectResidue x) 1 = x • b.toQuotient' 0 + b.toQuotient' 1

noncomputable def Module.Basis.unipotentResidue {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : b.toLattice.quotient ≃ₗ[IsLocalRing.ResidueField ↥R] b.toLattice.quotient

Basis.unipotent pushed to L ⧸ ϖ L where L is the lattice generated by b.

Equations

• b.unipotentResidue x = b.toQuotient'.equiv (b.transvectResidue x) (Equiv.refl (Fin 2))

theorem Module.Basis.unipotentResidue_apply₁ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.unipotentResidue x) (b.toQuotient' 1) = x • b.toQuotient' 0 + b.toQuotient' 1

theorem Module.Basis.unipotentResidue_apply₀ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) : (b.unipotentResidue x) (b.toQuotient' 0) = b.toQuotient' 0

theorem Module.Basis.transvectEquiv_apply_mem {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (y : ↥b.toSubmodule) : (b.transvectEquiv x) ↑y ∈ b.toSubmodule

theorem Module.Basis.unipotentResidue_mk {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (y : ↥b.toSubmodule) : (b.unipotentResidue x) (Submodule.Quotient.mk y) = Submodule.Quotient.mk ⟨(b.transvectEquiv x) ↑y, ⋯⟩

noncomputable def BruhatTits.Lattice.mapIntermediateSubmodule {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) (M : Submodule (↥R) (Fin 2 → K)) : Submodule (IsLocalRing.ResidueField ↥R) L.quotient

If L is a lattice and M any submodule of K^2, this is the image of M ⊓ L in L ⧸ ϖ L as a R ⧸ ϖ R-submodule.

Equations

• L.mapIntermediateSubmodule M = { toAddSubmonoid := (Submodule.map L.toQuotient (Submodule.comap L.M.subtype M)).toAddSubmonoid, smul_mem' := ⋯ }

noncomputable def BruhatTits.Lattice.mapIntermediate {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L M : Lattice R) : Submodule (IsLocalRing.ResidueField ↥R) L.quotient

Variant of Lattice.mapIntermediateSubmodule where M is a second lattice. This is the most frequent use case.

Equations

• L.mapIntermediate M = L.mapIntermediateSubmodule M.M

theorem BruhatTits.Lattice.mem_mapIntermediate {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L M : Lattice R) (x : L.quotient) : x ∈ L.mapIntermediate M ↔ ∃ (y : ↥L.M), ↑y ∈ M.M ∧ x = L.toQuotient y

theorem BruhatTits.Lattice.mapIntermediateSubmodule_inj_of {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Lattice R) (M₁ M₂ : Submodule (↥R) (Fin 2 → K)) (hle₁ : M₁ ≤ L.M) (hge₁ : IsLocalRing.maximalIdeal ↥R • L.M ≤ M₁) (hle₂ : M₂ ≤ L.M) (hge₂ : IsLocalRing.maximalIdeal ↥R • L.M ≤ M₂) (h : L.mapIntermediateSubmodule M₁ = L.mapIntermediateSubmodule M₂) : M₁ = M₂

Lattice.mapIntermediateSubmodule is injective on submodules between ϖ L and `L``.

theorem BruhatTits.Lattice.mapIntermediate_inj_of {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L M₁ M₂ : Lattice R) (hle₁ : M₁.M ≤ L.M) (hge₁ : IsLocalRing.maximalIdeal ↥R • L.M ≤ M₁.M) (hle₂ : M₂.M ≤ L.M) (hge₂ : IsLocalRing.maximalIdeal ↥R • L.M ≤ M₂.M) (h : L.mapIntermediate M₁ = L.mapIntermediate M₂) : M₁ = M₂

Lattice.mapIntermediate is injective on lattices between ϖ L and `L``.

noncomputable def Module.Basis.quotientStdLine₀ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : Submodule (IsLocalRing.ResidueField ↥R) b.toLattice.quotient

The image of the lattice spanned by (ϖ • b₀, b₁) in L ⧸ ϖ L where L is spanned by (b₀, b₁).

Equations

• b.quotientStdLine₀ hϖ = b.toLattice.mapIntermediate (b.ntwist₂ hϖ 1 0).toLattice

noncomputable def Module.Basis.quotientStdLine₁ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : Submodule (IsLocalRing.ResidueField ↥R) b.toLattice.quotient

The image of the lattice spanned by (b₀, ϖ • b₁) in L ⧸ ϖ L where L is spanned by (b₀, b₁).

Equations

• b.quotientStdLine₁ hϖ = b.toLattice.mapIntermediate (b.ntwist₂ hϖ 0 1).toLattice

theorem BruhatTits.mapIntermediate_stdLine₀ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : b.quotientStdLine₀ hϖ = IsLocalRing.ResidueField ↥R ∙ b.toQuotient' 1

The image of the span of (ϖ • b₀, b₁) in L ⧸ ϖ L is the submodule generated by the image of b₁.

theorem BruhatTits.mapIntermediate_stdLine₁ {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : b.quotientStdLine₁ hϖ = IsLocalRing.ResidueField ↥R ∙ b.toQuotient' 0

The image of the span of (b₀, ϖ • b₁) in L ⧸ ϖ L is the submodule generated by the image of b₀.

theorem BruhatTits.Lattice.mapIntermediate_ne_bot_of {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L M : Lattice R) {ϖ : ↥R} (hϖ : Irreducible ϖ) (h1 : M.M ≤ L.M) (h2 : ϖ • L.M < M.M) : L.mapIntermediate M ≠ ⊥

theorem BruhatTits.Lattice.mapIntermediate_ne_top_of {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L M : Lattice R) {ϖ : ↥R} (hϖ : Irreducible ϖ) (h1 : M.M < L.M) (h2 : ϖ • L.M ≤ M.M) : L.mapIntermediate M ≠ ⊤

theorem BruhatTits.Lattice.mapIntermediate_finrank_eq_one_of {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L M : Lattice R} {ϖ : ↥R} (hϖ : Irreducible ϖ) (h1 : M.M < L.M) (h2 : ϖ • L.M < M.M) : Module.finrank (IsLocalRing.ResidueField ↥R) ↥(L.mapIntermediate M) = 1

theorem BruhatTits.Lattice.mapIntermediate_eq_span'' {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) (M : Lattice R) {ϖ : ↥R} (hϖ : Irreducible ϖ) (h1 : M.M < b.toSubmodule) (h2 : ϖ • b.toSubmodule < M.M) (h3 : M.M ≠ (b.ntwist₂ hϖ 0 1).toSubmodule) : ∃ (α : ↥R), b.toLattice.mapIntermediate M = IsLocalRing.ResidueField ↥R ∙ (α • b.toQuotient' 0 + b.toQuotient' 1)

theorem BruhatTits.mapIntermediate_unipotent_smul {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (M : Lattice R) : b.toLattice.mapIntermediate (b.unipotent x • M) = Submodule.map (↑(b.unipotentResidue x)) (b.toLattice.mapIntermediate M)

The action of b.unipotent on lattices commutes with the projection L to L ⧸ ϖ L.

theorem BruhatTits.mapIntermediate_unipotent_smul' {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (b : Module.Basis (Fin 2) K (Fin 2 → K)) (x : ↥R) (M : Lattice R) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n : ℕ) : (b.ntwist₂ hϖ n 0).toLattice.mapIntermediate (b.unipotent (ϖ ^ n * x) • M) = Submodule.map (↑((b.ntwist₂ hϖ n 0).unipotentResidue x)) ((b.ntwist₂ hϖ n 0).toLattice.mapIntermediate M)

Variant of mapIntermediate_unipotent_smul for the lattice spanned by (ϖ ^ n • b₀, b₁).