The good products span

Most of the argument is developing an API for π C (· ∈ s) when s : Finset I; then the image of C is finite with the discrete topology. In this case, there is a direct argument that the good products span. The general result is deduced from this.

For the overall proof outline see Mathlib/Topology/Category/Profinite/Nobeling/Basic.lean.

Main theorems

• GoodProducts.spanFin : The good products span the locally constant functions on π C (· ∈ s) if s is finite.
• GoodProducts.span : The good products span LocallyConstant C ℤ for every closed subset C.

References

• [scholze2019condensed], Theorem 5.4.

noncomputable def Profinite.NobelingProof.πJ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) : LocallyConstant ↑(π C fun (x : I) => x ∈ s) ℤ →ₗ[ℤ] LocallyConstant ↑C ℤ

The ℤ-linear map induced by precomposition of the projection C → π C (· ∈ s).

theorem Profinite.NobelingProof.eval_eq_πJ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (l : Products I) (hl : Products.isGood (π C fun (x : I) => x ∈ s) l) : Products.eval C l = (πJ C s) (Products.eval (π C fun (x : I) => x ∈ s) l)

noncomputable instance Profinite.NobelingProof.instFintypeElemForallBoolπMemFinset {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) : Fintype ↑(π C fun (x : I) => x ∈ s)

π C (· ∈ s) is finite for a finite set s.

noncomputable def Profinite.NobelingProof.spanFinBasis {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (x : ↑(π C fun (x : I) => x ∈ s)) : LocallyConstant ↑(π C fun (x : I) => x ∈ s) ℤ

The Kronecker delta as a locally constant map from π C (· ∈ s) to ℤ.

theorem Profinite.NobelingProof.spanFinBasis.span {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) : ⊤ ≤ Submodule.span ℤ (Set.range (spanFinBasis C s))

def Profinite.NobelingProof.factors {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (x : ↑(π C fun (x : I) => x ∈ s)) : List (LocallyConstant ↑(π C fun (x : I) => x ∈ s) ℤ)

A certain explicit list of locally constant maps. The theorem factors_prod_eq_basis shows that the product of the elements in this list is the delta function spanFinBasis C s x.

theorem Profinite.NobelingProof.list_prod_apply {I : Type u_1} (C : Set (I → Bool)) (x : ↑C) (l : List (LocallyConstant ↑C ℤ)) : l.prod x = (List.map (⇑(LocallyConstant.evalMonoidHom x)) l).prod

theorem Profinite.NobelingProof.factors_prod_eq_basis_of_eq {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x y : ↑(π C fun (x : I) => x ∈ s)} (h : y = x) : (factors C s x).prod y = 1

theorem Profinite.NobelingProof.e_mem_of_eq_true {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x : ↑(π C fun (x : I) => x ∈ s)} {a : I} (hx : ↑x a = true) : e (π C fun (x : I) => x ∈ s) a ∈ factors C s x

theorem Profinite.NobelingProof.one_sub_e_mem_of_false {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x y : ↑(π C fun (x : I) => x ∈ s)} {a : I} (ha : ↑y a = true) (hx : ↑x a = false) : 1 - e (π C fun (x : I) => x ∈ s) a ∈ factors C s x

theorem Profinite.NobelingProof.factors_prod_eq_basis_of_ne {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x y : ↑(π C fun (x : I) => x ∈ s)} (h : y ≠ x) : (factors C s x).prod y = 0

theorem Profinite.NobelingProof.factors_prod_eq_basis {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (x : ↑(π C fun (x : I) => x ∈ s)) : (factors C s x).prod = spanFinBasis C s x

If s is finite, the product of the elements of the list factors C s x is the delta function at x.

theorem Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {a : I} {as : List I} (ha : List.Chain' (fun (x1 x2 : I) => x1 > x2) (a :: as)) {c : Products I →₀ ℤ} (hc : ↑c.support ⊆ {m : Products I | ↑m ≤ as}) : (c.sum fun (a_1 : Products I) (b : ℤ) => e (π C fun (x : I) => x ∈ s) a * b • Products.eval (π C fun (x : I) => x ∈ s) a_1) ∈ Submodule.span ℤ (Products.eval (π C fun (x : I) => x ∈ s) '' {m : Products I | ↑m ≤ a :: as})

@[deprecated Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval (since := "2025-04-06")]

theorem Profinite.NobelingProof.GoodProducts.finsupp_sum_mem_span_eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {a : I} {as : List I} (ha : List.Chain' (fun (x1 x2 : I) => x1 > x2) (a :: as)) {c : Products I →₀ ℤ} (hc : ↑c.support ⊆ {m : Products I | ↑m ≤ as}) : (c.sum fun (a_1 : Products I) (b : ℤ) => e (π C fun (x : I) => x ∈ s) a * b • Products.eval (π C fun (x : I) => x ∈ s) a_1) ∈ Submodule.span ℤ (Products.eval (π C fun (x : I) => x ∈ s) '' {m : Products I | ↑m ≤ a :: as})

Alias of Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval.

theorem Profinite.NobelingProof.GoodProducts.spanFin {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) [WellFoundedLT I] : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun (x : I) => x ∈ s)))

If s is a finite subset of I, then the good products span.

theorem Profinite.NobelingProof.fin_comap_jointlySurjective {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (hC : IsClosed C) (f : LocallyConstant ↑C ℤ) : ∃ (s : Finset I) (g : LocallyConstant ↑(π C fun (x : I) => x ∈ s) ℤ), f = LocallyConstant.comap { toFun := ProjRestrict C fun (x : I) => x ∈ s, continuous_toFun := ⋯ } g

theorem Profinite.NobelingProof.GoodProducts.span {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (hC : IsClosed C) : ⊤ ≤ Submodule.span ℤ (Set.range (eval C))

The good products span all of LocallyConstant C ℤ if C is closed.