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

The first part of this file concerns directed systems: DirectLimit is defined as the quotient of the disjoint union (Sigma type) by an equivalence relation (Setoid): compare CategoryTheory.Limits.Types.Quot, which is a quotient by a plain relation. Recursion and induction principles for constructing functions from and to DirectLimit and proving things about elements in DirectLimit.

In the second part 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_4) (f : ⦃i j : ι⦄ → i ≤ j → F i → F j) : Prop

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

theorem DirectedSystem.map_self' {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] ⦃i : ι⦄ (x : F i) : (f i i ⋯) x = x

A copy of DirectedSystem.map_self specialized to FunLike, as otherwise the fun i j h ↦ f i j h can confuse the simplifier.

theorem DirectedSystem.map_map' {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] ⦃i j k : ι⦄ (hij : i ≤ j) (hjk : j ≤ k) (x : F i) : (f j k hjk) ((f i j hij) x) = (f i k ⋯) x

A copy of DirectedSystem.map_map specialized to FunLike, as otherwise the fun i j h ↦ f i j h can confuse the simplifier.

def DirectLimit.setoid {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] : Setoid ((i : ι) × F i)

The setoid on the sigma type defining the direct limit.

Equations

• DirectLimit.setoid f = { r := fun (x y : (i : ι) × F i) => ∃ (i : ι) (hx : x.fst ≤ i) (hy : y.fst ≤ i), (f x.fst i hx) x.snd = (f y.fst i hy) y.snd, iseqv := ⋯ }

