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 #
LocallyConstant.freeOfProfinite
: Nöbeling's theorem. ForS : Profinite
, theℤ
-moduleLocallyConstant 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 thatGoodProducts C
is linearly independent whenC
is closed.
We also define
GoodProducts.Basis
which usesGoodProducts.linearIndependent
andGoodProducts.span
to define a basis forLocallyConstant 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 : o.IsLimit)
:
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)
:
_root_.Basis ↑(GoodProducts C) ℤ (LocallyConstant ↑C ℤ)
GoodProducts C
as a ℤ
-basis for LocallyConstant C ℤ
.
Equations
Instances For
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.
The map Nobeling.ι
is a closed embedding.
@[deprecated Profinite.Nobeling.isClosedEmbedding (since := "2024-10-26")]
Alias of Profinite.Nobeling.isClosedEmbedding
.
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
.