Nöbeling's theorem

This file proves Nöbeling's theorem.

Main result

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

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.

References

• [Sch19], Theorem 5.4.

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 : I → Prop) [(i : I) → Decidable (J i)] : (I → Bool) → I → Bool

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

Equations

• Profinite.NobelingProof.Proj J c i = if J i then c i else false

@[simp]

theorem Profinite.NobelingProof.continuous_proj {I : Type u} (J : I → Prop) [(i : I) → Decidable (J i)] : Continuous (Profinite.NobelingProof.Proj J)

def Profinite.NobelingProof.π {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : Set (I → Bool)

The image of Proj π J

Equations

• Profinite.NobelingProof.π C J = Profinite.NobelingProof.Proj J '' C

def Profinite.NobelingProof.ProjRestrict {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : ↑C → ↑(Profinite.NobelingProof.π C J)

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

Equations

• Profinite.NobelingProof.ProjRestrict C J = Set.MapsTo.restrict (Profinite.NobelingProof.Proj J) C (Profinite.NobelingProof.π C J) ⋯

@[simp]

theorem Profinite.NobelingProof.ProjRestrict_coe {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] (a✝ : ↑C) (a✝¹ : I) : ↑(Profinite.NobelingProof.ProjRestrict C J a✝) a✝¹ = Profinite.NobelingProof.Proj J (↑a✝) a✝¹

@[simp]

theorem Profinite.NobelingProof.continuous_projRestrict {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : Continuous (Profinite.NobelingProof.ProjRestrict C J)

theorem Profinite.NobelingProof.proj_eq_self {I : Type u} (J : I → Prop) [(i : I) → Decidable (J i)] {x : I → Bool} (h : ∀ (i : I), x i ≠ false → J i) : Profinite.NobelingProof.Proj J x = x

theorem Profinite.NobelingProof.proj_prop_eq_self {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] (hh : ∀ (i : I), ∀ x ∈ C, x i ≠ false → J i) : Profinite.NobelingProof.π C J = C

theorem Profinite.NobelingProof.proj_comp_of_subset {I : Type u} (J K : I → Prop) [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) : Profinite.NobelingProof.Proj J ∘ Profinite.NobelingProof.Proj K = Profinite.NobelingProof.Proj J

theorem Profinite.NobelingProof.proj_eq_of_subset {I : Type u} (C : Set (I → Bool)) (J K : I → Prop) [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) : Profinite.NobelingProof.π (Profinite.NobelingProof.π C K) J = Profinite.NobelingProof.π C J

def Profinite.NobelingProof.ProjRestricts {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) : ↑(Profinite.NobelingProof.π C K) → ↑(Profinite.NobelingProof.π C J)

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

Equations

• Profinite.NobelingProof.ProjRestricts C h = ⇑(Homeomorph.setCongr ⋯) ∘ Profinite.NobelingProof.ProjRestrict (Profinite.NobelingProof.π C K) J

@[simp]

theorem Profinite.NobelingProof.ProjRestricts_coe {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) (a✝ : ↑(Profinite.NobelingProof.π C K)) (a✝¹ : I) : ↑(Profinite.NobelingProof.ProjRestricts C h a✝) a✝¹ = Profinite.NobelingProof.Proj J (↑a✝) a✝¹

@[simp]

theorem Profinite.NobelingProof.continuous_projRestricts {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) : Continuous (Profinite.NobelingProof.ProjRestricts C h)

theorem Profinite.NobelingProof.surjective_projRestricts {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) : Function.Surjective (Profinite.NobelingProof.ProjRestricts C h)

theorem Profinite.NobelingProof.projRestricts_eq_id {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : Profinite.NobelingProof.ProjRestricts C ⋯ = id

theorem Profinite.NobelingProof.projRestricts_eq_comp {I : Type u} (C : Set (I → Bool)) {J K L : I → Prop} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] [(i : I) → Decidable (L i)] (hJK : ∀ (i : I), J i → K i) (hKL : ∀ (i : I), K i → L i) : Profinite.NobelingProof.ProjRestricts C hJK ∘ Profinite.NobelingProof.ProjRestricts C hKL = Profinite.NobelingProof.ProjRestricts C ⋯

theorem Profinite.NobelingProof.projRestricts_comp_projRestrict {I : Type u} (C : Set (I → Bool)) {J K : I → Prop} [(i : I) → Decidable (J i)] [(i : I) → Decidable (K i)] (h : ∀ (i : I), J i → K i) : Profinite.NobelingProof.ProjRestricts C h ∘ Profinite.NobelingProof.ProjRestrict C K = Profinite.NobelingProof.ProjRestrict C J

def Profinite.NobelingProof.iso_map {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : C(↑(Profinite.NobelingProof.π C J), ↑(Profinite.IndexFunctor.obj C J))

The objectwise map in the isomorphism spanFunctor ≅ Profinite.indexFunctor.

Equations

• Profinite.NobelingProof.iso_map C J = { toFun := fun (x : ↑(Profinite.NobelingProof.π C J)) => ⟨fun (i : { i : I // J i }) => ↑x ↑i, ⋯⟩, continuous_toFun := ⋯ }

theorem Profinite.NobelingProof.iso_map_bijective {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : Function.Bijective ⇑(Profinite.NobelingProof.iso_map C J)

noncomputable def Profinite.NobelingProof.spanFunctor {I : Type u} {C : Set (I → Bool)} [(s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C) : CategoryTheory.Functor (Finset I)ᵒᵖ Profinite

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.

noncomputable def Profinite.NobelingProof.spanCone {I : Type u} {C : Set (I → Bool)} [(s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C) : CategoryTheory.Limits.Cone (Profinite.NobelingProof.spanFunctor hC)

The limit cone on spanFunctor with point C.

Equations

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

noncomputable def Profinite.NobelingProof.spanCone_isLimit {I : Type u} {C : Set (I → Bool)} [(s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C) : CategoryTheory.Limits.IsLimit (Profinite.NobelingProof.spanCone hC)

spanCone is a limit cone.

Equations

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

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

• Products.evalFacProp and Products.evalFacProps establish the fact that Products.eval interacts nicely with the projection maps from the previous section.

• GoodProducts.span_iff_products: the good products span LocallyConstant C ℤ iff all the products span LocallyConstant C ℤ.

def Profinite.NobelingProof.e {I : Type u} (C : Set (I → Bool)) (i : I) : LocallyConstant ↑C ℤ

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

• Profinite.NobelingProof.e C i = { toFun := fun (f : ↑C) => if ↑f i = true then 1 else 0, isLocallyConstant := ⋯ }

def Profinite.NobelingProof.Products (I : Type u_1) [LinearOrder I] : Type u_1

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

• Profinite.NobelingProof.Products I = { l : List I // List.Chain' (fun (x1 x2 : I) => x1 > x2) l }

instance Profinite.NobelingProof.Products.instLinearOrder {I : Type u} [LinearOrder I] : LinearOrder (Profinite.NobelingProof.Products I)

Equations

• Profinite.NobelingProof.Products.instLinearOrder = inferInstanceAs (LinearOrder { l : List I // List.Chain' (fun (x1 x2 : I) => x1 > x2) l })

@[simp]

theorem Profinite.NobelingProof.Products.lt_iff_lex_lt {I : Type u} [LinearOrder I] (l m : Profinite.NobelingProof.Products I) : l < m ↔ List.Lex (fun (x1 x2 : I) => x1 < x2) ↑l ↑m

instance Profinite.NobelingProof.Products.instWellFoundedLT {I : Type u} [LinearOrder I] [WellFoundedLT I] : WellFoundedLT (Profinite.NobelingProof.Products I)

Equations

• ⋯ = ⋯

def Profinite.NobelingProof.Products.eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (l : Profinite.NobelingProof.Products I) : LocallyConstant ↑C ℤ

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

Equations

• Profinite.NobelingProof.Products.eval C l = (List.map (Profinite.NobelingProof.e C) ↑l).prod

def Profinite.NobelingProof.Products.isGood {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (l : Profinite.NobelingProof.Products I) : Prop

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.

theorem Profinite.NobelingProof.Products.rel_head!_of_mem {I : Type u} [LinearOrder I] [Inhabited I] {i : I} {l : Profinite.NobelingProof.Products I} (hi : i ∈ ↑l) : i ≤ (↑l).head!

theorem Profinite.NobelingProof.Products.head!_le_of_lt {I : Type u} [LinearOrder I] [Inhabited I] {q l : Profinite.NobelingProof.Products I} (h : q < l) (hq : ↑q ≠ []) : (↑q).head! ≤ (↑l).head!

def Profinite.NobelingProof.GoodProducts {I : Type u} (C : Set (I → Bool)) [LinearOrder I] : Set (Profinite.NobelingProof.Products I)

The set of good products.

Equations

• Profinite.NobelingProof.GoodProducts C = {l : Profinite.NobelingProof.Products I | Profinite.NobelingProof.Products.isGood C l}

def Profinite.NobelingProof.GoodProducts.eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (l : { l : Profinite.NobelingProof.Products I // Profinite.NobelingProof.Products.isGood C l }) : LocallyConstant ↑C ℤ

Evaluation of good products.

Equations

• Profinite.NobelingProof.GoodProducts.eval C l = Profinite.NobelingProof.Products.eval C ↑l

theorem Profinite.NobelingProof.GoodProducts.injective {I : Type u} (C : Set (I → Bool)) [LinearOrder I] : Function.Injective (Profinite.NobelingProof.GoodProducts.eval C)

def Profinite.NobelingProof.GoodProducts.range {I : Type u} (C : Set (I → Bool)) [LinearOrder I] : Set (LocallyConstant ↑C ℤ)

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

Equations

• Profinite.NobelingProof.GoodProducts.range C = Set.range (Profinite.NobelingProof.GoodProducts.eval C)

noncomputable def Profinite.NobelingProof.GoodProducts.equiv_range {I : Type u} (C : Set (I → Bool)) [LinearOrder I] : ↑(Profinite.NobelingProof.GoodProducts C) ≃ ↑(Profinite.NobelingProof.GoodProducts.range C)

The type of good products is equivalent to its image.

Equations

• Profinite.NobelingProof.GoodProducts.equiv_range C = Equiv.ofInjective (Profinite.NobelingProof.GoodProducts.eval C) ⋯

theorem Profinite.NobelingProof.GoodProducts.equiv_toFun_eq_eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] : (Profinite.NobelingProof.GoodProducts.equiv_range C).toFun = Set.rangeFactorization (Profinite.NobelingProof.GoodProducts.eval C)

theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range {I : Type u} (C : Set (I → Bool)) [LinearOrder I] : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔ LinearIndependent ℤ fun (p : ↑(Profinite.NobelingProof.GoodProducts.range C)) => ↑p

theorem Profinite.NobelingProof.Products.eval_eq {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (l : Profinite.NobelingProof.Products I) (x : ↑C) : (Profinite.NobelingProof.Products.eval C l) x = if ∀ i ∈ ↑l, ↑x i = true then 1 else 0

theorem Profinite.NobelingProof.Products.evalFacProp {I : Type u} (C : Set (I → Bool)) [LinearOrder I] {l : Profinite.NobelingProof.Products I} (J : I → Prop) (h : ∀ a ∈ ↑l, J a) [(j : I) → Decidable (J j)] : ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘ Profinite.NobelingProof.ProjRestrict C J = ⇑(Profinite.NobelingProof.Products.eval C l)

theorem Profinite.NobelingProof.Products.evalFacProps {I : Type u} (C : Set (I → Bool)) [LinearOrder I] {l : Profinite.NobelingProof.Products I} (J K : I → Prop) (h : ∀ a ∈ ↑l, J a) [(j : I) → Decidable (J j)] [(j : I) → Decidable (K j)] (hJK : ∀ (i : I), J i → K i) : ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C J) l) ∘ Profinite.NobelingProof.ProjRestricts C hJK = ⇑(Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C K) l)

theorem Profinite.NobelingProof.Products.prop_of_isGood {I : Type u} (C : Set (I → Bool)) [LinearOrder I] {l : Profinite.NobelingProof.Products I} (J : I → Prop) [(j : I) → Decidable (J j)] (h : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C J) l) (a : I) : a ∈ ↑l → J a

theorem Profinite.NobelingProof.GoodProducts.span_iff_products {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C)) ↔ ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.Products.eval C))

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

• GoodProducts.spanFin : The good products span the locally constant functions on π C (· ∈ s) if s is finite.

• GoodProducts.span : The good products span LocallyConstant C ℤ for every closed subset C.

noncomputable def Profinite.NobelingProof.πJ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s) ℤ →ₗ[ℤ] LocallyConstant ↑C ℤ

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

Equations

• Profinite.NobelingProof.πJ C s = LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.ProjRestrict C fun (x : I) => x ∈ s, continuous_toFun := ⋯ }

theorem Profinite.NobelingProof.eval_eq_πJ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (l : Profinite.NobelingProof.Products I) (hl : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => x ∈ s) l) : Profinite.NobelingProof.Products.eval C l = (Profinite.NobelingProof.πJ C s) (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => x ∈ s) l)

noncomputable instance Profinite.NobelingProof.instFintypeElemForallBoolπMemFinset {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) : Fintype ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)

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

Equations

• Profinite.NobelingProof.instFintypeElemForallBoolπMemFinset C s = Fintype.ofInjective (fun (x : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)) (j : { x : I // x ∈ s }) => ↑x ↑j) ⋯

noncomputable def Profinite.NobelingProof.spanFinBasis {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (x : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)) : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s) ℤ

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

Equations

• Profinite.NobelingProof.spanFinBasis C s x = { toFun := fun (y : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)) => if y = x then 1 else 0, isLocallyConstant := ⋯ }

theorem Profinite.NobelingProof.spanFinBasis.span {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.spanFinBasis C s))

def Profinite.NobelingProof.factors {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (x : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)) : List (LocallyConstant ↑(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.

theorem Profinite.NobelingProof.list_prod_apply {I : Type u_1} (C : Set (I → Bool)) (x : ↑C) (l : List (LocallyConstant ↑C ℤ)) : l.prod x = (List.map (⇑(LocallyConstant.evalMonoidHom x)) l).prod

theorem Profinite.NobelingProof.factors_prod_eq_basis_of_eq {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x y : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)} (h : y = x) : (Profinite.NobelingProof.factors C s x).prod y = 1

theorem Profinite.NobelingProof.e_mem_of_eq_true {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)} {a : I} (hx : ↑x a = true) : Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun (x : I) => x ∈ s) a ∈ Profinite.NobelingProof.factors C s x

theorem Profinite.NobelingProof.one_sub_e_mem_of_false {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x y : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)} {a : I} (ha : ↑y a = true) (hx : ↑x a = false) : 1 - Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun (x : I) => x ∈ s) a ∈ Profinite.NobelingProof.factors C s x

theorem Profinite.NobelingProof.factors_prod_eq_basis_of_ne {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) {x y : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)} (h : y ≠ x) : (Profinite.NobelingProof.factors C s x).prod y = 0

