Documentation

LeanPool.BruhatTits.Graph.Orientation

Orientation on the Bruhat-Tits tree #

The Bruhat-Tits tree admits a natural orientation, by which we mean a partition of the vertices in odd and even, which can be interpreted as a direction on the edges.

We say an R-lattice L is even if the additive valuation of the determinant of an R-basis of L is even. This is independent of the choice of the basis (see BruhatTits.Lattice.zaddVal_det_eq_of_basis) and invariant under homothety (see BruhatTits.Lattice.isEven_smul_of_isEven). A vertex is then even if a (equivalently all) representative is even.

Finally, we define a ±1-valued weight function on the vertices by sending even vertices to 1 and odd vertices to -1. This will be later used to define the harmonic co-chains on the Bruhat-Tits tree (see BruhatTits.Harmonic.Application).

SL₂ action #

While the GL₂ action is transitive, the SL₂ action preserves the orientation, i.e. it preserves evenness of vertices (see BruhatTits.isEven_specialLinearGroup_smul_iff).

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

The valuation associated to a lattice is the additive valuation of the determinant of a basis. This is independent of the choice of a basis (see BruhatTits.Lattice.zaddVal_det_eq_of_basis), but not invariant under homothety.

Equations

L.valuation = zaddVal (Matrix.GeneralLinearGroup.det L.basis.toGL)

Instances For

theorem BruhatTits.Lattice.zaddVal_det_eq_of_basis {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} (b₁ b₂ : Module.Basis (Fin 2) ↥R ↥L.M) :

zaddVal (Matrix.GeneralLinearGroup.det b₁.toGL) = zaddVal (Matrix.GeneralLinearGroup.det b₂.toGL)

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

A lattice is called even, if the determinant of the matrix spanned by a basis has even additive valuation.

Equations

L.IsEven = Even L.valuation

Instances For

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

A lattice is called odd, if the determinant of the matrix spanned by a basis has odd additive valuation.

Equations

L.IsOdd = Odd L.valuation

Instances For

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

L.IsOdd ↔ ¬L.IsEven

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

L.IsEven ↔ ∃ (b : Module.Basis (Fin 2) ↥R ↥L.M), Even (zaddVal (Matrix.GeneralLinearGroup.det b.toGL))

theorem BruhatTits.Lattice.isEven_iff' {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) :

L.IsEven ↔ ∃ (b : Module.Basis (Fin 2) K (Fin 2 → K)), b.toLattice = L ∧ Even (zaddVal (Matrix.GeneralLinearGroup.det b.toGeneralLinearGroup))

theorem BruhatTits.Lattice.isEven_smul_of_isEven {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} (a : Kˣ) (h : L.IsEven) :

(a • L).IsEven

theorem BruhatTits.Lattice.isEven_smul_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (L : Lattice R) (a : Kˣ) :

(a • L).IsEven ↔ L.IsEven

theorem BruhatTits.Lattice.isEven_iff_of_isSimilar {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {M L : Lattice R} (h : IsSimilar R M L) :

M.IsEven ↔ L.IsEven

theorem BruhatTits.Lattice.isOdd_iff_of_isSimilar {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {M L : Lattice R} (h : IsSimilar R M L) :

M.IsOdd ↔ L.IsOdd

@[implicit_reducible]

noncomputable instance BruhatTits.instMulActionSpecialLinearGroupFinOfNatNatLattice {K : Type u_1} [Field K] {R : Subring K} :

MulAction (Matrix.SpecialLinearGroup (Fin 2) K) (Lattice R)

Equations

BruhatTits.instMulActionSpecialLinearGroupFinOfNatNatLattice = MulAction.compHom (BruhatTits.Lattice R) Matrix.SpecialLinearGroup.toGL

@[implicit_reducible]

noncomputable instance BruhatTits.instMulActionSpecialLinearGroupFinOfNatNatVertices {K : Type u_1} [Field K] {R : Subring K} :

MulAction (Matrix.SpecialLinearGroup (Fin 2) K) (Vertices R)

Equations

BruhatTits.instMulActionSpecialLinearGroupFinOfNatNatVertices = MulAction.compHom (BruhatTits.Vertices R) Matrix.SpecialLinearGroup.toGL

@[simp]

theorem BruhatTits.specialLinearGroupToGL_smul {K : Type u_1} [Field K] {R : Subring K} (g : Matrix.SpecialLinearGroup (Fin 2) K) (L : Lattice R) :

Matrix.SpecialLinearGroup.toGL g • L = g • L

noncomputable def BruhatTits.IsEven {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (x : Vertices R) :

A vertex ⟦L⟧ is called even, if L is even. This is independent of the choice of L.

Equations

BruhatTits.IsEven x = Quotient.lift BruhatTits.Lattice.IsEven ⋯ x

Instances For

noncomputable def BruhatTits.IsOdd {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (x : Vertices R) :

A vertex ⟦L⟧ is called odd, if L is odd. This is independent of the choice of L.

Equations

BruhatTits.IsOdd x = Quotient.lift BruhatTits.Lattice.IsOdd ⋯ x

Instances For

theorem BruhatTits.isOdd_iff_notEven {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (x : Vertices R) :

IsOdd x ↔ ¬IsEven x

@[simp]

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

IsEven ⟦L⟧ ↔ L.IsEven

noncomputable def BruhatTits.BTweight {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] (A : Type u_2) [CommRing A] (x : Vertices R) :

A canonical weight function on the vertices of the BT tree: Even vertices have weight 1 and odd vertices have weight -1.

Equations

BruhatTits.BTweight A x = if BruhatTits.IsEven x then 1 else -1

Instances For

instance BruhatTits.instGraphActionVerticesSpecialLinearGroupFinOfNatNatBTgraph {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] :

GraphAction (Matrix.SpecialLinearGroup (Fin 2) K) BTgraph

theorem BruhatTits.Lattice.isEven_specialLinearGroup_smul {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} (h : L.IsEven) (g : Matrix.SpecialLinearGroup (Fin 2) K) :

(g • L).IsEven

@[simp]

theorem BruhatTits.Lattice.isEven_specialLinearGroup_smul_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {L : Lattice R} (g : Matrix.SpecialLinearGroup (Fin 2) K) :

(g • L).IsEven ↔ L.IsEven

theorem BruhatTits.isEven_specialLinearGroup_smul {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x : Vertices R} (h : IsEven x) (g : Matrix.SpecialLinearGroup (Fin 2) K) :

IsEven (g • x)

@[simp]

theorem BruhatTits.isEven_specialLinearGroup_smul_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x : Vertices R} (g : Matrix.SpecialLinearGroup (Fin 2) K) :

IsEven (g • x) ↔ IsEven x

theorem BruhatTits.isOdd_specialLinearGroup_smul_iff {K : Type u_1} [Field K] {R : Subring K} [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] {x : Vertices R} (g : Matrix.SpecialLinearGroup (Fin 2) K) :

IsOdd (g • x) ↔ IsOdd x