theorem DirectLimit.r_of_le {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (x : (i : ι) × F i) (i : ι) (h : x.fst ≤ i) : (DirectLimit.setoid f) x ⟨i, (f x.fst i h) x.snd⟩

@[reducible, inline]

abbrev DirectLimit {ι : Type u_1} [Preorder ι] (F : ι → Type u_4) {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] : Type (max u_4 u_1)

The direct limit of a directed system.

Equations

• DirectLimit F f = Quotient (DirectLimit.setoid f)

theorem DirectLimit.eq_of_le {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} {f : (i j : ι) → (h : i ≤ j) → T h} [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (x : (i : ι) × F i) (i : ι) (h : x.fst ≤ i) : ⟦x⟧ = ⟦⟨i, (f x.fst i h) x.snd⟩⟧

theorem DirectLimit.induction {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : DirectLimit F f → Prop} (ih : ∀ (i : ι) (x : F i), C ⟦⟨i, x⟩⟧) (x : DirectLimit F f) : C x

theorem DirectLimit.exists_eq_mk {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (z : DirectLimit F f) : ∃ (i : ι) (x : F i), z = ⟦⟨i, x⟩⟧

theorem DirectLimit.exists_eq_mk₂ {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (z w : DirectLimit F f) : ∃ (i : ι) (x : F i) (y : F i), z = ⟦⟨i, x⟩⟧ ∧ w = ⟦⟨i, y⟩⟧

theorem DirectLimit.exists_eq_mk₃ {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (w u v : DirectLimit F f) : ∃ (i : ι) (x : F i) (y : F i) (z : F i), w = ⟦⟨i, x⟩⟧ ∧ u = ⟦⟨i, y⟩⟧ ∧ v = ⟦⟨i, z⟩⟧

theorem DirectLimit.induction₂ {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : DirectLimit F f → DirectLimit F f → Prop} (ih : ∀ (i : ι) (x y : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧) (x y : DirectLimit F f) : C x y

theorem DirectLimit.induction₃ {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : DirectLimit F f → DirectLimit F f → DirectLimit F f → Prop} (ih : ∀ (i : ι) (x y z : F i), C ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ ⟦⟨i, z⟩⟧) (x y z : DirectLimit F f) : C x y z

theorem DirectLimit.mk_injective {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (h : ∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f i j hij)) (i : ι) : Function.Injective fun (x : F i) => ⟦⟨i, x⟩⟧

noncomputable def DirectLimit.map₀ {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] (ih : (i : ι) → F i) : DirectLimit F f

"Nullary map" to construct an element in the direct limit.

Equations

• DirectLimit.map₀ f ih = ⟦⟨Classical.arbitrary ι, ih (Classical.arbitrary ι)⟩⟧

theorem DirectLimit.map₀_def {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] [Nonempty ι] (ih : (i : ι) → F i) (compat : ∀ (i j : ι) (h : i ≤ j), (f i j h) (ih i) = ih j) (i : ι) : DirectLimit.map₀ f ih = ⟦⟨i, ih i⟩⟧

def DirectLimit.lift {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : Sort u_9} (ih : (i : ι) → F i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)) (z : DirectLimit F f) : C

To define a function from the direct limit, it suffices to provide one function from each component subject to a compatibility condition.

Equations

• DirectLimit.lift f ih compat z = Quotient.recOn z (fun (x : (i : ι) × F i) => ih x.fst x.snd) ⋯

theorem DirectLimit.lift_def {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : Sort u_9} (ih : (i : ι) → F i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)) (x : (i : ι) × F i) : DirectLimit.lift f ih compat ⟦x⟧ = ih x.fst x.snd

theorem DirectLimit.lift_injective {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : Sort u_9} (ih : (i : ι) → F i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F i), ih i x = ih j ((f i j h) x)) (h : ∀ (i : ι), Function.Injective (ih i)) : Function.Injective (DirectLimit.lift f ih compat)

def DirectLimit.map {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (ih : (i : ι) → F₁ i → F₂ i) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) (z : DirectLimit F₁ f₁) : DirectLimit F₂ f₂

To define a function from the direct limit, it suffices to provide one function from each component subject to a compatibility condition.

Equations

• DirectLimit.map f₁ f₂ ih compat z = DirectLimit.lift f₁ (fun (i : ι) (x : F₁ i) => ⟦⟨i, ih i x⟩⟧) ⋯ z

theorem DirectLimit.map_def {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (ih : (i : ι) → F₁ i → F₂ i) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i), (f₂ i j h) (ih i x) = ih j ((f₁ i j h) x)) (x : (i : ι) × F₁ i) : DirectLimit.map f₁ f₂ ih compat ⟦x⟧ = ⟦⟨x.fst, ih x.fst x.snd⟩⟧

noncomputable def DirectLimit.lift₂ {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : Sort u_9} (ih : (i : ι) → F₁ i → F₂ i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)) (z : DirectLimit F₁ f₁) (w : DirectLimit F₂ f₂) : C

To define a binary function from the direct limit, it suffices to provide one binary function from each component subject to a compatibility condition.

Equations

• DirectLimit.lift₂ f₁ f₂ ih compat z w = Quotient.hrecOn₂ z w (fun (x1 : (i : ι) × F₁ i) (x2 : (i : ι) × F₂ i) => ↑(DirectLimit.lift₂Aux✝ f₁ f₂ ih compat x1 x2)) ⋯

theorem DirectLimit.lift₂_def₂ {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : Sort u_9} (ih : (i : ι) → F₁ i → F₂ i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)) (x : (i : ι) × F₁ i) (y : (i : ι) × F₂ i) (i : ι) (hxi : x.fst ≤ i) (hyi : y.fst ≤ i) : DirectLimit.lift₂ f₁ f₂ ih compat ⟦x⟧ ⟦y⟧ = ih i ((f₁ x.fst i hxi) x.snd) ((f₂ y.fst i hyi) y.snd)

theorem DirectLimit.lift₂_def {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] {C : Sort u_9} (ih : (i : ι) → F₁ i → F₂ i → C) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), ih i x y = ih j ((f₁ i j h) x) ((f₂ i j h) y)) (i : ι) (x : F₁ i) (y : F₂ i) : DirectLimit.lift₂ f₁ f₂ ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ih i x y

noncomputable def DirectLimit.map₂ {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {F : ι → Type u_4} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (ih : (i : ι) → F₁ i → F₂ i → F i) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y)) : DirectLimit F₁ f₁ → DirectLimit F₂ f₂ → DirectLimit F f

To define a function from the direct limit, it suffices to provide one function from each component subject to a compatibility condition.

Equations

• DirectLimit.map₂ f₁ f₂ f ih compat = DirectLimit.lift₂ f₁ f₂ (fun (i : ι) (x : F₁ i) (y : F₂ i) => ⟦⟨i, ih i x y⟩⟧) ⋯

theorem DirectLimit.map₂_def₂ {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {F : ι → Type u_4} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (ih : (i : ι) → F₁ i → F₂ i → F i) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y)) (x : (i : ι) × F₁ i) (y : (i : ι) × F₂ i) (i : ι) (hxi : x.fst ≤ i) (hyi : y.fst ≤ i) : DirectLimit.map₂ f₁ f₂ f ih compat ⟦x⟧ ⟦y⟧ = ⟦⟨i, ih i ((f₁ x.fst i hxi) x.snd) ((f₂ y.fst i hyi) y.snd)⟩⟧