theorem Profinite.NobelingProof.factors_prod_eq_basis {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) (x : ↑(Profinite.NobelingProof.π C fun (x : I) => x ∈ s)) : (Profinite.NobelingProof.factors C s x).prod = Profinite.NobelingProof.spanFinBasis C s x

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 (I → Bool)) [LinearOrder I] (s : Finset I) {a : I} {as : List I} (ha : List.Chain' (fun (x1 x2 : I) => x1 > x2) (a :: as)) {c : Profinite.NobelingProof.Products I →₀ ℤ} (hc : ↑c.support ⊆ {m : Profinite.NobelingProof.Products I | ↑m ≤ as}) : (c.sum fun (a_1 : Profinite.NobelingProof.Products I) (b : ℤ) => Profinite.NobelingProof.e (Profinite.NobelingProof.π C fun (x : I) => x ∈ s) a * b • Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => x ∈ s) a_1) ∈ Submodule.span ℤ (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => x ∈ s) '' {m : Profinite.NobelingProof.Products I | ↑m ≤ a :: as})

theorem Profinite.NobelingProof.GoodProducts.spanFin {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (s : Finset I) [WellFoundedLT I] : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => x ∈ s)))

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

theorem Profinite.NobelingProof.fin_comap_jointlySurjective {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (hC : IsClosed C) (f : LocallyConstant ↑C ℤ) : ∃ (s : Finset I) (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} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (hC : IsClosed C) : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval C))

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) [LinearOrder I] [WellFoundedLT I] (i : I) : Ordinal.{u}

