Preliminaries for Nöbeling's theorem

This file constructs basic objects and results concerning them that are needed in the proof of Nöbeling's theorem, which is in Mathlib/Topology/Category/Profinite/Nobeling/Induction.lean. See the section docstrings for more information.

Proof idea

We follow the proof of theorem 5.4 in [scholze2019condensed], 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 (in Mathlib/Topology/Category/Profinite/Nobeling/ZeroLimit.lean and Mathlib/Topology/Category/Profinite/Nobeling/Successor.lean) is that this set is linearly independent. The fact that it spans is proved directly in Mathlib/Topology/Category/Profinite/Nobeling/Span.lean.

References

• [scholze2019condensed], 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

@[simp]

theorem Profinite.NobelingProof.continuous_proj {I : Type u} (J : I → Prop) [(i : I) → Decidable (J i)] : Continuous (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

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

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

@[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) : ↑(ProjRestrict C J a✝) a✝¹ = 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 (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) : 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) : π 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) : Proj J ∘ Proj K = 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) : π (π C K) J = π 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) : ↑(π C K) → ↑(π C J)

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

@[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✝ : ↑(π C K)) (a✝¹ : I) : ↑(ProjRestricts C h a✝) a✝¹ = 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 (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 (ProjRestricts C h)

theorem Profinite.NobelingProof.projRestricts_eq_id {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : 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) : ProjRestricts C hJK ∘ ProjRestricts C hKL = 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) : ProjRestricts C h ∘ ProjRestrict C K = ProjRestrict C J

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

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

theorem Profinite.NobelingProof.iso_map_bijective {I : Type u} (C : Set (I → Bool)) (J : I → Prop) [(i : I) → Decidable (J i)] : Function.Bijective ⇑(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.

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 (spanFunctor hC)

The limit cone on spanFunctor with point C.

noncomputable def Profinite.NobelingProof.spanFunctorIsoIndexFunctor {I : Type u} {C : Set (I → Bool)} [(s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C) : spanFunctor hC ≅ indexFunctor hC

The isomorphism spanFunctor hC ≅ indexFunctor hC when hC : IsCompact C.

@[simp]

theorem Profinite.NobelingProof.spanFunctorIsoIndexFunctor_hom_app_hom_hom_apply_coe {I : Type u} {C : Set (I → Bool)} [(s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C) (X : (Finset I)ᵒᵖ) (x : ↑(π C fun (x : I) => x ∈ Opposite.unop X)) (i : { i : I // (fun (x : I) => x ∈ Opposite.unop X) i }) : ↑((TopCat.Hom.hom ((spanFunctorIsoIndexFunctor hC).hom.app X).hom) x) i = ↑x ↑i

@[simp]

theorem Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app {I : Type u} {C : Set (I → Bool)} [(s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C) (X : (Finset I)ᵒᵖ) : (spanFunctorIsoIndexFunctor hC).inv.app X = (CompHausLike.isoOfBijective (CategoryTheory.ConcreteCategory.ofHom (iso_map C fun (x : I) => x ∈ Opposite.unop X)) ⋯).inv

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 (spanCone hC)

spanCone is a limit cone.

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.

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.

@[implicit_reducible]

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

@[simp]

theorem Profinite.NobelingProof.Products.lt_iff_lex_lt {I : Type u} [LinearOrder I] (l m : 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 (Products I)

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

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

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

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

theorem Profinite.NobelingProof.Products.rel_head!_of_mem {I : Type u} [LinearOrder I] [Inhabited I] {i : I} {l : 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 : 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 (Products I)

The set of good products.

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

Evaluation of good products.

theorem Profinite.NobelingProof.GoodProducts.injective {I : Type u} (C : Set (I → Bool)) [LinearOrder I] : Function.Injective (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 ℤ.

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

The type of good products is equivalent to its image.

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

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

theorem Profinite.NobelingProof.Products.eval_eq {I : Type u} (C : Set (I → Bool)) [LinearOrder I] (l : Products I) (x : ↑C) : (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 : Products I} (J : I → Prop) (h : ∀ a ∈ ↑l, J a) [(j : I) → Decidable (J j)] : ⇑(eval (π C J) l) ∘ ProjRestrict C J = ⇑(eval C l)

theorem Profinite.NobelingProof.Products.evalFacProps {I : Type u} (C : Set (I → Bool)) [LinearOrder I] {l : 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) : ⇑(eval (π C J) l) ∘ ProjRestricts C hJK = ⇑(eval (π C K) l)

theorem Profinite.NobelingProof.Products.prop_of_isGood {I : Type u} (C : Set (I → Bool)) [LinearOrder I] {l : Products I} (J : I → Prop) [(j : I) → Decidable (J j)] (h : isGood (π 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 (eval C)) ↔ ⊤ ≤ Submodule.span ℤ (Set.range (Products.eval C))

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

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.

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.

theorem Profinite.NobelingProof.term_ord_aux {I : Type u} [LinearOrder I] [WellFoundedLT I] {i : I} (ho : ord I i < Ordinal.type fun (x1 x2 : I) => x1 < x2) : 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) : ord I (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) : ord I i = o ↔ 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.

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

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

ℤ-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 : contained C o) : C = π C fun (x : I) => 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 (π C fun (x : I) => ord I x < o)

theorem Profinite.NobelingProof.contained_proj {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : contained (π C fun (x : I) => 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 ↑(π C fun (x : I) => ord I x < o) ℤ →ₗ[ℤ] LocallyConstant ↑C ℤ

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

@[simp]

theorem Profinite.NobelingProof.πs_apply_apply {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) (g : LocallyConstant ↑(π C fun (x : I) => ord I x < o) ℤ) (a✝ : ↑C) : ((πs C o) g) a✝ = g (ProjRestrict C (fun (x : I) => 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 ↑(π C fun (x : I) => ord I x < o) ℤ) : ⇑((πs C o) f) = ⇑f ∘ ProjRestrict C fun (x : I) => 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 ⇑(π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 ↑(π C fun (x : I) => ord I x < o₁) ℤ →ₗ[ℤ] LocallyConstant ↑(π C fun (x : I) => ord I x < o₂) ℤ

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

@[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 ↑(π C fun (x : I) => ord I x < o₁) ℤ) (a✝ : ↑(π C fun (x : I) => ord I x < o₂)) : ((πs' C h) g) a✝ = g (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 ↑(π C fun (x : I) => ord I x < o₁) ℤ) : ((πs' C h) f).toFun = f.toFun ∘ 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 ⇑(πs' C h)

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

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

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

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

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

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