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
.
Main theorems #
GoodProducts.spanFin
: The good products span the locally constant functions onπ C (· ∈ s)
ifs
is finite.GoodProducts.span
: The good products spanLocallyConstant C ℤ
for every closed subsetC
.
References #
- [Sch19], Theorem 5.4.
The ℤ
-linear map induced by precomposition of the projection C → π C (· ∈ s)
.
Equations
- Profinite.NobelingProof.πJ C s = LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.ProjRestrict C fun (x : I) => x ∈ s, continuous_toFun := ⋯ }
Instances For
π C (· ∈ s)
is finite for a finite set s
.
Equations
- Profinite.NobelingProof.instFintypeElemForallBoolπMemFinset C s = Fintype.ofInjective (fun (x : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)) (j : { x : I // x ∈ s }) => ↑x ↑j) ⋯
The Kronecker delta as a locally constant map from π C (· ∈ s)
to ℤ
.
Equations
- Profinite.NobelingProof.spanFinBasis C s x = { toFun := fun (y : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)) => if y = x then 1 else 0, isLocallyConstant := ⋯ }
Instances For
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If s
is finite, the product of the elements of the list factors C s x
is the delta function at x
.
Alias of Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval
.
If s
is a finite subset of I
, then the good products span.
The good products span all of LocallyConstant C ℤ
if C
is closed.