A term of I regarded as an ordinal.

Equations

• Profinite.NobelingProof.ord I i = (Ordinal.typein fun (x1 x2 : I) => x1 < x2).toRelEmbedding i

noncomputable def Profinite.NobelingProof.term (I : Type u) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : I

An ordinal regarded as a term of I.

Equations

• Profinite.NobelingProof.term I ho = (Ordinal.enum fun (x1 x2 : I) => x1 < x2) ⟨o, ho⟩

theorem Profinite.NobelingProof.term_ord_aux {I : Type u} [LinearOrder I] [WellFoundedLT I] {i : I} (ho : Profinite.NobelingProof.ord I i < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.term I ho = i

@[simp]

theorem Profinite.NobelingProof.ord_term_aux {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.ord I (Profinite.NobelingProof.term I ho) = o

theorem Profinite.NobelingProof.ord_term {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (i : I) : Profinite.NobelingProof.ord I i = o ↔ Profinite.NobelingProof.term I ho = i

def Profinite.NobelingProof.contained {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : Prop

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

Equations

• Profinite.NobelingProof.contained C o = ∀ f ∈ C, ∀ (i : I), f i = true → Profinite.NobelingProof.ord I i < o

def Profinite.NobelingProof.P (I : Type u) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : Prop

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.

theorem Profinite.NobelingProof.Products.prop_of_isGood_of_contained {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {l : Profinite.NobelingProof.Products I} (o : Ordinal.{u}) (h : Profinite.NobelingProof.Products.isGood C l) (hsC : Profinite.NobelingProof.contained C o) (i : I) (hi : i ∈ ↑l) : Profinite.NobelingProof.ord I i < o

The zero case of the induction

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

instance Profinite.NobelingProof.instSubsingletonLocallyConstantElemForallBoolEmptyCollectionSetInt {I : Type u} : Subsingleton (LocallyConstant ↑∅ ℤ)

Equations

• ⋯ = ⋯

instance Profinite.NobelingProof.instIsEmptySubtypeProductsIsGoodEmptyCollectionSetForallBool {I : Type u} [LinearOrder I] : IsEmpty { l : Profinite.NobelingProof.Products I // Profinite.NobelingProof.Products.isGood ∅ l }

Equations

• ⋯ = ⋯

theorem Profinite.NobelingProof.GoodProducts.linearIndependentEmpty {I : Type u_1} [LinearOrder I] : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval ∅)

def Profinite.NobelingProof.Products.nil {I : Type u} [LinearOrder I] : Profinite.NobelingProof.Products I

The empty list as a Products

Equations

• Profinite.NobelingProof.Products.nil = ⟨[], ⋯⟩

theorem Profinite.NobelingProof.Products.lt_nil_empty {I : Type u_1} [LinearOrder I] : {m : Profinite.NobelingProof.Products I | m < Profinite.NobelingProof.Products.nil} = ∅

instance Profinite.NobelingProof.instNontrivialLocallyConstantIntOfNonempty {α : Type u_1} [TopologicalSpace α] [Nonempty α] : Nontrivial (LocallyConstant α ℤ)

Equations

• ⋯ = ⋯

theorem Profinite.NobelingProof.Products.isGood_nil {I : Type u_1} [LinearOrder I] : Profinite.NobelingProof.Products.isGood {fun (x : I) => false} Profinite.NobelingProof.Products.nil

theorem Profinite.NobelingProof.Products.span_nil_eq_top {I : Type u_1} [LinearOrder I] : Submodule.span ℤ (Profinite.NobelingProof.Products.eval {fun (x : I) => false} '' {Profinite.NobelingProof.Products.nil}) = ⊤

noncomputable instance Profinite.NobelingProof.instUniqueSubtypeProductsIsGoodSingletonForallBoolSetFalse {I : Type u} [LinearOrder I] : Unique { l : Profinite.NobelingProof.Products I // Profinite.NobelingProof.Products.isGood {fun (x : I) => false} l }

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

Equations

• Profinite.NobelingProof.instUniqueSubtypeProductsIsGoodSingletonForallBoolSetFalse = { default := ⟨Profinite.NobelingProof.Products.nil, ⋯⟩, uniq := ⋯ }

instance Profinite.NobelingProof.instNoZeroSMulDivisorsIntLocallyConstant (α : Type u_1) [TopologicalSpace α] : NoZeroSMulDivisors ℤ (LocallyConstant α ℤ)

Equations

• ⋯ = ⋯

theorem Profinite.NobelingProof.GoodProducts.linearIndependentSingleton {I : Type u_1} [LinearOrder I] : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval {fun (x : I) => false})

ℤ-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 definitions

• πs and πs' are the ℤ-linear maps corresponding to ProjRestrict and ProjRestricts respectively.

Main result

• We prove that πs and πs' interact well with Products.eval and the main application is the theorem isGood_mono which says that the property isGood is "monotone" on ordinals.

theorem Profinite.NobelingProof.contained_eq_proj {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) (h : Profinite.NobelingProof.contained C o) : C = Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o

theorem Profinite.NobelingProof.isClosed_proj {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) (hC : IsClosed C) : IsClosed (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)

theorem Profinite.NobelingProof.contained_proj {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : Profinite.NobelingProof.contained (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) o

noncomputable def Profinite.NobelingProof.πs {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) ℤ →ₗ[ℤ] LocallyConstant ↑C ℤ

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

Equations

• Profinite.NobelingProof.πs C o = LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.ProjRestrict C fun (x : I) => Profinite.NobelingProof.ord I x < o, continuous_toFun := ⋯ }

@[simp]

theorem Profinite.NobelingProof.πs_apply_apply {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) (g : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) ℤ) (a✝ : ↑C) : ((Profinite.NobelingProof.πs C o) g) a✝ = g (Profinite.NobelingProof.ProjRestrict C (fun (x : I) => Profinite.NobelingProof.ord I x < o) a✝)

theorem Profinite.NobelingProof.coe_πs {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) (f : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) ℤ) : ⇑((Profinite.NobelingProof.πs C o) f) = ⇑f ∘ Profinite.NobelingProof.ProjRestrict C fun (x : I) => Profinite.NobelingProof.ord I x < o

theorem Profinite.NobelingProof.injective_πs {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : Function.Injective ⇑(Profinite.NobelingProof.πs C o)

noncomputable def Profinite.NobelingProof.πs' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₁) ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₂) ℤ

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

Equations

• Profinite.NobelingProof.πs' C h = LocallyConstant.comapₗ ℤ { toFun := Profinite.NobelingProof.ProjRestricts C ⋯, continuous_toFun := ⋯ }

@[simp]

theorem Profinite.NobelingProof.πs'_apply_apply {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) (g : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₁) ℤ) (a✝ : ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₂)) : ((Profinite.NobelingProof.πs' C h) g) a✝ = g (Profinite.NobelingProof.ProjRestricts C ⋯ a✝)

theorem Profinite.NobelingProof.coe_πs' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) (f : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₁) ℤ) : ((Profinite.NobelingProof.πs' C h) f).toFun = f.toFun ∘ Profinite.NobelingProof.ProjRestricts C ⋯

