Documentation

Mathlib.Order.DirectedInverseSystem

Definition of direct systems, inverse systems, and cardinalities in specific inverse systems #

In this file we compute the cardinality of each node in an inverse system F i indexed by a well-order in which every map between successive nodes has constant fiber X i, and every limit node is the limit of the inverse subsystem formed by all previous nodes. (To avoid importing Cardinal, we in fact construct a bijection rather than stating the result in terms of Cardinal.mk.)

The most tricky part of the whole argument happens at limit nodes: if i : ι is a limit, what we have in hand is a family of bijections F j ≃ ∀ l : Iio j, X l for every j < i, which we would like to "glue" up to a bijection F i ≃ ∀ l : Iio i, X l. We denote ∀ l : Iio i, X l by PiLT X i, and they form an inverse system just like the F i. Observe that at a limit node i, PiLT X i is actually the inverse limit of PiLT X j over all j < i (piLTLim). If the family of bijections F j ≃ PiLT X j is natural (IsNatEquiv), we immediately obtain a bijection between the limits limit F i ≃ PiLT X i (invLimEquiv), and we just need an additional bijection F i ≃ limit F i to obtain the desired extension F i ≃ PiLT X i to the limit node i. (We do have such a bijection, for example, when we consider a directed system of algebraic structures (say fields) K i, and F is the inverse system of homomorphisms K i ⟶ K into a specific field K.)

Now our task reduces to the recursive construction of a natural family of bijections for each i. We can prove that a natural family over all l ≤ i (Iic i) extends to a natural family over Iic i⁺ (where i⁺ = succ i), but at a limit node, recursion stops working: we have natural families over all Iic j for each j < i, but we need to know that they glue together to form a natural family over all l < i (Iio i). This intricacy did not occur to the author when he thought he had a proof and set out to formalize it. Fortunately he was able to figure out an additional compat condition (compatibility with the bijections F i⁺ ≃ F i × X i in the X component) that guarantees uniqueness (unique_pEquivOn) and hence gluability (well-definedness): see pEquivOnGlue. Instead of just a family of natural families, we actually construct a family of the stronger PEquivOns that bundles the compat condition, in order for the inductive argument to work.

It is possible to circumvent the introduction of the compat condition using Zorn's lemma; if there is a chain of natural families (i.e. for any two families in the chain, one is an extension of the other) over lowersets (which are all of the form Iic, Iio, or univ), we can clearly take the union to get a natural family that extends them all. If a maximal natural family has domain Iic i or Iio i (i a limit), we already know how to extend it one step further to Iic i⁺ or Iic i respectively, so it must be the case that the domain is everything. However, the author chose the compat approach in the end because it constructs the distinguished bijection that is compatible with the projections to all X i.

class DirectedSystem {ι : Type u_1} [Preorder ι] (F : ιType u_2) (f : i j : ι⦄ → i jF iF j) :

A directed system is a functor from a category (directed poset) to another category.

  • map_self : ∀ ⦃i : ι⦄ (x : F i), f x = x
  • map_map : ∀ ⦃k j i : ι⦄ (hij : i j) (hjk : j k) (x : F i), f hjk (f hij x) = f x
