The successor case in the induction for Nöbeling's theorem

Here we assume that o is an ordinal such that contained C (o+1) and o < I. The element in I corresponding to o is called term I ho, but in this informal docstring we refer to it simply as o.

This section follows the proof in [scholze2019condensed] 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 [scholze2019condensed] with this proof, one should read the phrase "is a basis" as "is linearly independent". Also, the short exact sequence in [scholze2019condensed] 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 [scholze2019condensed]. The second one, GoodProducts corresponds to the last paragraph in the proof in [scholze2019condensed].

For the overall proof outline see Mathlib/Topology/Category/Profinite/Nobeling/Basic.lean.

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

References

• [scholze2019condensed], Theorem 5.4.

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 (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 (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) : contained (π (C1 C ho) fun (x : I) => 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) : C0 C ho ∪ 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 (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) : contained (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 (SwapTrue o)

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

theorem Profinite.NobelingProof.continuous_CC'₁ {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Continuous (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 ↑(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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : LocallyConstant ↑C ℤ →ₗ[ℤ] LocallyConstant ↑(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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (y : LocallyConstant ↑(π C fun (x : I) => ord I x < o) ℤ) : (Linear_CC' C hsC ho) ((π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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {x : I → Bool} (hx : x ∈ C0 C ho) : Proj (fun (x : I) => 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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {x : I → Bool} (hx : x ∈ C1 C ho) : SwapTrue o (Proj (fun (x : I) => 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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {f : LocallyConstant ↑C ℤ} (hf : (Linear_CC' C hsC ho) f = 0) : ∃ (y : LocallyConstant ↑(π C fun (x : I) => ord I x < o) ℤ), (π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.ofHom (π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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : { X₁ := ModuleCat.of ℤ (LocallyConstant ↑(π C fun (x : I) => ord I x < o) ℤ), X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ), X₃ := ModuleCat.of ℤ (LocallyConstant ↑(C' C ho) ℤ), f := ModuleCat.ofHom (πs C o), g := ModuleCat.ofHom (Linear_CC' C hsC ho), zero := ⋯ }.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 (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : GoodProducts C = GoodProducts (π C fun (x : I) => ord I x < o) ∪ 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) : ↑(GoodProducts (π C fun (x : I) => ord I x < o)) ⊕ ↑(MaxProducts C ho) → 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 (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 (sum_to C ho) = GoodProducts (π C fun (x : I) => ord I x < o) ∪ 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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : ↑(GoodProducts (π C fun (x : I) => ord I x < o)) ⊕ ↑(MaxProducts C ho) ≃ ↑(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.setCongr ⋯)

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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : eval C ∘ (sum_equiv C hsC ho).toFun = Sum.elim (fun (l : ↑(GoodProducts (π C fun (x : I) => ord I x < o))) => Products.eval C ↑l) fun (l : ↑(MaxProducts C ho)) => 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) : ↑(GoodProducts (π C fun (x : I) => ord I x < o)) ⊕ ↑(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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : LinearIndependent ℤ (eval C) ↔ LinearIndependent ℤ (SumEval C ho)

theorem Profinite.NobelingProof.GoodProducts.span_sum {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : Set.range (eval C) = Set.range (Sum.elim (fun (l : ↑(GoodProducts (π C fun (x : I) => ord I x < o))) => Products.eval C ↑l) fun (l : ↑(MaxProducts C ho)) => 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) : SumEval C ho ∘ Sum.inl = ⇑(CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom (πs C o))) ∘ eval (π C fun (x : I) => 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) : SwapTrue o x (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 ∈ C' C ho → x (term I ho) = false

def Profinite.NobelingProof.Products.Tail {I : Type u} [LinearOrder I] (l : Products I) : 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 : Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = term I ho) : ↑l = 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 : Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = term I ho) (hlc : List.Chain' (fun (x1 x2 : I) => x1 > x2) (term I ho :: ↑l.Tail)) : l = ⟨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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) [Inhabited I] (l : ↑(MaxProducts C ho)) : (↑↑l).head! = 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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(MaxProducts C ho)) : ↑↑l = 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)) : eval C ⟨a :: l, hla⟩ = e C a * 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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) [Inhabited I] (l : Products I) (hl : ↑l ≠ []) (hlh : (↑l).head! = term I ho) : (Linear_CC' C hsC ho) (eval C l) = eval (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(MaxProducts C ho)) : (Linear_CC' C hsC ho) (Products.eval C ↑l) = Products.eval (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) : (⇑(Linear_CC' C hsC ho) ∘ fun (l : ↑(MaxProducts C ho)) => Products.eval C ↑l) = fun (l : ↑(MaxProducts C ho)) => Products.eval (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(MaxProducts C ho)) (q : Products I) (hq : q < (↑l).Tail) : List.Chain' (fun (x x_1 : I) => x > x_1) (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (q : ↑(GoodProducts (π C fun (x : I) => ord I x < o))) (l : ↑(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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (l : ↑(MaxProducts C ho)) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun (x : I) => ord I x < o)))) : Products.isGood (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun (x : I) => ord I x < o)))) : ↑(MaxProducts C ho) → ↑(GoodProducts (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun (x : I) => ord I x < o)))) : Function.Injective (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 : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (h₁ : ⊤ ≤ Submodule.span ℤ (Set.range (eval (π C fun (x : I) => ord I x < o)))) : LinearIndependent ℤ (eval (C' C ho)) → LinearIndependent (ι := ↑(MaxProducts C ho)) ℤ (⇑(CategoryTheory.ConcreteCategory.hom (ModuleCat.ofHom (Linear_CC' C hsC ho))) ∘ SumEval C ho ∘ Sum.inr)