The successor case in the induction for Nöbeling's theorem #
Here we assume that o
is an ordinal such that contained C (o+1)
and o < I
. The element in I
corresponding to o
is called term I ho
, but in this informal docstring we refer to it simply as
o
.
This section follows the proof in [Sch19] quite closely. A translation of the notation there is as follows:
[scholze2019condensed] | This file
`S₀` |`C0`
`S₁` |`C1`
`\overline{S}` |`π C (ord I · < o)
`\overline{S}'` |`C'`
The left map in the exact sequence |`πs`
The right map in the exact sequence |`Linear_CC'`
When comparing the proof of the successor case in Theorem 5.4 in [Sch19] with this proof, one should read the phrase "is a basis" as "is linearly independent". Also, the short exact sequence in [Sch19] is only proved to be left exact here (indeed, that is enough since we are only proving linear independence).
This section is split into two sections. The first one, ExactSequence
defines the left exact
sequence mentioned in the previous paragraph (see succ_mono
and succ_exact
). It corresponds to
the penultimate paragraph of the proof in [Sch19]. The second one, GoodProducts
corresponds to the last paragraph in the proof in [Sch19].
For the overall proof outline see Mathlib.Topology.Category.Profinite.Nobeling.Basic
.
Main definitions #
The main definitions in the section ExactSequence
are all just notation explained in the table
above.
The main definitions in the section GoodProducts
are as follows:
MaxProducts
: the set of good products that contain the ordinalo
(since we havecontained C (o+1)
, these all start witho
).GoodProducts.sum_equiv
: the equivalence betweenGoodProducts C
and the disjoint union ofMaxProducts C
andGoodProducts (π C (ord I · < o))
.
Main results #
- The main results in the section
ExactSequence
aresucc_mono
andsucc_exact
which together say that the sequence given byπs
andLinear_CC'
is left exact:
wheref g 0 --→ LocallyConstant (π C (ord I · < o)) ℤ --→ LocallyConstant C ℤ --→ LocallyConstant C' ℤ
f
isπs
andg
isLinear_CC'
.
The main results in the section GoodProducts
are as follows:
Products.max_eq_eval
says that the linear map on the right in the exact sequence, i.e.Linear_CC'
, takes the evaluation of a term ofMaxProducts
to the evaluation of the corresponding list with the leadingo
removed.GoodProducts.maxTail_isGood
says that removing the leadingo
from a term ofMaxProducts C
yields a list whichisGood
with respect toC'
.
References #
- [Sch19], Theorem 5.4.
The subset of C
consisting of those elements whose o
-th entry is false
.
Equations
Instances For
The subset of C
consisting of those elements whose o
-th entry is true
.
Equations
Instances For
The intersection of C0
and the projection of C1
. We will apply the inductive hypothesis to
this set.
Equations
- Profinite.NobelingProof.C' C ho = Profinite.NobelingProof.C0 C ho ∩ Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun (x : I) => Profinite.NobelingProof.ord I x < o
Instances For
Swapping the o
-th coordinate to true
.
Equations
- Profinite.NobelingProof.SwapTrue o f i = if Profinite.NobelingProof.ord I i = o then true else f i
Instances For
The first way to map C'
into C
.
Equations
- Profinite.NobelingProof.CC'₀ C ho g = ⟨↑g, ⋯⟩
Instances For
The second way to map C'
into C
.
Equations
- Profinite.NobelingProof.CC'₁ C hsC ho g = ⟨Profinite.NobelingProof.SwapTrue o ↑g, ⋯⟩
Instances For
The ℤ
-linear map induced by precomposing with CC'₀
Equations
- Profinite.NobelingProof.Linear_CC'₀ C ho = LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.CC'₀ C ho, continuous_toFun := ⋯ }
Instances For
The ℤ
-linear map induced by precomposing with CC'₁
Equations
- Profinite.NobelingProof.Linear_CC'₁ C hsC ho = LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.CC'₁ C hsC ho, continuous_toFun := ⋯ }
Instances For
The difference between Linear_CC'₁
and Linear_CC'₀
.
Equations
- Profinite.NobelingProof.Linear_CC' C hsC ho = Profinite.NobelingProof.Linear_CC'₁ C hsC ho - Profinite.NobelingProof.Linear_CC'₀ C ho
Instances For
The GoodProducts
in C
that contain o
(they necessarily start with o
, see
GoodProducts.head!_eq_o_of_maxProducts
)
Equations
Instances For
The inclusion map from the sum of GoodProducts (π C (ord I · < o))
and
(MaxProducts C ho)
to Products I
.
Instances For
The equivalence from the sum of GoodProducts (π C (ord I · < o))
and
(MaxProducts C ho)
to GoodProducts C
.
Equations
Instances For
Let
N := LocallyConstant (π C (ord I · < o)) ℤ
M := LocallyConstant C ℤ
P := LocallyConstant (C' C ho) ℤ
ι := GoodProducts (π C (ord I · < o))
ι' := GoodProducts (C' C ho')
v : ι → N := GoodProducts.eval (π C (ord I · < o))
Then SumEval C ho
is the map u
in the diagram below. It is linearly independent if and only if
GoodProducts.eval C
is, see linearIndependent_iff_sum
. The top row is the exact sequence given
by succ_exact
and succ_mono
. The left square commutes by GoodProducts.square_commutes
.
0 --→ N --→ M --→ P
↑ ↑ ↑
v| u| |
ι → ι ⊕ ι' ← ι'
Equations
- One or more equations did not get rendered due to their size.
Instances For
List.tail
as a Products
.
Instances For
Removing the leading o
from a term of MaxProducts C
yields a list which isGood
with respect to
C'
.
Given l : MaxProducts C ho
, its Tail
is a GoodProducts (C' C ho)
.
Equations
- Profinite.NobelingProof.GoodProducts.MaxToGood C hC hsC ho h₁ l = ⟨(↑l).Tail, ⋯⟩