Surjectivity of the Bruhat-Tits Laplacian

In this file we show that the Laplacian of the Bruhat-Tits tree is surjective.

noncomputable def BruhatTits.BTlaplace {K : Type u_1} [Field K] (R : Subring K) [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] [Finite (IsLocalRing.ResidueField ↥R)] (A : Type u_2) (M : Type u_3) [CommRing A] [AddCommGroup M] [Module A M] : (↑BTgraph.edgeSet → M) →ₗ[A] Vertices R → M

The Laplacian on the Bruhat-Tits tree with coefficients in any A-module M.

Equations

• BruhatTits.BTlaplace R A M = SimpleGraph.laplaceLinearMap (BruhatTits.BTweight A)

theorem BruhatTits.BTlaplace_surjective {K : Type u_1} [Field K] (R : Subring K) [IsDiscreteValuationRing ↥R] [IsFractionRing (↥R) K] [Finite (IsLocalRing.ResidueField ↥R)] (A : Type u_2) (M : Type u_3) [CommRing A] [AddCommGroup M] [Module A M] : Function.Surjective ⇑(BTlaplace R A M)