theorem DirectLimit.map₂_def {ι : Type u_1} [Preorder ι] {F₁ : ι → Type u_2} {F₂ : ι → Type u_3} {F : ι → Type u_4} {T₁ : ⦃i j : ι⦄ → i ≤ j → Sort u_6} (f₁ : (i j : ι) → (h : i ≤ j) → T₁ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₁ h) (F₁ i) (F₁ j)] [DirectedSystem F₁ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₁ x1 x2 x3)] {T₂ : ⦃i j : ι⦄ → i ≤ j → Sort u_7} (f₂ : (i j : ι) → (h : i ≤ j) → T₂ h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T₂ h) (F₂ i) (F₂ j)] [DirectedSystem F₂ fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f₂ x1 x2 x3)] {T : ⦃i j : ι⦄ → i ≤ j → Sort u_8} (f : (i j : ι) → (h : i ≤ j) → T h) [⦃i j : ι⦄ → (h : i ≤ j) → FunLike (T h) (F i) (F j)] [DirectedSystem F fun (x1 x2 : ι) (x3 : x1 ≤ x2) => ⇑(f x1 x2 x3)] [IsDirected ι fun (x1 x2 : ι) => x1 ≤ x2] (ih : (i : ι) → F₁ i → F₂ i → F i) (compat : ∀ (i j : ι) (h : i ≤ j) (x : F₁ i) (y : F₂ i), (f i j h) (ih i x y) = ih j ((f₁ i j h) x) ((f₂ i j h) y)) (i : ι) (x : F₁ i) (y : F₂ i) : DirectLimit.map₂ f₁ f₂ f ih compat ⟦⟨i, x⟩⟧ ⟦⟨i, y⟩⟧ = ⟦⟨i, ih i x y⟩⟧

class InverseSystem {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} (f : ⦃i j : ι⦄ → i ≤ j → F j → F i) : Prop

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

def InverseSystem.limit {ι : Type u_1} [Preorder ι] {F : ι → Type u_4} (f : ⦃i j : ι⦄ → i ≤ j → F j → F i) (i : ι) : Set ((l : ↑(Set.Iio i)) → F ↑l)

The inverse limit of an inverse system of types.

Equations

• InverseSystem.limit f i = {F_1 : (l : ↑(Set.Iio i)) → F ↑l | ∀ ⦃j k : ↑(Set.Iio i)⦄ (h : ↑j ≤ ↑k), f h (F_1 k) = F_1 j}

@[reducible, inline]

abbrev InverseSystem.piLT {ι : Type u_1} [Preorder ι] (X : ι → Type u_6) (i : ι) : Type (max u_1 u_6)

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

• InverseSystem.piLT X i = ((l : ↑(Set.Iio i)) → X ↑l)

@[reducible, inline]

abbrev InverseSystem.piLTProj {ι : Type u_1} [Preorder ι] {X : ι → Type u_5} ⦃i j : ι⦄ (h : i ≤ j) (f : InverseSystem.piLT X j) : InverseSystem.piLT X i

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

Equations

• InverseSystem.piLTProj h f l = f ⟨↑l, ⋯⟩

theorem InverseSystem.piLTProj_intro {ι : Type u_1} [Preorder ι] {X : ι → Type u_5} ⦃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_4} {X : ι → Type u_5} (f : ⦃i j : ι⦄ → i ≤ j → F j → F i) {s : Set ι} (equiv : (j : ↑s) → F ↑j ≃ InverseSystem.piLT X ↑j) : Prop

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

Equations

• InverseSystem.IsNatEquiv f equiv = ∀ ⦃j k : ι⦄ (hj : j ∈ s) (hk : k ∈ s) (h : k ≤ j) (x : F j), (equiv ⟨k, hk⟩) (f h x) = InverseSystem.piLTProj h ((equiv ⟨j, hj⟩) x)

