Documentation

Mathlib.Topology.Category.Profinite.Nobeling.Successor

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 [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].

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

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:

Main results #

The main results in the section GoodProducts are as follows:

References #

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

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

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

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

    Equations
    Instances For
      theorem Profinite.NobelingProof.isClosed_C0 {I : Type u} (C : Set (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :
      Set (IBool)

      The intersection of C0 and the projection of C1. We will apply the inductive hypothesis to this set.

      Equations
      Instances For
        theorem Profinite.NobelingProof.isClosed_C' {I : Type u} (C : Set (IBool)) [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 (IBool)) [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}) :
        (IBool)IBool

        Swapping the o-th coordinate to true.

        Equations
        Instances For
          theorem Profinite.NobelingProof.swapTrue_mem_C1 {I : Type u} (C : Set (IBool)) [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 (IBool)) [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
          Instances For
            noncomputable def Profinite.NobelingProof.CC'₁ {I : Type u} (C : Set (IBool)) [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
            Instances For
              theorem Profinite.NobelingProof.continuous_CC'₀ {I : Type u} (C : Set (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :
              theorem Profinite.NobelingProof.continuous_CC'₁ {I : Type u} (C : Set (IBool)) [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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :

              The -linear map induced by precomposing with CC'₀

              Equations
              Instances For
                noncomputable def Profinite.NobelingProof.Linear_CC'₁ {I : Type u} (C : Set (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :

                The -linear map induced by precomposing with CC'₁

                Equations
                Instances For
                  noncomputable def Profinite.NobelingProof.Linear_CC' {I : Type u} (C : Set (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :

                  The difference between Linear_CC'₁ and Linear_CC'₀.

                  Equations
                  Instances For
                    theorem Profinite.NobelingProof.CC_comp_zero {I : Type u} (C : Set (IBool)) [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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {x : IBool} (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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (hsC : contained C (Order.succ o)) (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) {x : IBool} (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 (IBool)) [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_exact {I : Type u} (C : Set (IBool)) [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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :

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

                    Equations
                    Instances For
                      theorem Profinite.NobelingProof.GoodProducts.union_succ {I : Type u} (C : Set (IBool)) [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 (IBool)) [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
                      Instances For
                        theorem Profinite.NobelingProof.GoodProducts.injective_sum_to {I : Type u} (C : Set (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :
                        theorem Profinite.NobelingProof.GoodProducts.sum_to_range {I : Type u} (C : Set (IBool)) [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 (IBool)) [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
                        Instances For
                          theorem Profinite.NobelingProof.GoodProducts.sum_equiv_comp_eval_eq_elim {I : Type u} (C : Set (IBool)) [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 (IBool)) [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.
                          Instances For
                            theorem Profinite.NobelingProof.GoodProducts.span_sum {I : Type u} (C : Set (IBool)) [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 (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) :
                            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 : IBool) :
                            SwapTrue o x (term I ho) = true
                            theorem Profinite.NobelingProof.mem_C'_eq_false {I : Type u} (C : Set (IBool)) [LinearOrder I] [WellFoundedLT I] {o : Ordinal.{u}} (ho : o < Ordinal.type fun (x1 x2 : I) => x1 < x2) (x : IBool) :
                            x C' C hox (term I ho) = false

                            List.tail as a Products.

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