theorem Profinite.NobelingProof.injective_πs' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) : Function.Injective ⇑(Profinite.NobelingProof.πs' C h)

theorem Profinite.NobelingProof.Products.lt_ord_of_lt {I : Type u} [LinearOrder I] [WellFoundedLT I] {l m : Profinite.NobelingProof.Products I} {o : Ordinal.{u}} (h₁ : m < l) (h₂ : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o) (i : I) : i ∈ ↑m → Profinite.NobelingProof.ord I i < o

theorem Profinite.NobelingProof.Products.eval_πs {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {l : Profinite.NobelingProof.Products I} {o : Ordinal.{u}} (hlt : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o) : (Profinite.NobelingProof.πs C o) (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) l) = Profinite.NobelingProof.Products.eval C l

theorem Profinite.NobelingProof.Products.eval_πs' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {l : Profinite.NobelingProof.Products I} {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) (hlt : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o₁) : (Profinite.NobelingProof.πs' C h) (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₁) l) = Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₂) l

theorem Profinite.NobelingProof.Products.eval_πs_image {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {l : Profinite.NobelingProof.Products I} {o : Ordinal.{u}} (hl : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o) : Profinite.NobelingProof.Products.eval C '' {m : Profinite.NobelingProof.Products I | m < l} = ⇑(Profinite.NobelingProof.πs C o) '' (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) '' {m : Profinite.NobelingProof.Products I | m < l})

