Documentation

Mathlib.Topology.Category.Profinite.Nobeling.Span

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 #

References #

noncomputable def Profinite.NobelingProof.πJ {I : Type u} (C : Set (IBool)) [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).

Equations
Instances For
    theorem Profinite.NobelingProof.eval_eq_πJ {I : Type u} (C : Set (IBool)) [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 (IBool)) [LinearOrder I] (s : Finset I) :
    Fintype (π C fun (x : I) => x s)

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

    Equations
    noncomputable def Profinite.NobelingProof.spanFinBasis {I : Type u} (C : Set (IBool)) [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 .

    Equations
    Instances For
      def Profinite.NobelingProof.factors {I : Type u} (C : Set (IBool)) [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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem Profinite.NobelingProof.list_prod_apply {I : Type u_1} (C : Set (IBool)) (x : C) (l : List (LocallyConstant C )) :
        theorem Profinite.NobelingProof.factors_prod_eq_basis_of_eq {I : Type u} (C : Set (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [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

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