Documentation

Mathlib.Topology.Category.Profinite.Nobeling.Induction

Nöbeling's theorem #

This file proves Nöbeling's theorem. For the overall proof outline see Mathlib.Topology.Category.Profinite.Nobeling.Basic.

Main result #

References #

The induction #

Here we put together the results of the sections Zero, Limit and Successor to prove the predicate P I o holds for all ordinals o, and conclude with the main result:

We also define

theorem Profinite.NobelingProof.GoodProducts.Plimit {I : Type u} [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) (ho : o.IsLimit) :
(∀ o' < o, P I o')P I o

GoodProducts C as a -basis for LocallyConstant C ℤ.

Equations
Instances For

    Given a profinite set S and a closed embedding S → (I → Bool), the -module LocallyConstant C ℤ is free.

    noncomputable def Profinite.Nobeling.ι (S : Profinite) :
    S.toTop{ C : Set S.toTop // IsClopen C }Bool

    The embedding S → (I → Bool) where I is the set of clopens of S.

    Equations
    Instances For
      @[deprecated Profinite.Nobeling.isClosedEmbedding (since := "2024-10-26")]

      Alias of Profinite.Nobeling.isClosedEmbedding.


      The map Nobeling.ι is a closed embedding.

      Nöbeling's theorem. The -module LocallyConstant S ℤ is free for every S : Profinite.