theorem Profinite.NobelingProof.Products.eval_πs_image' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {l : Profinite.NobelingProof.Products I} {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) (hl : ∀ i ∈ ↑l, Profinite.NobelingProof.ord I i < o₁) : Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₂) '' {m : Profinite.NobelingProof.Products I | m < l} = ⇑(Profinite.NobelingProof.πs' C h) '' (Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₁) '' {m : Profinite.NobelingProof.Products I | m < l})

theorem Profinite.NobelingProof.Products.head_lt_ord_of_isGood {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] [Inhabited I] {l : Profinite.NobelingProof.Products I} {o : Ordinal.{u}} (h : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) l) (hn : ↑l ≠ []) : Profinite.NobelingProof.ord I (↑l).head! < o

theorem Profinite.NobelingProof.Products.isGood_mono {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {l : Profinite.NobelingProof.Products I} {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) (hl : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₁) l) : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o₂) 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 definitions

• GoodProducts.smaller is the image of good products coming from a smaller ordinal.

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

Main results

• Products.limitOrdinal: for o a limit ordinal such that contained C o, a product l is good w.r.t. C iff it there exists an ordinal o' < o such that l 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.

def Profinite.NobelingProof.GoodProducts.smaller {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : Set (LocallyConstant ↑C ℤ)

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.

noncomputable def Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) (x : ↑(Profinite.NobelingProof.GoodProducts.range (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o))) : ↑(Profinite.NobelingProof.GoodProducts.smaller C o)

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

Equations

• Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun C o x = ⟨(Profinite.NobelingProof.πs C o) ↑x, ⋯⟩

