Basic constructions and operations on lattices

In this file we provide the infrastructure for going back and forth between K-bases of Fin 2 → K and R-lattices. Also we provide operations on bases, such as twisting by units of K and permutations of the basis.

The main definition is Basis.toLattice which, given a basis b of Fin 2 → K constructs the lattice spanned by the entries of b. The API is built around this definition in the following sense: Every operation on lattices comes with API lemmas showing the interaction with Basis.toLattice, reducing it to an operation on bases. In a general situation, try to use the induction principle of equality (i.e. the subst tactic) to replace arbitrary lattices with b.toLattice for a suitable basis.

Most constructions work for an arbitrary subring R of a field K.

Main definitions

• Basis.toSubmodule: Given a K-basis b of ι → K, this is the R-submodule of ι → K spanned by K. This is a lattice (toSubmodule_isLattice).
• Basis.toLattice: Basis.toSubmodule as a lattice. See the docstring for more details.
• Basis.twist: Let f be a tuple of integers and let ϖ be a uniformizer. The twist of a basis b by f is defined as b i ↦ ϖ.val ^ f i • b i. We provide variants for ι = Fin 2 and for natural exponents. Generally, try to bring all lattices in the context in the form of b.twist hϖ f for fixed b and varying f, in order to simplify calculations.

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

From a ι-indexed basis b of ι → K, we obtain an R submodule of ι → K generated by the entries of b.

Equations

• b.toSubmodule = Submodule.span (↥R) (Set.range ⇑b)

theorem Module.Basis.self_mem_toSubmodule {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} (b : Basis ι K (ι → K)) (i : ι) : b i ∈ b.toSubmodule

theorem Module.Basis.toSubmodule_isLattice {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Finite ι] (b : Basis ι K (ι → K)) : IsLattice b.toSubmodule

noncomputable def Module.Basis.toLattice {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) : BruhatTits.Lattice R

Given a K-basis of K^2, this is the R-lattice generated by the entries of b.

This is the normal form of a lattice in our API and for every operation on lattices suitable simp lemmas should be provided for lattices given by Basis.toLattice.

If possible, in proofs use the induction principle of equality (i.e. the subst tactic) to replace all occurring lattices by invocations of Basis.toLattice.

Equations

• b.toLattice = { M := b.toSubmodule, isLattice := ⋯ }

@[simp]

theorem Module.Basis.toLattice_module {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) : b.toLattice.M = b.toSubmodule

noncomputable def Module.Basis.twist' {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) (f : ι → Kˣ) : Basis ι K (ι → K)

If b is a K-basis of ι → K and f : ι → Kˣ a family of invertible elements of K, this is the basis of ι → K obtained by multiplying i-th entry of b by f i.

Equations

• b.twist' f = Module.Basis.mk ⋯ ⋯

@[simp]

theorem Module.Basis.twist'_apply {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) (f : ι → Kˣ) (i : ι) : (b.twist' f) i = f i • b i

noncomputable def Module.Basis.twist {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f : ι → ℤ) : Basis ι K (ι → K)

Given integer exponents f and a uniformizer ϖ, we may twist a basis b by b i ↦ ϖ.val ^ f i • b i.

Equations

• b.twist hϖ f = b.twist' fun (i : ι) => Units.mk0 ↑ϖ ⋯ ^ f i

@[simp]

theorem Module.Basis.twist_apply {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f : ι → ℤ) (i : ι) : (b.twist hϖ f) i = ↑ϖ ^ f i • b i

noncomputable def Module.Basis.ntwist {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f : ι → ℕ) : Basis ι K (ι → K)

twist but for natural exponents.

Equations

• b.ntwist hϖ f = b.twist hϖ fun (i : ι) => ↑(f i)

@[simp]

theorem Module.Basis.ntwist_apply {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f : ι → ℕ) (i : ι) : (b.ntwist hϖ f) i = ϖ ^ f i • b i

noncomputable def Module.Basis.twist₂ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℤ) : Basis (Fin 2) K (Fin 2 → K)

twist specialized to dimension two.

Equations

• b.twist₂ hϖ n m = b.twist hϖ fun (i : Fin 2) => match i with | 0 => n | 1 => m

@[simp]

theorem Module.Basis.twist₂_apply₀ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℤ) : (b.twist₂ hϖ n m) 0 = ↑ϖ ^ n • b 0

@[simp]

theorem Module.Basis.twist₂_apply₁ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℤ) : (b.twist₂ hϖ n m) 1 = ↑ϖ ^ m • b 1

noncomputable def Module.Basis.ntwist₂ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℕ) : Basis (Fin 2) K (Fin 2 → K)

twist₂ for natural exponents.

Equations

