# Nöbeling's theorem #

This file proves Nöbeling's theorem.

## Proof idea #

We follow the proof of theorem 5.4 in [Sch19], in which the idea is to embed S in a product of I copies of Bool for some sufficiently large I, and then to choose a well-ordering on I and use ordinal induction over that well-order. Here we can let I be the set of clopen subsets of S since S is totally separated.

The above means it suffices to prove the following statement: For a closed subset C of I → Bool, the -module LocallyConstant C ℤ is free.

For i : I, let e C i : LocallyConstant C ℤ denote the map fun f ↦ (if f.val i then 1 else 0).

The basis will consist of products e C iᵣ * ⋯ * e C i₁ with iᵣ > ⋯ > i₁ which cannot be written as linear combinations of lexicographically smaller products. We call this set GoodProducts C

What is proved by ordinal induction is that this set is linearly independent. The fact that it spans can be proved directly.

## Projection maps #

The purpose of this section is twofold.

Firstly, in the proof that the set GoodProducts C spans the whole module LocallyConstant C ℤ, we need to project C down to finite discrete subsets and write C as a cofiltered limit of those.

Secondly, in the inductive argument, we need to project C down to "smaller" sets satisfying the inductive hypothesis.

In this section we define the relevant projection maps and prove some compatibility results.

### Main definitions #

• Let J : I → Prop. Then Proj J : (I → Bool) → (I → Bool) is the projection mapping everything that satisfies J i to itself, and everything else to false.

• The image of C under Proj J is denoted π C J and the corresponding map C → π C J is called ProjRestrict. If J implies K we have a map ProjRestricts : π C K → π C J.

• spanCone_isLimit establishes that when C is compact, it can be written as a limit of its images under the maps Proj (· ∈ s) where s : Finset I.

def Profinite.NobelingProof.Proj {I : Type u} (J : IProp) [(i : I) → Decidable (J i)] :
(IBool)IBool

The projection mapping everything that satisfies J i to itself, and everything else to false

Equations
Instances For
@[simp]
theorem Profinite.NobelingProof.continuous_proj {I : Type u} (J : IProp) [(i : I) → Decidable (J i)] :
def Profinite.NobelingProof.π {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] :
Set (IBool)

The image of Proj π J

Equations
Instances For
@[simp]
theorem Profinite.NobelingProof.ProjRestrict_coe {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] :
∀ (a : C) (a_1 : I), a_1 = Profinite.NobelingProof.Proj J (a) a_1
def Profinite.NobelingProof.ProjRestrict {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] :
C

The restriction of Proj π J to a subset, mapping to its image.

Equations
Instances For
@[simp]
theorem Profinite.NobelingProof.continuous_projRestrict {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] :
theorem Profinite.NobelingProof.proj_eq_self {I : Type u} (J : IProp) [(i : I) → Decidable (J i)] {x : IBool} (h : ∀ (i : I), x i falseJ i) :
theorem Profinite.NobelingProof.proj_prop_eq_self {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] (hh : ∀ (i : I), xC, x i falseJ i) :
theorem Profinite.NobelingProof.proj_comp_of_subset {I : Type u} (J : IProp) (K : IProp) [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J iK i) :
theorem Profinite.NobelingProof.proj_eq_of_subset {I : Type u} (C : Set (IBool)) (J : IProp) (K : IProp) [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J iK i) :
@[simp]
theorem Profinite.NobelingProof.ProjRestricts_coe {I : Type u} (C : Set (IBool)) {J : IProp} {K : IProp} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J iK i) :
∀ (a : ) (a_1 : I), a_1 = Profinite.NobelingProof.Proj J (a) a_1
def Profinite.NobelingProof.ProjRestricts {I : Type u} (C : Set (IBool)) {J : IProp} {K : IProp} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J iK i) :

A variant of ProjRestrict with domain of the form π C K