theorem Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun_bijective {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : Function.Bijective (Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun C o)

noncomputable def Profinite.NobelingProof.GoodProducts.range_equiv_smaller {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : ↑(Profinite.NobelingProof.GoodProducts.range (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)) ≃ ↑(Profinite.NobelingProof.GoodProducts.smaller C o)

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

Equations

• Profinite.NobelingProof.GoodProducts.range_equiv_smaller C o = Equiv.ofBijective (Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun C o) ⋯

theorem Profinite.NobelingProof.GoodProducts.smaller_factorization {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : (fun (p : ↑(Profinite.NobelingProof.GoodProducts.smaller C o)) => ↑p) ∘ (Profinite.NobelingProof.GoodProducts.range_equiv_smaller C o).toFun = ⇑(Profinite.NobelingProof.πs C o) ∘ fun (p : ↑(Profinite.NobelingProof.GoodProducts.range (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o))) => ↑p

theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(Profinite.NobelingProof.GoodProducts.smaller C o)) => ↑p

theorem Profinite.NobelingProof.GoodProducts.smaller_mono {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o₁ o₂ : Ordinal.{u}} (h : o₁ ≤ o₂) : Profinite.NobelingProof.GoodProducts.smaller C o₁ ⊆ Profinite.NobelingProof.GoodProducts.smaller C o₂

theorem Profinite.NobelingProof.Products.limitOrdinal {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (l : Profinite.NobelingProof.Products I) : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) l ↔ ∃ o' < o, Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o') l

theorem Profinite.NobelingProof.GoodProducts.union {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : Profinite.NobelingProof.contained C o) : Profinite.NobelingProof.GoodProducts.range C = ⋃ (e : { o' : Ordinal.{u} // o' < o }), Profinite.NobelingProof.GoodProducts.smaller C ↑e

def Profinite.NobelingProof.GoodProducts.range_equiv {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : Profinite.NobelingProof.contained C o) : ↑(Profinite.NobelingProof.GoodProducts.range C) ≃ ↑(⋃ (e : { o' : Ordinal.{u} // o' < o }), Profinite.NobelingProof.GoodProducts.smaller C ↑e)

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

Equations

• Profinite.NobelingProof.GoodProducts.range_equiv C ho hsC = Equiv.Set.ofEq ⋯

theorem Profinite.NobelingProof.GoodProducts.range_equiv_factorization {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : Profinite.NobelingProof.contained C o) : (fun (p : ↑(⋃ (e : { o' : Ordinal.{u} // o' < o }), Profinite.NobelingProof.GoodProducts.smaller C ↑e)) => ↑p) ∘ (Profinite.NobelingProof.GoodProducts.range_equiv C ho hsC).toFun = fun (p : ↑(Profinite.NobelingProof.GoodProducts.range C)) => ↑p

theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (hsC : Profinite.NobelingProof.contained C o) : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔ LinearIndependent ℤ fun (p : ↑(⋃ (e : { o' : Ordinal.{u} // o' < o }), Profinite.NobelingProof.GoodProducts.smaller C ↑e)) => ↑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:

• MaxProducts: the set of good products that contain the ordinal o (since we have contained C (o+1), these all start with o).

• GoodProducts.sum_equiv: the equivalence between GoodProducts C and the disjoint union of MaxProducts C and GoodProducts (π C (ord I · < o)).

Main results

• The main results in the section ExactSequence are succ_mono and succ_exact which together say that the sequence given by πs and Linear_CC' is left exact:

                                              f                        g
  0 --→ LocallyConstant (π C (ord I · < o)) ℤ --→ LocallyConstant C ℤ --→ LocallyConstant C' ℤ
  

  where f is πs and g is Linear_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 of MaxProducts to the evaluation of the corresponding list with the leading o removed.

• GoodProducts.maxTail_isGood says that removing the leading o from a term of MaxProducts C yields a list which isGood with respect to C'.

def Profinite.NobelingProof.C0 {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Set (I → Bool)

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

Equations

• Profinite.NobelingProof.C0 C ho = C ∩ {f : I → Bool | f (Profinite.NobelingProof.term I ho) = false}

def Profinite.NobelingProof.C1 {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Set (I → Bool)

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

Equations

• Profinite.NobelingProof.C1 C ho = C ∩ {f : I → Bool | f (Profinite.NobelingProof.term I ho) = true}

theorem Profinite.NobelingProof.isClosed_C0 {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : IsClosed (Profinite.NobelingProof.C0 C ho)

theorem Profinite.NobelingProof.isClosed_C1 {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : IsClosed (Profinite.NobelingProof.C1 C ho)

theorem Profinite.NobelingProof.contained_C1 {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.contained (Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun (x : I) => Profinite.NobelingProof.ord I x < o) o

theorem Profinite.NobelingProof.union_C0C1_eq {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.C0 C ho ∪ Profinite.NobelingProof.C1 C ho = C

def Profinite.NobelingProof.C' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Set (I → Bool)

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

theorem Profinite.NobelingProof.isClosed_C' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : IsClosed (Profinite.NobelingProof.C' C ho)

theorem Profinite.NobelingProof.contained_C' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.contained (Profinite.NobelingProof.C' C ho) o

noncomputable def Profinite.NobelingProof.SwapTrue {I : Type u} [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : (I → Bool) → I → Bool

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

theorem Profinite.NobelingProof.continuous_swapTrue {I : Type u} [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : Continuous (Profinite.NobelingProof.SwapTrue o)

theorem Profinite.NobelingProof.swapTrue_mem_C1 {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (f : ↑(Profinite.NobelingProof.π (Profinite.NobelingProof.C1 C ho) fun (x : I) => Profinite.NobelingProof.ord I x < o)) : Profinite.NobelingProof.SwapTrue o ↑f ∈ Profinite.NobelingProof.C1 C ho

def Profinite.NobelingProof.CC'₀ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : ↑(Profinite.NobelingProof.C' C ho) → ↑C

The first way to map C' into C.

Equations

• Profinite.NobelingProof.CC'₀ C ho g = ⟨↑g, ⋯⟩

noncomputable def Profinite.NobelingProof.CC'₁ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : ↑(Profinite.NobelingProof.C' C ho) → ↑C

The second way to map C' into C.

Equations

• Profinite.NobelingProof.CC'₁ C hsC ho g = ⟨Profinite.NobelingProof.SwapTrue o ↑g, ⋯⟩

theorem Profinite.NobelingProof.continuous_CC'₀ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Continuous (Profinite.NobelingProof.CC'₀ C ho)

theorem Profinite.NobelingProof.continuous_CC'₁ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Continuous (Profinite.NobelingProof.CC'₁ C hsC ho)

noncomputable def Profinite.NobelingProof.Linear_CC'₀ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ

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 := ⋯ }

noncomputable def Profinite.NobelingProof.Linear_CC'₁ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ

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 := ⋯ }

noncomputable def Profinite.NobelingProof.Linear_CC' {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ

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

theorem Profinite.NobelingProof.CC_comp_zero {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (y : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) ℤ) : (Profinite.NobelingProof.Linear_CC' C hsC ho) ((Profinite.NobelingProof.πs C o) y) = 0

theorem Profinite.NobelingProof.C0_projOrd {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {x : I → Bool} (hx : x ∈ Profinite.NobelingProof.C0 C ho) : Profinite.NobelingProof.Proj (fun (x : I) => Profinite.NobelingProof.ord I x < o) x = x

theorem Profinite.NobelingProof.C1_projOrd {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {x : I → Bool} (hx : x ∈ Profinite.NobelingProof.C1 C ho) : Profinite.NobelingProof.SwapTrue o (Profinite.NobelingProof.Proj (fun (x : I) => Profinite.NobelingProof.ord I x < o) x) = x

theorem Profinite.NobelingProof.CC_exact {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {f : LocallyConstant ↑C ℤ} (hf : (Profinite.NobelingProof.Linear_CC' C hsC ho) f = 0) : ∃ (y : LocallyConstant ↑(Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) ℤ), (Profinite.NobelingProof.πs C o) y = f

theorem Profinite.NobelingProof.succ_mono {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : CategoryTheory.Mono (ModuleCat.asHom (Profinite.NobelingProof.πs C o))

theorem Profinite.NobelingProof.succ_exact {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : (CategoryTheory.ShortComplex.mk (ModuleCat.asHom (Profinite.NobelingProof.πs C o)) (ModuleCat.asHom (Profinite.NobelingProof.Linear_CC' C hsC ho)) ⋯).Exact

def Profinite.NobelingProof.GoodProducts.MaxProducts {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Set (Profinite.NobelingProof.Products I)

The GoodProducts in C that contain o (they necessarily start with o, see GoodProducts.head!_eq_o_of_maxProducts)

Equations

• Profinite.NobelingProof.GoodProducts.MaxProducts C ho = {l : Profinite.NobelingProof.Products I | Profinite.NobelingProof.Products.isGood C l ∧ Profinite.NobelingProof.term I ho ∈ ↑l}

theorem Profinite.NobelingProof.GoodProducts.union_succ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.GoodProducts C = Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) ∪ Profinite.NobelingProof.GoodProducts.MaxProducts C ho

def Profinite.NobelingProof.GoodProducts.sum_to {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)) ⊕ ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) → Profinite.NobelingProof.Products I

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

Equations

• Profinite.NobelingProof.GoodProducts.sum_to C ho = Sum.elim Subtype.val Subtype.val

theorem Profinite.NobelingProof.GoodProducts.injective_sum_to {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Function.Injective (Profinite.NobelingProof.GoodProducts.sum_to C ho)

theorem Profinite.NobelingProof.GoodProducts.sum_to_range {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Set.range (Profinite.NobelingProof.GoodProducts.sum_to C ho) = Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o) ∪ Profinite.NobelingProof.GoodProducts.MaxProducts C ho

noncomputable def Profinite.NobelingProof.GoodProducts.sum_equiv {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)) ⊕ ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) ≃ ↑(Profinite.NobelingProof.GoodProducts C)

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

Equations

• Profinite.NobelingProof.GoodProducts.sum_equiv C hsC ho = Trans.trans (Equiv.ofInjective (Profinite.NobelingProof.GoodProducts.sum_to C ho) ⋯) (Equiv.Set.ofEq ⋯)

theorem Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.GoodProducts.eval C ∘ (Profinite.NobelingProof.GoodProducts.sum_equiv C hsC ho).toFun = Sum.elim (fun (l : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o))) => Profinite.NobelingProof.Products.eval C ↑l) fun (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) => Profinite.NobelingProof.Products.eval C ↑l

def Profinite.NobelingProof.GoodProducts.SumEval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)) ⊕ ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) → LocallyConstant ↑C ℤ

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.

theorem Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔ LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.SumEval C ho)

theorem Profinite.NobelingProof.GoodProducts.span_sum {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Set.range (Profinite.NobelingProof.GoodProducts.eval C) = Set.range (Sum.elim (fun (l : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o))) => Profinite.NobelingProof.Products.eval C ↑l) fun (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) => Profinite.NobelingProof.Products.eval C ↑l)

theorem Profinite.NobelingProof.GoodProducts.square_commutes {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ Sum.inl = ⇑(ModuleCat.asHom (Profinite.NobelingProof.πs C o)) ∘ Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)

theorem Profinite.NobelingProof.swapTrue_eq_true {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (x : I → Bool) : Profinite.NobelingProof.SwapTrue o x (Profinite.NobelingProof.term I ho) = true

theorem Profinite.NobelingProof.mem_C'_eq_false {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (x : I → Bool) : x ∈ Profinite.NobelingProof.C' C ho → x (Profinite.NobelingProof.term I ho) = false

def Profinite.NobelingProof.Products.Tail {I : Type u} [LinearOrder I] (l : Profinite.NobelingProof.Products I) : Profinite.NobelingProof.Products I

List.tail as a Products.

Equations

• l.Tail = ⟨(↑l).tail, ⋯⟩

theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) [Inhabited I] (l : Profinite.NobelingProof.Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = Profinite.NobelingProof.term I ho) : ↑l = Profinite.NobelingProof.term I ho :: ↑l.Tail

theorem Profinite.NobelingProof.Products.max_eq_o_cons_tail' {I : Type u} [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) [Inhabited I] (l : Profinite.NobelingProof.Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = Profinite.NobelingProof.term I ho) (hlc : List.Chain' (fun (x1 x2 : I) => x1 > x2) (Profinite.NobelingProof.term I ho :: ↑l.Tail)) : l = ⟨Profinite.NobelingProof.term I ho :: ↑l.Tail, hlc⟩

theorem Profinite.NobelingProof.GoodProducts.head!_eq_o_of_maxProducts {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) [Inhabited I] (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : (↑↑l).head! = Profinite.NobelingProof.term I ho

theorem Profinite.NobelingProof.GoodProducts.max_eq_o_cons_tail {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : ↑↑l = Profinite.NobelingProof.term I ho :: ↑(↑l).Tail

theorem Profinite.NobelingProof.Products.evalCons {I : Type u_1} [LinearOrder I] {C : Set (I → Bool)} {l : List I} {a : I} (hla : List.Chain' (fun (x1 x2 : I) => x1 > x2) (a :: l)) : Profinite.NobelingProof.Products.eval C ⟨a :: l, hla⟩ = Profinite.NobelingProof.e C a * Profinite.NobelingProof.Products.eval C ⟨l, ⋯⟩

theorem Profinite.NobelingProof.Products.max_eq_eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) [Inhabited I] (l : Profinite.NobelingProof.Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = Profinite.NobelingProof.term I ho) : (Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C l) = Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) l.Tail

theorem Profinite.NobelingProof.GoodProducts.max_eq_eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : (Profinite.NobelingProof.Linear_CC' C hsC ho) (Profinite.NobelingProof.Products.eval C ↑l) = Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail

theorem Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : (⇑(Profinite.NobelingProof.Linear_CC' C hsC ho) ∘ fun (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) => Profinite.NobelingProof.Products.eval C ↑l) = fun (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) => Profinite.NobelingProof.Products.eval (Profinite.NobelingProof.C' C ho) (↑l).Tail

theorem Profinite.NobelingProof.GoodProducts.chain'_cons_of_lt {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) (q : Profinite.NobelingProof.Products I) (hq : q < (↑l).Tail) : List.Chain' (fun (x x_1 : I) => x > x_1) (Profinite.NobelingProof.term I ho :: ↑q)

theorem Profinite.NobelingProof.GoodProducts.good_lt_maxProducts {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (q : ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o))) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) : List.Lex (fun (x1 x2 : I) => x1 < x2) ↑↑q ↑↑l

theorem Profinite.NobelingProof.GoodProducts.maxTail_isGood {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)))) : Profinite.NobelingProof.Products.isGood (Profinite.NobelingProof.C' C ho) (↑l).Tail

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} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)))) : ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho) → ↑(Profinite.NobelingProof.GoodProducts (Profinite.NobelingProof.C' C ho))

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, ⋯⟩

theorem Profinite.NobelingProof.GoodProducts.maxToGood_injective {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)))) : Function.Injective (Profinite.NobelingProof.GoodProducts.MaxToGood C hC hsC ho h₁)

theorem Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hC : IsClosed C) (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.π C fun (x : I) => Profinite.NobelingProof.ord I x < o)))) : LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval (Profinite.NobelingProof.C' C ho)) → LinearIndependent (ι := ↑(Profinite.NobelingProof.GoodProducts.MaxProducts C ho)) ℤ (⇑(ModuleCat.asHom (Profinite.NobelingProof.Linear_CC' C hsC ho)) ∘ Profinite.NobelingProof.GoodProducts.SumEval C ho ∘ 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:

• 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] : Profinite.NobelingProof.P I 0

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

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

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

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

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

Equations

• Profinite.NobelingProof.GoodProducts.Basis C hC = 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 (Profinite.Nobeling.ι S)

The map Nobeling.ι is a closed embedding.

@[deprecated Profinite.Nobeling.isClosedEmbedding]

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

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

Equations

• ⋯ = ⋯