• b.ntwist₂ hϖ n m = b.twist₂ hϖ ↑n ↑m

@[simp]

theorem Module.Basis.ntwist₂_apply₀ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℕ) : (b.ntwist₂ hϖ n m) 0 = ϖ ^ n • b 0

@[simp]

theorem Module.Basis.ntwist₂_apply₁ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℕ) : (b.ntwist₂ hϖ n m) 1 = ϖ ^ m • b 1

theorem Module.Basis.twist_le_twist_iff {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f g : ι → ℤ) : (b.twist hϖ f).toSubmodule ≤ (b.twist hϖ g).toSubmodule ↔ g ≤ f

theorem Module.Basis.twist_eq_twist_iff {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f g : ι → ℤ) : (b.twist hϖ f).toSubmodule = (b.twist hϖ g).toSubmodule ↔ g = f

theorem Module.Basis.twist_lt_twist_iff {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f g : ι → ℤ) : (b.twist hϖ f).toSubmodule < (b.twist hϖ g).toSubmodule ↔ g ≤ f ∧ ∃ (i : ι), g i < f i

theorem Module.Basis.twist₂_le_twist₂_iff {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n₁ m₁ n₂ m₂ : ℤ) : (b.twist₂ hϖ n₁ m₁).toSubmodule ≤ (b.twist₂ hϖ n₂ m₂).toSubmodule ↔ n₂ ≤ n₁ ∧ m₂ ≤ m₁

theorem Module.Basis.twist₂_eq_twist₂_iff {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n₁ m₁ n₂ m₂ : ℤ) : (b.twist₂ hϖ n₁ m₁).toSubmodule = (b.twist₂ hϖ n₂ m₂).toSubmodule ↔ n₂ = n₁ ∧ m₂ = m₁

theorem Module.Basis.ntwist₂_le_ntwist₂_iff {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n₁ m₁ n₂ m₂ : ℕ) : (b.ntwist₂ hϖ n₁ m₁).toSubmodule ≤ (b.ntwist₂ hϖ n₂ m₂).toSubmodule ↔ n₂ ≤ n₁ ∧ m₂ ≤ m₁

noncomputable def Module.Basis.fromSubmoduleOfIsLattice {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)

If M is a lattice, every R-basis of M is also a K-basis of ι → K.

Equations

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

@[simp]

theorem Module.Basis.fromSubmoduleOfIsLattice_apply {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) (i : ι) : b.fromSubmoduleOfIsLattice i = ↑(b i)

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

If M is an R-lattice, every R-basis of M is also a K-basis of Fin 2 → K.

Equations

• b.fromLattice = b.fromSubmoduleOfIsLattice

@[simp]

theorem Module.Basis.fromLattice_apply {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] {M : BruhatTits.Lattice R} (b : Basis (Fin 2) ↥R ↥M.M) (i : Fin 2) : b.fromLattice i = ↑(b i)

@[simp]

theorem Module.Basis.toSubmodule_fromLattice {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) : b.fromSubmoduleOfIsLattice.toSubmodule = M

@[simp]

theorem Module.Basis.toLattice_fromLattice {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] {M : BruhatTits.Lattice R} (b : Basis (Fin 2) ↥R ↥M.M) : b.fromLattice.toLattice = M

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

If b is a K-basis of ι → K, it is naturally an R-basis of the R-submodule generated by the entries of b.

Equations

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

@[simp]

theorem Module.Basis.restrict_apply {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [IsFractionRing (↥R) K] [Fintype ι] (b : Basis ι K (ι → K)) (i : ι) : ↑(b.restrict i) = b i

noncomputable def Module.Basis.restrictToLattice {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) : Basis (Fin 2) ↥R ↥b.toLattice.M

If b is a K-basis of Fin 2 → K, it is naturally an R-basis of the R-lattice generated by the entries of b.

Equations

• b.restrictToLattice = b.restrict

theorem Module.Basis.restrictToLattice_apply {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) (i : Fin 2) : ↑(b.restrictToLattice i) = b i

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

Scalar multiplication by GL ι K on ι-indexed bases of ι → K.

Equations

• Module.Basis.smulGL g b = b.map (Matrix.GeneralLinearGroup.toLin g).toLinearEquiv

@[implicit_reducible]

noncomputable instance Module.Basis.instSMulGeneralLinearGroupForallLeanPool {K : Type u_1} [Field K] {ι : Type u_2} [DecidableEq ι] [Fintype ι] : SMul (GL ι K) (Basis ι K (ι → K))

Equations

• Module.Basis.instSMulGeneralLinearGroupForallLeanPool = { smul := fun (g : GL ι K) (b : Module.Basis ι K (ι → K)) => Module.Basis.smulGL g b }

theorem Module.Basis.smulGL_def {K : Type u_1} [Field K] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : GL ι K) (b : Basis ι K (ι → K)) : g • b = b.map (Matrix.GeneralLinearGroup.toLin g).toLinearEquiv