Equations
Instances For
@[simp]
theorem Profinite.NobelingProof.continuous_projRestricts {I : Type u} (C : Set (IBool)) {J : IProp} {K : IProp} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J iK i) :
theorem Profinite.NobelingProof.surjective_projRestricts {I : Type u} (C : Set (IBool)) {J : IProp} {K : IProp} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J iK i) :
theorem Profinite.NobelingProof.projRestricts_eq_id {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] :
theorem Profinite.NobelingProof.projRestricts_eq_comp {I : Type u} (C : Set (IBool)) {J : IProp} {K : IProp} {L : IProp} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] [(i : I) → Decidable (L i)] (hJK : ∀ (i : I), J iK i) (hKL : ∀ (i : I), K iL i) :
theorem Profinite.NobelingProof.projRestricts_comp_projRestrict {I : Type u} (C : Set (IBool)) {J : IProp} {K : IProp} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J iK i) :
def Profinite.NobelingProof.iso_map {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] :
C(, )

The objectwise map in the isomorphism spanFunctorProfinite.indexFunctor

Equations
• = { toFun := fun (x : ) => fun (i : { i : I // J i }) => x i, , continuous_toFun := }
Instances For
theorem Profinite.NobelingProof.iso_map_bijective {I : Type u} (C : Set (IBool)) (J : IProp) [(i : I) → Decidable (J i)] :
noncomputable def Profinite.NobelingProof.spanFunctor {I : Type u} {C : Set (IBool)} (hC : ) [(s : ) → (i : I) → Decidable (i s)] :

For a given compact subset C of I → Bool, spanFunctor is the functor from the poset of finsets of I to Profinite, sending a finite subset set J to the image of C under the projection Proj J.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Profinite.NobelingProof.spanCone {I : Type u} {C : Set (IBool)} (hC : ) [(s : ) → (i : I) → Decidable (i s)] :

The limit cone on spanFunctor with point C.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def Profinite.NobelingProof.spanCone_isLimit {I : Type u} {C : Set (IBool)} (hC : ) [(s : ) → (i : I) → Decidable (i s)] :

spanCone is a limit cone.

Equations
• One or more equations did not get rendered due to their size.
Instances For

## Defining the basis #

Our proposed basis consists of products e C iᵣ * ⋯ * e C i₁ with iᵣ > ⋯ > i₁ which cannot be written as linear combinations of lexicographically smaller products. See below for the definition of e.

### Main definitions #

• For i : I, we let e C i : LocallyConstant C ℤ denote the map fun f ↦ (if f.val i then 1 else 0).

• Products I is the type of lists of decreasing elements of I, so a typical element is [i₁, i₂,..., iᵣ] with i₁ > i₂ > ... > iᵣ.

• Products.eval C is the C-evaluation of a list. It takes a term [i₁, i₂,..., iᵣ] : Products I and returns the actual product e C i₁ ··· e C iᵣ : LocallyConstant C ℤ.

• GoodProducts C is the set of Products I such that their C-evaluation cannot be written as a linear combination of evaluations of lexicographically smaller lists.

### Main results #

def Profinite.NobelingProof.e {I : Type u} (C : Set (IBool)) (i : I) :

e C i is the locally constant map from C : Set (I → Bool) to sending f to 1 if f.val i = true, and 0 otherwise.

Equations
• = { toFun := fun (f : C) => if f i = true then 1 else 0, isLocallyConstant := }
Instances For

Products I is the type of lists of decreasing elements of I, so a typical element is [i₁, i₂, ...] with i₁ > i₂ > .... We order Products I lexicographically, so [] < [i₁, ...], and [i₁, i₂, ...] < [j₁, j₂, ...] if either i₁ < j₁, or i₁ = j₁ and [i₂, ...] < [j₂, ...].

Terms m = [i₁, i₂, ..., iᵣ] of this type will be used to represent products of the form e C i₁ ··· e C iᵣ : LocallyConstant C ℤ . The function associated to m is m.eval.

Equations
Instances For
Equations
@[simp]
theorem Profinite.NobelingProof.Products.lt_iff_lex_lt {I : Type u} [] :
l < m List.Lex (fun (x x_1 : I) => x < x_1) l m
instance Profinite.NobelingProof.Products.instIsWellFoundedLt {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] :
IsWellFounded fun (x x_1 : ) => x < x_1
Equations
• =
def Profinite.NobelingProof.Products.eval {I : Type u} [] (C : Set (IBool)) :

The evaluation e C i₁ ··· e C iᵣ : C → ℤ of a formal product [i₁, i₂, ..., iᵣ].

Equations
• = ().prod
Instances For

The predicate on products which we prove picks out a basis of LocallyConstant C ℤ. We call such a product "good".

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Profinite.NobelingProof.Products.rel_head!_of_mem {I : Type u} [] [] {i : I} (hi : i l) :
theorem Profinite.NobelingProof.Products.head!_le_of_lt {I : Type u} [] [] (h : q < l) (hq : q []) :
def Profinite.NobelingProof.GoodProducts {I : Type u} [] (C : Set (IBool)) :

The set of good products.

Equations
Instances For
def Profinite.NobelingProof.GoodProducts.eval {I : Type u} [] (C : Set (IBool)) (l : ) :

Evaluation of good products.

Equations
Instances For

The image of the good products in the module LocallyConstant C ℤ

Equations
Instances For
noncomputable def Profinite.NobelingProof.GoodProducts.equiv_range {I : Type u} [] (C : Set (IBool)) :

The type of good products is equivalent to its image.

Equations
Instances For
theorem Profinite.NobelingProof.Products.eval_eq {I : Type u} [] (C : Set (IBool)) (x : C) :
= if il, x i = true then 1 else 0
theorem Profinite.NobelingProof.Products.evalFacProp {I : Type u} [] (C : Set (IBool)) (J : IProp) (h : al, J a) [(j : I) → Decidable (J j)] :
theorem Profinite.NobelingProof.Products.evalFacProps {I : Type u} [] (C : Set (IBool)) (J : IProp) (K : IProp) (h : al, J a) [(j : I) → Decidable (J j)] [(j : I) → Decidable (K j)] (hJK : ∀ (i : I), J iK i) :
theorem Profinite.NobelingProof.Products.prop_of_isGood {I : Type u} [] (C : Set (IBool)) (J : IProp) [(j : I) → Decidable (J j)] (a : I) :
a lJ a
theorem Profinite.NobelingProof.GoodProducts.span_iff_products {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) :

The good products span LocallyConstant C ℤ if and only all the products do.

## The good products span #

Most of the argument is developing an API for π C (· ∈ s) when s : Finset I; then the image of C is finite with the discrete topology. In this case, there is a direct argument that the good products span. The general result is deduced from this.

### Main theorems #

noncomputable def Profinite.NobelingProof.πJ {I : Type u} [] (C : Set (IBool)) (s : ) :

The -linear map induced by precomposition of the projection C → π C (· ∈ s).

Equations
Instances For
noncomputable instance Profinite.NobelingProof.instFintypeElemForallBoolπMemFinset {I : Type u} [] (C : Set (IBool)) (s : ) :
Fintype (Profinite.NobelingProof.π C fun (x : I) => x s)

π C (· ∈ s) is finite for a finite set s.

Equations
noncomputable def Profinite.NobelingProof.spanFinBasis {I : Type u} [] (C : Set (IBool)) (s : ) (x : (Profinite.NobelingProof.π C fun (x : I) => x s)) :

The Kronecker delta as a locally constant map from π C (· ∈ s) to .

Equations
Instances For
theorem Profinite.NobelingProof.spanFinBasis.span {I : Type u} [] (C : Set (IBool)) (s : ) :
def Profinite.NobelingProof.factors {I : Type u} [] (C : Set (IBool)) (s : ) (x : (Profinite.NobelingProof.π C fun (x : I) => x s)) :

A certain explicit list of locally constant maps. The theorem factors_prod_eq_basis shows that the product of the elements in this list is the delta function spanFinBasis C s x.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Profinite.NobelingProof.list_prod_apply {I : Type u} (C : Set (IBool)) (x : C) (l : List ()) :
l.prod x = ().prod
theorem Profinite.NobelingProof.factors_prod_eq_basis_of_eq {I : Type u} [] (C : Set (IBool)) (s : ) {x : (Profinite.NobelingProof.π C fun (x : I) => x s)} {y : (Profinite.NobelingProof.π C fun (x : I) => x s)} (h : y = x) :
().prod y = 1
theorem Profinite.NobelingProof.e_mem_of_eq_true {I : Type u} [] (C : Set (IBool)) (s : ) {x : (Profinite.NobelingProof.π C fun (x : I) => x s)} {a : I} (hx : x a = true) :
theorem Profinite.NobelingProof.one_sub_e_mem_of_false {I : Type u} [] (C : Set (IBool)) (s : ) {x : (Profinite.NobelingProof.π C fun (x : I) => x s)} {y : (Profinite.NobelingProof.π C fun (x : I) => x s)} {a : I} (ha : y a = true) (hx : x a = false) :
theorem Profinite.NobelingProof.factors_prod_eq_basis_of_ne {I : Type u} [] (C : Set (IBool)) (s : ) {x : (Profinite.NobelingProof.π C fun (x : I) => x s)} {y : (Profinite.NobelingProof.π C fun (x : I) => x s)} (h : y x) :
().prod y = 0
theorem Profinite.NobelingProof.factors_prod_eq_basis {I : Type u} [] (C : Set (IBool)) (s : ) (x : (Profinite.NobelingProof.π C fun (x : I) => x s)) :
().prod =

If s is finite, the product of the elements of the list factors C s x is the delta function at x.

theorem Profinite.NobelingProof.GoodProducts.finsupp_sum_mem_span_eval {I : Type u} [] (C : Set (IBool)) (s : ) {a : I} {as : List I} (ha : List.Chain' (fun (x x_1 : I) => x > x_1) (a :: as)) {c : } (hc : c.support {m : | m as}) :

If s is a finite subset of I, then the good products span.

theorem Profinite.NobelingProof.fin_comap_jointlySurjective {I : Type u} [] (C : Set (IBool)) (hC : ) (f : ) :
∃ (s : ) (g : LocallyConstant (Profinite.NobelingProof.π C fun (x : I) => x s) ), f = LocallyConstant.comap { toFun := Profinite.NobelingProof.ProjRestrict C fun (x : I) => x s, continuous_toFun := } g
theorem Profinite.NobelingProof.GoodProducts.span {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (hC : ) :

The good products span all of LocallyConstant C ℤ if C is closed.

## Relating elements of the well-order I with ordinals #

We choose a well-ordering on I. This amounts to regarding I as an ordinal, and as such it can be regarded as the set of all strictly smaller ordinals, allowing to apply ordinal induction.

### Main definitions #

• ord I i is the term i of I regarded as an ordinal.

• term I ho is a sufficiently small ordinal regarded as a term of I.

• contained C o is a predicate saying that C is "small" enough in relation to the ordinal o to satisfy the inductive hypothesis.

• P I is the predicate on ordinals about linear independence of good products, which the rest of this file is spent on proving by induction.

def Profinite.NobelingProof.ord (I : Type u) [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (i : I) :

A term of I regarded as an ordinal.

Equations
Instances For
noncomputable def Profinite.NobelingProof.term (I : Type u) [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
I

An ordinal regarded as a term of I.

Equations
Instances For
theorem Profinite.NobelingProof.term_ord_aux {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {i : I} (ho : < Ordinal.type fun (x x_1 : I) => x < x_1) :
@[simp]
theorem Profinite.NobelingProof.ord_term_aux {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.ord_term {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (i : I) :
def Profinite.NobelingProof.contained {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :

A predicate saying that C is "small" enough to satisfy the inductive hypothesis.

Equations
• = fC, ∀ (i : I), f i = true
Instances For
def Profinite.NobelingProof.P (I : Type u) [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (o : Ordinal.{u}) :

The predicate on ordinals which we prove by induction, see GoodProducts.P0, GoodProducts.Plimit and GoodProducts.linearIndependentAux in the section Induction below

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Profinite.NobelingProof.Products.prop_of_isGood_of_contained {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) (hsC : ) (i : I) (hi : i l) :

## The zero case of the induction #

In this case, we have contained C 0 which means that C is either empty or a singleton.

Equations
• =
Equations
• =

The empty list as a Products

Equations
• Profinite.NobelingProof.Products.nil = [],
Instances For
theorem Profinite.NobelingProof.Products.lt_nil_empty {I : Type u} [] :
{m : | m < Profinite.NobelingProof.Products.nil} =
theorem Profinite.NobelingProof.Products.isGood_nil {I : Type u} [] :
Profinite.NobelingProof.Products.isGood {fun (x : I) => false} Profinite.NobelingProof.Products.nil
theorem Profinite.NobelingProof.Products.span_nil_eq_top {I : Type u} [] :
Submodule.span (Profinite.NobelingProof.Products.eval {fun (x : I) => false} '' {Profinite.NobelingProof.Products.nil}) =

There is a unique GoodProducts for the singleton {fun _ ↦ false}.

Equations
• Profinite.NobelingProof.instUniqueSubtypeProductsIsGoodSingletonForallBoolSetFalse = { default := Profinite.NobelingProof.Products.nil, , uniq := }

## ℤ-linear maps induced by projections #

We define injective -linear maps between modules of the form LocallyConstant C ℤ induced by precomposition with the projections defined in the section Projections.

### Main result #

theorem Profinite.NobelingProof.contained_eq_proj {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) (h : ) :
C = Profinite.NobelingProof.π C fun (x : I) =>
theorem Profinite.NobelingProof.isClosed_proj {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) (hC : ) :
theorem Profinite.NobelingProof.contained_proj {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :
@[simp]
theorem Profinite.NobelingProof.πs_apply_apply {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) (g : LocallyConstant (Profinite.NobelingProof.π C fun (x : I) => ) ) :
∀ (a : C), ( g) a = g (Profinite.NobelingProof.ProjRestrict C (fun (x : I) => ) a)
noncomputable def Profinite.NobelingProof.πs {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :

The -linear map induced by precomposition of the projection C → π C (ord I · < o).

Equations
Instances For
theorem Profinite.NobelingProof.coe_πs {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) (f : LocallyConstant (Profinite.NobelingProof.π C fun (x : I) => ) ) :
( f) = f Profinite.NobelingProof.ProjRestrict C fun (x : I) =>
theorem Profinite.NobelingProof.injective_πs {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :
@[simp]
theorem Profinite.NobelingProof.πs'_apply_apply {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) (g : LocallyConstant (Profinite.NobelingProof.π C fun (x : I) => ) ) :
∀ (a : (Profinite.NobelingProof.π C fun (x : I) => )), ( g) a =
noncomputable def Profinite.NobelingProof.πs' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) :

The -linear map induced by precomposition of the projection π C (ord I · < o₂) → π C (ord I · < o₁) for o₁ ≤ o₂.

Equations
Instances For
theorem Profinite.NobelingProof.coe_πs' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) (f : LocallyConstant (Profinite.NobelingProof.π C fun (x : I) => ) ) :
( f).toFun = f.toFun
theorem Profinite.NobelingProof.injective_πs' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) :
theorem Profinite.NobelingProof.Products.lt_ord_of_lt {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {o : Ordinal.{u}} (h₁ : m < l) (h₂ : il, ) (i : I) :
i m
theorem Profinite.NobelingProof.Products.eval_πs {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hlt : il, ) :
theorem Profinite.NobelingProof.Products.eval_πs' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) (hlt : il, ) :
theorem Profinite.NobelingProof.Products.eval_πs_image {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hl : il, ) :
theorem Profinite.NobelingProof.Products.eval_πs_image' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) (hl : il, ) :
theorem Profinite.NobelingProof.Products.head_lt_ord_of_isGood {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) [] {o : Ordinal.{u}} (h : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => ) l) (hn : l []) :
theorem Profinite.NobelingProof.Products.isGood_mono {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) (hl : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => ) l) :

If l is good w.r.t. π C (ord I · < o₁) and o₁ ≤ o₂, then it is good w.r.t. π C (ord I · < o₂)

## 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 results #

def Profinite.NobelingProof.GoodProducts.smaller {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :
Set ()

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
noncomputable def Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) (x : (Profinite.NobelingProof.GoodProducts.range (Profinite.NobelingProof.π C fun (x : I) => ))) :

The map from the image of the GoodProducts in LocallyConstant (π C (ord I · < o)) ℤ to smaller C o

Equations
Instances For
theorem Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :
noncomputable def Profinite.NobelingProof.GoodProducts.range_equiv_smaller {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :

The equivalence from the image of the GoodProducts in LocallyConstant (π C (ord I · < o)) ℤ to smaller C o

Equations
Instances For
theorem Profinite.NobelingProof.GoodProducts.smaller_factorization {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :
(fun (p : ) => p) = fun (p : (Profinite.NobelingProof.GoodProducts.range (Profinite.NobelingProof.π C fun (x : I) => ))) => p
theorem Profinite.NobelingProof.GoodProducts.smaller_mono {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o₁ : Ordinal.{u}} {o₂ : Ordinal.{u}} (h : o₁ o₂) :
theorem Profinite.NobelingProof.Products.limitOrdinal {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o.IsLimit) :
theorem Profinite.NobelingProof.GoodProducts.union {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : ) :
= ⋃ (e : { o' : Ordinal.{u} // o' < o }),
def Profinite.NobelingProof.GoodProducts.range_equiv {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : ) :
(⋃ (e : { o' : Ordinal.{u} // o' < o }), )

The image of the GoodProducts in C is equivalent to the union of smaller C o' over all ordinals o' < o.

Equations
Instances For
theorem Profinite.NobelingProof.GoodProducts.range_equiv_factorization {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : ) :
(fun (p : (⋃ (e : { o' : Ordinal.{u} // o' < o }), )) => p) .toFun = fun (p : ) => p
theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : ) :
LinearIndependent fun (p : (⋃ (e : { o' : Ordinal.{u} // o' < o }), )) => p

## The successor case in the induction #

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].

### 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:

### Main results #

The main results in the section GoodProducts are as follows:

def Profinite.NobelingProof.C0 {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
Set (IBool)

The subset of C consisting of those elements whose o-th entry is false.

Equations
Instances For
def Profinite.NobelingProof.C1 {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
Set (IBool)

The subset of C consisting of those elements whose o-th entry is true.

Equations
Instances For
theorem Profinite.NobelingProof.isClosed_C0 {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.isClosed_C1 {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.contained_C1 {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.union_C0C1_eq {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
def Profinite.NobelingProof.C' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
Set (IBool)

The intersection of C0 and the projection of C1. We will apply the inductive hypothesis to this set.

Equations
Instances For
theorem Profinite.NobelingProof.isClosed_C' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.contained_C' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
noncomputable def Profinite.NobelingProof.SwapTrue {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (o : Ordinal.{u}) :
(IBool)IBool

Swapping the o-th coordinate to true.

Equations
Instances For
theorem Profinite.NobelingProof.continuous_swapTrue {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (o : Ordinal.{u}) :
theorem Profinite.NobelingProof.swapTrue_mem_C1 {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (f : (Profinite.NobelingProof.π () fun (x : I) => )) :
def Profinite.NobelingProof.CC'₀ {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
()C

The first way to map C' into C.

Equations
• = g,
Instances For
noncomputable def Profinite.NobelingProof.CC'₁ {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
()C

The second way to map C' into C.

Equations
Instances For
theorem Profinite.NobelingProof.continuous_CC'₀ {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.continuous_CC'₁ {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
noncomputable def Profinite.NobelingProof.Linear_CC'₀ {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :

The -linear map induced by precomposing with CC'₀

Equations
Instances For
noncomputable def Profinite.NobelingProof.Linear_CC'₁ {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :

The -linear map induced by precomposing with CC'₁

Equations
Instances For
noncomputable def Profinite.NobelingProof.Linear_CC' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :

The difference between Linear_CC'₁ and Linear_CC'₀.

Equations
Instances For
theorem Profinite.NobelingProof.CC_comp_zero {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (y : LocallyConstant (Profinite.NobelingProof.π C fun (x : I) => ) ) :
() ( y) = 0
theorem Profinite.NobelingProof.C0_projOrd {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) {x : IBool} (hx : ) :
Profinite.NobelingProof.Proj (fun (x : I) => ) x = x
theorem Profinite.NobelingProof.C1_projOrd {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) {x : IBool} (hx : ) :
theorem Profinite.NobelingProof.CC_exact {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) {f : } (hf : () f = 0) :
∃ (y : LocallyConstant (Profinite.NobelingProof.π C fun (x : I) => ) ), y = f
theorem Profinite.NobelingProof.succ_mono {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (o : Ordinal.{u}) :
theorem Profinite.NobelingProof.succ_exact {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
().Exact
def Profinite.NobelingProof.GoodProducts.MaxProducts {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :

Equations
Instances For
theorem Profinite.NobelingProof.GoodProducts.union_succ {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
def Profinite.NobelingProof.GoodProducts.sum_to {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :

The inclusion map from the sum of GoodProducts (π C (ord I · < o)) and (MaxProducts C ho) to Products I.

Equations
Instances For
theorem Profinite.NobelingProof.GoodProducts.injective_sum_to {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.GoodProducts.sum_to_range {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
noncomputable def Profinite.NobelingProof.GoodProducts.sum_equiv {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :

The equivalence from the sum of GoodProducts (π C (ord I · < o)) and (MaxProducts C ho) to GoodProducts C.

Equations
Instances For
theorem Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
= Sum.elim (fun (l : (Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => ))) => ) fun (l : ) =>
def Profinite.NobelingProof.GoodProducts.SumEval {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :

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
theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.GoodProducts.span_sum {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
= Set.range (Sum.elim (fun (l : (Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => ))) => ) fun (l : ) => )
theorem Profinite.NobelingProof.GoodProducts.square_commutes {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
theorem Profinite.NobelingProof.swapTrue_eq_true {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (x : IBool) :
theorem Profinite.NobelingProof.mem_C'_eq_false {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (x : IBool) :
x () = false

List.tail as a Products.

Equations
• l.Tail = (l).tail,
Instances For
theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) [] (hl : l []) (hlh : (l).head! = ) :
l = :: l.Tail
theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail' {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) [] (hl : l []) (hlh : (l).head! = ) (hlc : List.Chain' (fun (x x_1 : I) => x > x_1) ( :: l.Tail)) :
l = :: l.Tail, hlc
theorem Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) [] (l : ) :
theorem Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (l : ) :
l = :: (l).Tail
theorem Profinite.NobelingProof.Products.evalCons {I : Type u} [] (C : Set (IBool)) {l : List I} {a : I} (hla : List.Chain' (fun (x x_1 : I) => x > x_1) (a :: l)) :
theorem Profinite.NobelingProof.Products.max_eq_eval {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) [] (hl : l []) (hlh : (l).head! = ) :
theorem Profinite.NobelingProof.GoodProducts.max_eq_eval {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (l : ) :
theorem Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) :
(() fun (l : ) => ) = fun (l : ) => Profinite.NobelingProof.Products.eval () (l).Tail
theorem Profinite.NobelingProof.GoodProducts.chain'_cons_of_lt {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (l : ) (hq : q < (l).Tail) :
List.Chain' (fun (x x_1 : I) => x > x_1) ()
theorem Profinite.NobelingProof.GoodProducts.good_lt_maxProducts {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (q : (Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => ))) (l : ) :
List.Lex (fun (x x_1 : I) => x < x_1) q l
theorem Profinite.NobelingProof.GoodProducts.maxTail_isGood {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (l : ) (h₁ : Submodule.span (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => )))) :

Removing the leading o from a term of MaxProducts C yields a list which isGood with respect to C'.

noncomputable def Profinite.NobelingProof.GoodProducts.MaxToGood {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (h₁ : Submodule.span (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => )))) :

Given l : MaxProducts C ho, its Tail is a GoodProducts (C' C ho).

Equations
• = (l).Tail,
Instances For
theorem Profinite.NobelingProof.GoodProducts.maxToGood_injective {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (h₁ : Submodule.span (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => )))) :
theorem Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) {o : Ordinal.{u}} (hC : ) (hsC : ) (ho : o < Ordinal.type fun (x x_1 : I) => x < x_1) (h₁ : Submodule.span (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => )))) :
LinearIndependent (ι := ) (() Sum.inr)

## 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.P0 {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] :
theorem Profinite.NobelingProof.GoodProducts.Plimit {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (o : Ordinal.{u}) (ho : o.IsLimit) :
(o' < o, )
theorem Profinite.NobelingProof.GoodProducts.linearIndependentAux {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (μ : Ordinal.{u}) :
theorem Profinite.NobelingProof.GoodProducts.linearIndependent {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (hC : ) :
noncomputable def Profinite.NobelingProof.GoodProducts.Basis {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] (C : Set (IBool)) (hC : ) :

GoodProducts C as a -basis for LocallyConstant C ℤ.

Equations
Instances For
theorem Profinite.NobelingProof.Nobeling_aux {I : Type u} [] [IsWellOrder I fun (x x_1 : I) => x < x_1] {S : Profinite} {ι : S.toTopIBool} (hι : ) :

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 // }Bool

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

Equations
Instances For

The map Nobeling.ι is a closed embedding.

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

Equations
• =