Instances
    theorem DirectedSystem.map_self {ι : Type u_1} :
    ∀ {inst : Preorder ι} {F : ιType u_2} {f : i j : ι⦄ → i jF iF j} [self : DirectedSystem F f] ⦃i : ι⦄ (x : F i), f x = x
    theorem DirectedSystem.map_map {ι : Type u_1} :
    ∀ {inst : Preorder ι} {F : ιType u_2} {f : i j : ι⦄ → i jF iF j} [self : DirectedSystem F f] ⦃k j i : ι⦄ (hij : i j) (hjk : j k) (x : F i), f hjk (f hij x) = f x
    class InverseSystem {ι : Type u_1} [Preorder ι] {F : ιType u_2} (f : i j : ι⦄ → i jF jF i) :

    A inverse system indexed by a preorder is a contravariant functor from the preorder to another category. It is dual to DirectedSystem.

    • map_self : ∀ ⦃i : ι⦄ (x : F i), f x = x
    • map_map : ∀ ⦃k j i : ι⦄ (hkj : k j) (hji : j i) (x : F i), f hkj (f hji x) = f x
    Instances
      theorem InverseSystem.map_self {ι : Type u_1} :
      ∀ {inst : Preorder ι} {F : ιType u_2} {f : i j : ι⦄ → i jF jF i} [self : InverseSystem f] ⦃i : ι⦄ (x : F i), f x = x
      theorem InverseSystem.map_map {ι : Type u_1} :
      ∀ {inst : Preorder ι} {F : ιType u_2} {f : i j : ι⦄ → i jF jF i} [self : InverseSystem f] ⦃k j i : ι⦄ (hkj : k j) (hji : j i) (x : F i), f hkj (f hji x) = f x
      def InverseSystem.limit {ι : Type u_1} [Preorder ι] {F : ιType u_2} (f : i j : ι⦄ → i jF jF i) (i : ι) :
      Set ((l : (Set.Iio i)) → F l)

      The inverse limit of an inverse system of types.

      Equations
      Instances For
        @[reducible, inline]
        abbrev InverseSystem.piLT {ι : Type u_1} [Preorder ι] (X : ιType u_4) (i : ι) :
        Type (max u_1 u_4)

        For a family of types X indexed by an preorder ι and an element i : ι, piLT X i is the product of all the types indexed by elements below i.

        Equations
        Instances For
          @[reducible, inline]
          abbrev InverseSystem.piLTProj {ι : Type u_1} [Preorder ι] {X : ιType u_3} ⦃i : ι ⦃j : ι (h : i j) (f : InverseSystem.piLT X j) :

          The projection from a Pi type to the Pi type over an initial segment of its indexing type.

          Equations
          Instances For
            theorem InverseSystem.piLTProj_intro {ι : Type u_1} [Preorder ι] {X : ιType u_3} ⦃i : ι ⦃j : ι (h : i j) {l : (Set.Iio j)} {f : InverseSystem.piLT X j} (hl : l < i) :
            f l = InverseSystem.piLTProj h f l, hl
            def InverseSystem.IsNatEquiv {ι : Type u_1} [Preorder ι] {F : ιType u_2} {X : ιType u_3} (f : i j : ι⦄ → i jF jF i) {s : Set ι} (equiv : (j : s) → F j InverseSystem.piLT X j) :

            The predicate that says a family of equivalences between F j and piLT X j is a natural transformation.

            Equations
            Instances For
              noncomputable def InverseSystem.piLTLim {ι : Type u_4} [LinearOrder ι] {X : ιType u_5} {i : ι} (hi : Order.IsSuccPrelimit i) :
              InverseSystem.piLT X i (InverseSystem.limit InverseSystem.piLTProj i)

              If i is a limit in a well-ordered type indexing a family of types, then piLT X i is the limit of all piLT X j for j < i.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem InverseSystem.piLTLim_apply {ι : Type u_4} [LinearOrder ι] {X : ιType u_5} {i : ι} (hi : Order.IsSuccPrelimit i) (f : InverseSystem.piLT X i) :
                (InverseSystem.piLTLim hi) f = fun (j : (Set.Iio i)) => InverseSystem.piLTProj f,
                theorem InverseSystem.piLTLim_symm_apply {ι : Type u_4} [LinearOrder ι] {X : ιType u_5} {i : ι} (hi : Order.IsSuccPrelimit i) {f : (InverseSystem.limit InverseSystem.piLTProj i)} (k : (Set.Iio i)) {l : (Set.Iio i)} (hl : l < k) :
                (InverseSystem.piLTLim hi).symm f l = f k l, hl
                def InverseSystem.piSplitLE {ι : Type u_4} {X : ιType u_6} {i : ι} [PartialOrder ι] [DecidableEq ι] :
                InverseSystem.piLT X i × X i ((j : (Set.Iic i)) → X j)

                Splitting off the X i factor from the Pi type over {j | j ≤ i}.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem InverseSystem.piSplitLE_eq {ι : Type u_4} {X : ιType u_6} {i : ι} [PartialOrder ι] [DecidableEq ι] {f : InverseSystem.piLT X i × X i} :
                  InverseSystem.piSplitLE f i, = f.2
                  theorem InverseSystem.piSplitLE_lt {ι : Type u_4} {X : ιType u_6} {i : ι} [PartialOrder ι] [DecidableEq ι] {f : InverseSystem.piLT X i × X i} {j : ι} (hj : j < i) :
                  InverseSystem.piSplitLE f j, = f.1 j, hj
                  def InverseSystem.piEquivSucc {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] [SuccOrder ι] (equiv : (j : (Set.Iic i)) → F j InverseSystem.piLT X j) (e : F (Order.succ i) F i × X i) (hi : ¬IsMax i) (j : (Set.Iic (Order.succ i))) :
                  F j InverseSystem.piLT X j

                  Extend a family of bijections to piLT by one step.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    theorem InverseSystem.piEquivSucc_self {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] [SuccOrder ι] (equiv : (j : (Set.Iic i)) → F j InverseSystem.piLT X j) (e : F (Order.succ i) F i × X i) (hi : ¬IsMax i) {x : F Order.succ i, } :
                    (InverseSystem.piEquivSucc equiv e hi Order.succ i, ) x i, = (e x).2
                    theorem InverseSystem.isNatEquiv_piEquivSucc {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equiv : (j : (Set.Iic i)) → F j InverseSystem.piLT X j} {e : F (Order.succ i) F i × X i} (hi : ¬IsMax i) [InverseSystem f] (H : ∀ (x : F (Order.succ i)), (e x).1 = f x) (nat : InverseSystem.IsNatEquiv f equiv) :
                    def InverseSystem.invLimEquiv {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} {equiv : (j : (Set.Iio i)) → F j InverseSystem.piLT X j} (nat : InverseSystem.IsNatEquiv f equiv) :
                    (InverseSystem.limit f i) (InverseSystem.limit InverseSystem.piLTProj i)

                    A natural family of bijections below a limit ordinal induces a bijection at the limit ordinal.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[simp]
                      theorem InverseSystem.invLimEquiv_apply_coe {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} {equiv : (j : (Set.Iio i)) → F j InverseSystem.piLT X j} (nat : InverseSystem.IsNatEquiv f equiv) (t : (InverseSystem.limit f i)) (l : (Set.Iio i)) (l : (Set.Iio l✝)) :
                      ((InverseSystem.invLimEquiv nat) t) l✝ l = (equiv l✝) (t l✝) l
                      @[simp]
                      theorem InverseSystem.invLimEquiv_symm_apply_coe {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} {equiv : (j : (Set.Iio i)) → F j InverseSystem.piLT X j} (nat : InverseSystem.IsNatEquiv f equiv) (t : (InverseSystem.limit InverseSystem.piLTProj i)) (l : (Set.Iio i)) :
                      ((InverseSystem.invLimEquiv nat).symm t) l = (equiv l).symm (t l)
                      noncomputable def InverseSystem.piEquivLim {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} {equiv : (j : (Set.Iio i)) → F j InverseSystem.piLT X j} (nat : InverseSystem.IsNatEquiv f equiv) (equivLim : F i (InverseSystem.limit f i)) (hi : Order.IsSuccPrelimit i) (j : (Set.Iic i)) :
                      F j InverseSystem.piLT X j

                      Extend a natural family of bijections to a limit ordinal.

                      Equations
                      Instances For
                        theorem InverseSystem.isNatEquiv_piEquivLim {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} {equiv : (j : (Set.Iio i)) → F j InverseSystem.piLT X j} (nat : InverseSystem.IsNatEquiv f equiv) {equivLim : F i (InverseSystem.limit f i)} (hi : Order.IsSuccPrelimit i) [InverseSystem f] (H : ∀ (x : F i) (l : (Set.Iio i)), (equivLim x) l = f x) :
                        structure InverseSystem.PEquivOn {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] (f : i j : ι⦄ → i jF jF i) [SuccOrder ι] (equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i) (s : Set ι) :
                        Type (max (max u_4 u_5) u_6)

                        A natural partial family of bijections to piLT satisfying a compatibility condition.

                        • equiv : (i : s) → F i InverseSystem.piLT X i

                          A partial family of bijections between F and piLT X defined on some set in ι.

                        • nat : InverseSystem.IsNatEquiv f self.equiv

                          It is a natural family of bijections.

                        • compat : ∀ {i : ι} (hsi : Order.succ i s) (hi : ¬IsMax i) (x : F Order.succ i, hsi), (self.equiv Order.succ i, hsi) x i, = ((equivSucc hi) x).2

                          It is compatible with a family of bijections relating F i⁺ to F i.

                        Instances For
                          theorem InverseSystem.PEquivOn.ext {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} :
                          ∀ {inst : LinearOrder ι} {f : i j : ι⦄ → i jF jF i} {inst_1 : SuccOrder ι} {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} {s : Set ι} {x y : InverseSystem.PEquivOn f equivSucc s}, x.equiv = y.equivx = y
                          theorem InverseSystem.PEquivOn.nat {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} {s : Set ι} (self : InverseSystem.PEquivOn f equivSucc s) :

                          It is a natural family of bijections.

                          theorem InverseSystem.PEquivOn.compat {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} {s : Set ι} (self : InverseSystem.PEquivOn f equivSucc s) {i : ι} (hsi : Order.succ i s) (hi : ¬IsMax i) (x : F Order.succ i, hsi) :
                          (self.equiv Order.succ i, hsi) x i, = ((equivSucc hi) x).2

                          It is compatible with a family of bijections relating F i⁺ to F i.

                          def InverseSystem.PEquivOn.restrict {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} {s : Set ι} {t : Set ι} (e : InverseSystem.PEquivOn f equivSucc t) (h : s t) :

                          Restrict a partial family of bijections to a smaller set.

                          Equations
                          • e.restrict h = { equiv := fun (i : s) => e.equiv i, , nat := , compat := }
                          Instances For
                            @[simp]
                            theorem InverseSystem.PEquivOn.restrict_equiv {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} {s : Set ι} {t : Set ι} (e : InverseSystem.PEquivOn f equivSucc t) (h : s t) (i : s) :
                            (e.restrict h).equiv i = e.equiv i,
                            theorem InverseSystem.unique_pEquivOn {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} {s : Set ι} [WellFoundedLT ι] (hs : IsLowerSet s) {e₁ : InverseSystem.PEquivOn f equivSucc s} {e₂ : InverseSystem.PEquivOn f equivSucc s} :
                            e₁ = e₂
                            theorem InverseSystem.pEquivOn_apply_eq {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} {s : Set ι} {t : Set ι} [WellFoundedLT ι] (h : IsLowerSet (s t)) {e₁ : InverseSystem.PEquivOn f equivSucc s} {e₂ : InverseSystem.PEquivOn f equivSucc t} {i : ι} {his : i s} {hit : i t} :
                            e₁.equiv i, his = e₂.equiv i, hit
                            def InverseSystem.pEquivOnSucc {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} [InverseSystem f] (hi : ¬IsMax i) (e : InverseSystem.PEquivOn f equivSucc (Set.Iic i)) (H : ∀ ⦃i : ι⦄ (hi : ¬IsMax i) (x : F (Order.succ i)), ((equivSucc hi) x).1 = f x) :

                            Extend a partial family of bijections by one step.

                            Equations
                            Instances For
                              noncomputable def InverseSystem.pEquivOnGlue {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} [WellFoundedLT ι] (hi : Order.IsSuccPrelimit i) (e : (j : (Set.Iio i)) → InverseSystem.PEquivOn f equivSucc (Set.Iic j)) :

                              Glue partial families of bijections at a limit ordinal, obtaining a partial family over a right-open interval.

                              Equations
                              Instances For
                                noncomputable def InverseSystem.pEquivOnLim {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} {i : ι} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [SuccOrder ι] {equivSucc : i : ι⦄ → ¬IsMax iF (Order.succ i) F i × X i} [WellFoundedLT ι] (hi : Order.IsSuccPrelimit i) (e : (j : (Set.Iio i)) → InverseSystem.PEquivOn f equivSucc (Set.Iic j)) [InverseSystem f] (equivLim : F i (InverseSystem.limit f i)) (H : ∀ (x : F i) (l : (Set.Iio i)), (equivLim x) l = f x) :

                                Extend pEquivOnGlue by one step, obtaining a partial family over a right-closed interval.

                                Equations
                                Instances For
                                  noncomputable def InverseSystem.globalEquiv {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [WellFoundedLT ι] [SuccOrder ι] [InverseSystem f] (equivSucc : (i : ι) → ¬IsMax i{ e : F (Order.succ i) F i × X i // ∀ (x : F (Order.succ i)), (e x).1 = f x }) (equivLim : (i : ι) → Order.IsSuccPrelimit i{ e : F i (InverseSystem.limit f i) // ∀ (x : F i) (l : (Set.Iio i)), (e x) l = f x }) (i : ι) :

                                  Over a well-ordered type, construct a family of bijections by transfinite recursion.

                                  Equations
                                  Instances For
                                    theorem InverseSystem.globalEquiv_naturality {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [WellFoundedLT ι] [SuccOrder ι] [InverseSystem f] (equivSucc : (i : ι) → ¬IsMax i{ e : F (Order.succ i) F i × X i // ∀ (x : F (Order.succ i)), (e x).1 = f x }) (equivLim : (i : ι) → Order.IsSuccPrelimit i{ e : F i (InverseSystem.limit f i) // ∀ (x : F i) (l : (Set.Iio i)), (e x) l = f x }) ⦃i : ι ⦃j : ι (h : i j) (x : F j) :
                                    (InverseSystem.globalEquiv equivSucc equivLim i) (f h x) = InverseSystem.piLTProj h ((InverseSystem.globalEquiv equivSucc equivLim j) x)
                                    theorem InverseSystem.globalEquiv_compatibility {ι : Type u_4} {F : ιType u_5} {X : ιType u_6} [LinearOrder ι] {f : i j : ι⦄ → i jF jF i} [WellFoundedLT ι] [SuccOrder ι] [InverseSystem f] (equivSucc : (i : ι) → ¬IsMax i{ e : F (Order.succ i) F i × X i // ∀ (x : F (Order.succ i)), (e x).1 = f x }) (equivLim : (i : ι) → Order.IsSuccPrelimit i{ e : F i (InverseSystem.limit f i) // ∀ (x : F i) (l : (Set.Iio i)), (e x) l = f x }) ⦃i : ι (hi : ¬IsMax i) (x : F (Order.succ i)) :
                                    (InverseSystem.globalEquiv equivSucc equivLim (Order.succ i)) x i, = ((equivSucc i hi) x).2