@[simp]

theorem Module.Basis.smulGL_apply {K : Type u_1} [Field K] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : GL ι K) (b : Basis ι K (ι → K)) (i : ι) : (g • b) i = (↑g).mulVec (b i)

theorem Module.Basis.smulGL_toSubmodule {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : GL ι K) (b : Basis ι K (ι → K)) : (g • b).toSubmodule = g • b.toSubmodule

theorem Module.Basis.smulGL_toLattice {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) K) (b : Basis (Fin 2) K (Fin 2 → K)) : (g • b).toLattice = g • b.toLattice

theorem Module.Basis.smulGL_twist {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : GL ι K) (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f : ι → ℤ) : g • b.twist hϖ f = (g • b).twist hϖ f

theorem Module.Basis.smulGL_toGeneralLinearGroup {K : Type u_1} [Field K] {ι : Type u_2} [DecidableEq ι] [Fintype ι] (g : GL ι K) (b : Basis ι K (ι → K)) : (g • b).toGeneralLinearGroup = g * b.toGeneralLinearGroup

noncomputable def Module.Basis.smul' {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (a : Kˣ) (b : Basis ι K (ι → K)) : Basis ι K (ι → K)

Scalar multiplication of units of K on bases of ι → K by twisting.

Equations

• Module.Basis.smul' a b = b.twist' fun (x : ι) => a

@[implicit_reducible]

noncomputable instance Module.Basis.instSMulUnitsForallLeanPool {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] : SMul Kˣ (Basis ι K (ι → K))

Equations

