Documentation

Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

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.

References #

The zero case of the induction #

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

The empty list as a Products

Equations
Instances For

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

    Equations

    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 #

    Main results #

    The image of the GoodProducts for π C (ord I · < o) in LocallyConstant C ℤ. The name smaller refers to the setting in which we will use this, when we are mapping in GoodProducts from a smaller set, i.e. when o is a smaller ordinal than the one C is "contained" in.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      noncomputable def Profinite.NobelingProof.GoodProducts.range_equiv_smaller_toFun {I : Type u} (C : Set (IBool)) [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

      Equations
      Instances For
        noncomputable def Profinite.NobelingProof.GoodProducts.range_equiv_smaller {I : Type u} (C : Set (IBool)) [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

        Equations
        Instances For
          theorem Profinite.NobelingProof.GoodProducts.smaller_factorization {I : Type u} (C : Set (IBool)) [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.smaller_mono {I : Type u} (C : Set (IBool)) [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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (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.

          Equations
          Instances For
            theorem Profinite.NobelingProof.GoodProducts.range_equiv_factorization {I : Type u} (C : Set (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o.IsLimit) (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