Nöbeling's theorem

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

Main result

• LocallyConstant.freeOfProfinite: Nöbeling's theorem. For S : Profinite, the ℤ-module LocallyConstant S ℤ is free.

References

• [Sch19], Theorem 5.4.

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:

• GoodProducts.linearIndependent which says that GoodProducts C is linearly independent when C is closed.

We also define

• GoodProducts.Basis which uses GoodProducts.linearIndependent and GoodProducts.span to define a basis for LocallyConstant C ℤ

theorem Profinite.NobelingProof.GoodProducts.P0 {I : Type u} [LinearOrder I] [WellFoundedLT I] : P I 0

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

theorem Profinite.NobelingProof.GoodProducts.linearIndependentAux {I : Type u} [LinearOrder I] [WellFoundedLT I] (μ : Ordinal.{u}) : P I μ

theorem Profinite.NobelingProof.GoodProducts.linearIndependent {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (hC : IsClosed C) : LinearIndependent ℤ (eval C)

noncomputable def Profinite.NobelingProof.GoodProducts.Basis {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (hC : IsClosed C) : Module.Basis ↑(GoodProducts C) ℤ (LocallyConstant ↑C ℤ)

GoodProducts C as a ℤ-basis for LocallyConstant C ℤ.

Equations

• Profinite.NobelingProof.GoodProducts.Basis C hC = Module.Basis.mk ⋯ ⋯

theorem Profinite.NobelingProof.Nobeling_aux {I : Type u} [LinearOrder I] [WellFoundedLT I] {S : Profinite} {ι : ↑S.toTop → I → Bool} (hι : Topology.IsClosedEmbedding ι) : Module.Free ℤ (LocallyConstant ↑S.toTop ℤ)

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

• Profinite.Nobeling.ι S s C = decide (s ∈ ↑C)

theorem Profinite.Nobeling.isClosedEmbedding (S : Profinite) : Topology.IsClosedEmbedding (ι S)

The map Nobeling.ι is a closed embedding.

instance LocallyConstant.freeOfProfinite (S : Profinite) : Module.Free ℤ (LocallyConstant ↑S.toTop ℤ)

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