The zero and limit cases in the induction for Nöbeling's theorem

This file proves the zero and limit cases of the ordinal induction used in the proof of Nöbeling's theorem. See the section docstrings for more information.

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

References

• [scholze2019condensed], Theorem 5.4.

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 ↑∅ ℤ)

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

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

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

The empty list as a Products

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

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

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

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

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

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

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

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

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.

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

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

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 (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}) : ↑(range (π C fun (x : I) => ord I x < o)) ≃ ↑(smaller C o)

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

theorem Profinite.NobelingProof.GoodProducts.smaller_factorization {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] (o : Ordinal.{u}) : (fun (p : ↑(smaller C o)) => ↑p) ∘ (range_equiv_smaller C o).toFun = ⇑(πs C o) ∘ fun (p : ↑(range (π C fun (x : I) => 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 ℤ (eval (π C fun (x : I) => ord I x < o)) ↔ LinearIndependent ℤ fun (p : ↑(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₂) : smaller C o₁ ⊆ smaller C o₂

theorem Profinite.NobelingProof.Products.limitOrdinal {I : Type u} (C : Set (I → Bool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : Order.IsSuccLimit o) (l : Products I) : isGood (π C fun (x : I) => ord I x < o) l ↔ ∃ o' < o, isGood (π C fun (x : I) => 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 : Order.IsSuccLimit o) (hsC : contained C o) : range C = ⋃ (e : { o' : Ordinal.{u} // o' < o }), smaller C ↑e

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

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

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