noncomputable def InverseSystem.piLTLim {ι : Type u_6} [LinearOrder ι] {X : ι → Type u_7} {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.

@[simp]

theorem InverseSystem.piLTLim_apply {ι : Type u_6} [LinearOrder ι] {X : ι → Type u_7} {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_6} [LinearOrder ι] {X : ι → Type u_7} {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_6} {X : ι → Type u_8} {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.

@[simp]

theorem InverseSystem.piSplitLE_eq {ι : Type u_6} {X : ι → Type u_8} {i : ι} [PartialOrder ι] [DecidableEq ι] {f : InverseSystem.piLT X i × X i} : InverseSystem.piSplitLE f ⟨i, ⋯⟩ = f.2

theorem InverseSystem.piSplitLE_lt {ι : Type u_6} {X : ι → Type u_8} {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_6} {F : ι → Type u_7} {X : ι → Type u_8} {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.

theorem InverseSystem.piEquivSucc_self {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {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_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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) : InverseSystem.IsNatEquiv f (InverseSystem.piEquivSucc equiv e hi)

def InverseSystem.invLimEquiv {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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.

@[simp]

theorem InverseSystem.invLimEquiv_symm_apply_coe {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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)

@[simp]

theorem InverseSystem.invLimEquiv_apply_coe {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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✝

noncomputable def InverseSystem.piEquivLim {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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

• InverseSystem.piEquivLim nat equivLim hi = InverseSystem.piSplitLE (equiv, equivLim.trans ((InverseSystem.invLimEquiv nat).trans (InverseSystem.piLTLim hi).symm))

theorem InverseSystem.isNatEquiv_piEquivLim {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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) : InverseSystem.IsNatEquiv f (InverseSystem.piEquivLim nat equivLim hi)

structure InverseSystem.PEquivOn {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] (f : ⦃i j : ι⦄ → i ≤ j → F j → F i) [SuccOrder ι] (equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i) (s : Set ι) : Type (max (max u_6 u_7) u_8)

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.

theorem InverseSystem.PEquivOn.ext {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {inst✝ : LinearOrder ι} {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} {inst✝¹ : SuccOrder ι} {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι} {x y : InverseSystem.PEquivOn f equivSucc s} (equiv : x.equiv = y.equiv) : x = y

def InverseSystem.PEquivOn.restrict {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s t : Set ι} (e : InverseSystem.PEquivOn f equivSucc t) (h : s ⊆ t) : InverseSystem.PEquivOn f equivSucc s

Restrict a partial family of bijections to a smaller set.

Equations

• e.restrict h = { equiv := fun (i : ↑s) => e.equiv ⟨↑i, ⋯⟩, nat := ⋯, compat := ⋯ }

@[simp]

theorem InverseSystem.PEquivOn.restrict_equiv {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s 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_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s : Set ι} [WellFoundedLT ι] (hs : IsLowerSet s) {e₁ e₂ : InverseSystem.PEquivOn f equivSucc s} : e₁ = e₂

theorem InverseSystem.pEquivOn_apply_eq {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} {s 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_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (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) : InverseSystem.PEquivOn f equivSucc (Set.Iic (Order.succ i))

Extend a partial family of bijections by one step.

Equations

• InverseSystem.pEquivOnSucc hi e H = { equiv := InverseSystem.piEquivSucc e.equiv (equivSucc hi) hi, nat := ⋯, compat := ⋯ }

noncomputable def InverseSystem.pEquivOnGlue {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (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.PEquivOn f equivSucc (Set.Iio i)

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

Equations

• InverseSystem.pEquivOnGlue hi e = { equiv := (InverseSystem.piLTLim hi).symm ⟨fun (j : ↑(Set.Iio i)) => ((e j).restrict ⋯).equiv, ⋯⟩, nat := ⋯, compat := ⋯ }

noncomputable def InverseSystem.pEquivOnLim {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} {i : ι} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} [SuccOrder ι] {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (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) : InverseSystem.PEquivOn f equivSucc (Set.Iic i)

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

Equations

• InverseSystem.pEquivOnLim hi e equivLim H = { equiv := InverseSystem.piEquivLim ⋯ equivLim hi, nat := ⋯, compat := ⋯ }

noncomputable def InverseSystem.globalEquiv {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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 : ι) : F i ≃ InverseSystem.piLT X i

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

Equations

• InverseSystem.globalEquiv equivSucc equivLim i = (InverseSystem.globalEquivAux✝ equivSucc equivLim i).equiv ⟨i, ⋯⟩

theorem InverseSystem.globalEquiv_naturality {ι : Type u_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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_6} {F : ι → Type u_7} {X : ι → Type u_8} [LinearOrder ι] {f : ⦃i j : ι⦄ → i ≤ j → F j → F 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