• Module.Basis.instSMulUnitsForallLeanPool = { smul := Module.Basis.smul' }

theorem Module.Basis.smul'_def {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (a : Kˣ) (b : Basis ι K (ι → K)) : a • b = b.twist' fun (x : ι) => a

@[simp]

theorem Module.Basis.smul'_apply {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] (a : Kˣ) (b : Basis ι K (ι → K)) (i : ι) : (a • b) i = a • b i

theorem Module.Basis.smul_toSubmodule {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (a : Kˣ) (b : Basis ι K (ι → K)) : a • b.toSubmodule = (a • b).toSubmodule

theorem Module.Basis.smul_twist {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f : ι → ℤ) : ϖ • (b.twist hϖ f).toSubmodule = (b.twist hϖ (f + 1)).toSubmodule

theorem Module.Basis.smul_ntwist₂ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℕ) : ϖ • (b.ntwist₂ hϖ n m).toSubmodule = (b.ntwist₂ hϖ (n + 1) (m + 1)).toSubmodule

theorem Module.Basis.smul_pow_twist {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (f : ι → ℤ) (k : ℤ) : ↑ϖ ^ k • (b.twist hϖ f).toSubmodule = (b.twist hϖ (f + ↑k)).toSubmodule

theorem Module.Basis.smul_pow_twist₂ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m k : ℤ) : ↑ϖ ^ k • (b.twist₂ hϖ n m).toSubmodule = (b.twist₂ hϖ (n + k) (m + k)).toSubmodule

theorem Module.Basis.twist_zero {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] (b : Basis ι K (ι → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : b.twist hϖ 0 = b

theorem Module.Basis.ntwist₂_zero_zero {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) : b.ntwist₂ hϖ 0 0 = b

theorem Module.Basis.ntwist₂_toSubmodule_le_ntwist₂_toSubmodule {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) {n₁ m₁ n₂ m₂ : ℕ} (hn : n₂ ≤ n₁) (hm : m₂ ≤ m₁) : (b.ntwist₂ hϖ n₁ m₁).toSubmodule ≤ (b.ntwist₂ hϖ n₂ m₂).toSubmodule

theorem Module.Basis.ntwist₂_toSubmodule_le {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℕ) : (b.ntwist₂ hϖ n m).toSubmodule ≤ b.toSubmodule

theorem Module.Basis.ntwist₂_ntwist₂ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n₁ m₁ n₂ m₂ : ℕ) : (b.ntwist₂ hϖ n₁ m₁).ntwist₂ hϖ n₂ m₂ = b.ntwist₂ hϖ (n₁ + n₂) (m₁ + m₂)

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

Given a basis b of ι → K and a permutation of the basis vectors, this is the matrix representing the K-automorphisms induced by the permutation.

Equations

• b.permMatrix e = Matrix.GeneralLinearGroup.toLin.symm (LinearMap.GeneralLinearGroup.ofLinearEquiv (b.equiv (b.reindex e) (Equiv.refl ι)))

theorem Module.Basis.toLinear_symm_ofLinearEquiv_mulVec {K : Type u_1} [Field K] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : (ι → K) ≃ₗ[K] ι → K) (x : ι → K) : (↑(Matrix.GeneralLinearGroup.toLin.symm (LinearMap.GeneralLinearGroup.ofLinearEquiv e))).mulVec x = e x

theorem Module.Basis.permMatrix_smul_toSubmodule {K : Type u_1} [Field K] {R : Subring K} {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Basis ι K (ι → K)) (e : ι ≃ ι) : b.permMatrix e • b.toSubmodule = (b.reindex e).toSubmodule

@[simp]

theorem Module.Basis.swap₂_apply₀ : Module.Basis.swap₂✝ 0 = 1

@[simp]

theorem Module.Basis.swap₂_apply₁ : Module.Basis.swap₂✝ 1 = 0

@[simp]

theorem Module.Basis.swap₂_symm : Module.Basis.swap₂✝.symm = Module.Basis.swap₂✝

noncomputable def Module.Basis.swap {K : Type u_1} [Field K] (b : Basis (Fin 2) K (Fin 2 → K)) : Basis (Fin 2) K (Fin 2 → K)

Swap the entries of a basis of Fin 2 → K.

Equations

• b.swap = b.reindex Module.Basis.swap₂✝

@[simp]

theorem Module.Basis.swap_apply₀ {K : Type u_1} [Field K] (b : Basis (Fin 2) K (Fin 2 → K)) : b.swap 0 = b 1

@[simp]

theorem Module.Basis.swap_apply₁ {K : Type u_1} [Field K] (b : Basis (Fin 2) K (Fin 2 → K)) : b.swap 1 = b 0

theorem Module.Basis.swap_toSubmodule {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) : b.swap.toSubmodule = b.toSubmodule

noncomputable def Module.Basis.swapMatrix {K : Type u_1} [Field K] (b : Basis (Fin 2) K (Fin 2 → K)) : GL (Fin 2) K

The swap matrix associated to a basis b: the invertible matrix acting on Fin 2 → K by swapping the entries of b.

Equations

• b.swapMatrix = b.permMatrix Module.Basis.swap₂✝

theorem Module.Basis.swapMatrix_smul_toSubmodule {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) : b.swapMatrix • b.toSubmodule = b.swap.toSubmodule

theorem Module.Basis.swapMatrix_smul_ntwist₂ {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (n m : ℕ) : b.swapMatrix • (b.ntwist₂ hϖ n m).toSubmodule = (b.ntwist₂ hϖ m n).toSubmodule

@[implicit_reducible]

noncomputable instance Module.Basis.instSMulSubtypeMemSubringForallFinOfNatNatSubmoduleToSubmodule {K : Type u_1} [Field K] {R : Subring K} (b : Basis (Fin 2) K (Fin 2 → K)) : SMul ↥R ↥b.toSubmodule

Equations

• b.instSMulSubtypeMemSubringForallFinOfNatNatSubmoduleToSubmodule = b.toSubmodule.smul

theorem Module.Basis.is_linear_comb_of_mem_ntwist {K : Type u_1} [Field K] {R : Subring K} [IsFractionRing (↥R) K] (b : Basis (Fin 2) K (Fin 2 → K)) {ϖ : ↥R} (hϖ : Irreducible ϖ) (y : ↥b.toSubmodule) {n m : ℕ} (hy : ↑y ∈ (b.ntwist₂ hϖ n m).toSubmodule) : ∃ (α : ↥R) (β : ↥R), y = α • ϖ ^ n • b.restrict 0 + β • ϖ ^ m • b.restrict 1

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

The standard R-lattice R ⊕ R.

Equations

• Lattice.standard R = (Pi.basisFun K (Fin 2)).toLattice

theorem Lattice.standard_M {K : Type u_1} [Field K] {R : Subring K} : (standard R).M = ((Algebra.linearMap (↥R) K).compLeft (Fin 2)).range

@[simp]

theorem map_subtype_smul_standard_eq_standard {K : Type u_1} [Field K] {R : Subring K} (g : GL (Fin 2) ↥R) : (Matrix.GeneralLinearGroup.map R.subtype) g • Lattice.standard R = Lattice.standard R

theorem IsLattice.of_le_of_isLattice_right {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] (L : Submodule (↥R) (Fin 2 → K)) [IsLattice L] (M : Submodule (↥R) (Fin 2 → K)) (h₁ : M ≤ L) (h₂ : IsLocalRing.maximalIdeal ↥R • L ≤ M) : IsLattice M