Finite projections of abstract measures

An abstract measure can be pushed to a finite discrete quotient by recording its values on the fibres. This file constructs that linear projection, proves its functoriality under refinement, identifies measures on a finite discrete space with finitely supported coefficient functions, and proves that binary projections already determine a measure on a profinite space.

The construction follows the finite-coefficient description in Rodrigues Jacinto and Williams, An introduction to p-adic L-functions, Sections 3.2--3.3.

noncomputable def AbstractMeasure.finiteProjection {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (q : C(X, A)) : AbstractMeasure X R R →ₗ[R] A →₀ R

The finite projection of a measure records its values on all fibres of q.

@[simp]

theorem AbstractMeasure.finiteProjection_apply {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (q : C(X, A)) (μ : AbstractMeasure X R R) (a : A) : ((finiteProjection q) μ) a = μ (q.fiberIndicator a)

theorem AbstractMeasure.apply_comp_eq_sum_finiteProjection {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Fintype A] [DiscreteTopology A] (q : C(X, A)) (μ : AbstractMeasure X R R) (g : A → R) : μ ((ContinuousMap.equivFnOfDiscrete.symm g).comp q) = ∑ a : A, g a * ((finiteProjection q) μ) a

Integration of a function factoring through a finite quotient is the corresponding finite sum against the projected coefficients.

@[simp]

theorem AbstractMeasure.finiteProjection_dirac {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (q : C(X, A)) (x : X) : (finiteProjection q) (dirac R x) = Finsupp.single (q x) 1

The finite projection of a Dirac measure is the point mass at the image of its support.

theorem AbstractMeasure.finiteProjection_apply_of_notMem_range {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] {q : C(X, A)} (μ : AbstractMeasure X R R) {a : A} (ha : a ∉ Set.range ⇑q) : ((finiteProjection q) μ) a = 0

A fibre of q that is empty carries no mass.

@[simp]

theorem AbstractMeasure.finiteProjection_map {X : Type u_1} {A : Type u_2} {B : Type u_3} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (φ : C(B, X)) (q : C(X, A)) (μ : AbstractMeasure B R R) : (finiteProjection q) ((map φ) μ) = (finiteProjection (q.comp φ)) μ

The finite projection of a pushforward is the finite projection along the composite.

theorem AbstractMeasure.finiteProjection_comp {X : Type u_1} {A : Type u_2} {B : Type u_3} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace B] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [Finite B] [DiscreteTopology A] [DiscreteTopology B] (q : C(X, A)) (t : C(A, B)) (μ : AbstractMeasure X R R) : (finiteProjection (t.comp q)) μ = Finsupp.mapDomain (⇑t) ((finiteProjection q) μ)

Finite projection is functorial when one finite quotient refines another.

@[simp]

theorem AbstractMeasure.sum_finiteProjection {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (q : C(X, A)) (μ : AbstractMeasure X R R) : (((finiteProjection q) μ).sum fun (x : A) (r : R) => r) = μ 1

The sum of all finite coefficients is the total mass of the measure.

noncomputable def AbstractMeasure.ofFiniteCoefficients {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] : (A →₀ R) →ₗ[R] AbstractMeasure A R R

A finitely supported coefficient function on a finite discrete space defines the corresponding finite linear combination of Dirac measures.

@[simp]

theorem AbstractMeasure.ofFiniteCoefficients_single {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] (a : A) (r : R) : ofFiniteCoefficients (Finsupp.single a r) = r • dirac R a

@[simp]

theorem AbstractMeasure.ofFiniteCoefficients_apply {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] (c : A →₀ R) (f : C(A, R)) : (ofFiniteCoefficients c) f = c.sum fun (a : A) (r : R) => r * f a

Evaluating the measure associated to finite coefficients pairs the coefficients with the values of the test function.

@[simp]

theorem AbstractMeasure.finiteProjection_id_ofFiniteCoefficients {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (c : A →₀ R) : (finiteProjection (ContinuousMap.id A)) (ofFiniteCoefficients c) = c

Finite projection along the identity recovers the coefficients used to build a measure.

@[simp]

theorem AbstractMeasure.ofFiniteCoefficients_finiteProjection_id {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (μ : AbstractMeasure A R R) : ofFiniteCoefficients ((finiteProjection (ContinuousMap.id A)) μ) = μ

Reconstructing a measure on a finite discrete space from its identity projection returns the original measure.

noncomputable def AbstractMeasure.finiteProjectionEquiv {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] : AbstractMeasure A R R ≃ₗ[R] A →₀ R

Measures on a finite discrete space are equivalent to their coefficient functions.

@[simp]

theorem AbstractMeasure.finiteProjectionEquiv_apply {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (μ : AbstractMeasure A R R) : finiteProjectionEquiv μ = (finiteProjection (ContinuousMap.id A)) μ

@[simp]

theorem AbstractMeasure.finiteProjectionEquiv_symm_apply {A : Type u_2} {R : Type u_4} [TopologicalSpace A] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [Finite A] [DiscreteTopology A] (c : A →₀ R) : finiteProjectionEquiv.symm c = ofFiniteCoefficients c

theorem AbstractMeasure.finiteProjection_ext {X : Type u_1} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace R] [CommRing R] [IsTopologicalRing R] [CompactSpace X] [T2Space X] [TotallyDisconnectedSpace X] [T2Space R] (μ ν : AbstractMeasure X R R) (h : ∀ (q : C(X, Fin 2)), (finiteProjection q) μ = (finiteProjection q) ν) : μ = ν

A measure on a profinite space is determined by its projections to binary discrete quotients.

theorem AbstractMeasure.continuous_finiteProjection {X : Type u_1} {A : Type u_2} {R : Type u_4} [TopologicalSpace X] [TopologicalSpace A] [NormedCommRing R] [Finite A] [DiscreteTopology A] (q : C(X, A)) : Continuous fun (μ : AbstractMeasure X R R) (a : A) => ((finiteProjection q) μ) a

Finite projection is weakly continuous when its coefficients carry the product topology.