The zero and limit cases in the induction for Nöbeling's theorem #
This file proves the zero and limit cases of the ordinal induction used in the proof of Nöbeling's theorem. See the section docstrings for more information.
For the overall proof outline see Mathlib.Topology.Category.Profinite.Nobeling.Basic
.
References #
- [Sch19], Theorem 5.4.
The zero case of the induction #
In this case, we have contained C 0
which means that C
is either empty or a singleton.
The empty list as a Products
Equations
Instances For
There is a unique GoodProducts
for the singleton {fun _ ↦ false}
.
Equations
- Profinite.NobelingProof.instUniqueSubtypeProductsIsGoodSingletonForallBoolSetFalse = { default := ⟨Profinite.NobelingProof.Products.nil, ⋯⟩, uniq := ⋯ }
The limit case of the induction #
We relate linear independence in LocallyConstant (π C (ord I · < o')) ℤ
with linear independence
in LocallyConstant C ℤ
, where contained C o
and o' < o
.
When o
is a limit ordinal, we prove that the good products in LocallyConstant C ℤ
are linearly
independent if and only if a certain directed union is linearly independent. Each term in this
directed union is in bijection with the good products w.r.t. π C (ord I · < o')
for an ordinal
o' < o
, and these are linearly independent by the inductive hypothesis.
Main definitions #
GoodProducts.smaller
is the image of good products coming from a smaller ordinal.GoodProducts.range_equiv
: The image of theGoodProducts
inC
is equivalent to the union ofsmaller C o'
over all ordinalso' < o
.
Main results #
Products.limitOrdinal
: foro
a limit ordinal such thatcontained C o
, a productl
is good w.r.t.C
iff it there exists an ordinalo' < o
such thatl
is good w.r.t.π C (ord I · < o')
.GoodProducts.linearIndependent_iff_union_smaller
is the result mentioned above, that the good products are linearly independent iff a directed union is.
The image of the GoodProducts
for π C (ord I · < o)
in LocallyConstant C ℤ
. The name smaller
refers to the setting in which we will use this, when we are mapping in GoodProducts
from a
smaller set, i.e. when o
is a smaller ordinal than the one C
is "contained" in.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The map from the image of the GoodProducts
in LocallyConstant (π C (ord I · < o)) ℤ
to
smaller C o
Equations
Instances For
The equivalence from the image of the GoodProducts
in LocallyConstant (π C (ord I · < o)) ℤ
to
smaller C o
Equations
Instances For
The image of the GoodProducts
in C
is equivalent to the union of smaller C o'
over all
ordinals o' < o
.