Limits of inverse systems indexed by well-ordered types

Given a functor F : Jᵒᵖ ⥤ Type v where J is a well-ordered type, we introduce a structure F.WellOrderInductionData which allows to show that the map F.sections → F.obj (op ⊥) is surjective.

The data and properties in F.WellOrderInductionData consist of a section to the maps F.obj (op (Order.succ j)) → F.obj (op j) when j is not maximal, and, when j is limit, a section to the canonical map from F.obj (op j) to the type of compatible families of elements in F.obj (op i) for i < j.

In other words, from val₀ : F.obj (op ⊥), a term d : F.WellOrderInductionData allows the construction, by transfinite induction, of a section of F which restricts to val₀.

structure CategoryTheory.Functor.WellOrderInductionData {J : Type u} [LinearOrder J] [SuccOrder J] (F : Functor Jᵒᵖ (Type v)) : Type (max u v)

Given a functor F : Jᵒᵖ ⥤ Type v where J is a well-ordered type, this data allows to construct a section of F from an element in F.obj (op ⊥), see WellOrderInductionData.sectionsMk.

• succ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)) : F.obj (Opposite.op (Order.succ j))

  A section F.obj (op j) → F.obj (op (Order.succ j)) to the restriction F.obj (op (Order.succ j)) → F.obj (op j) when j is not maximal.

• map_succ (j : J) (hj : ¬IsMax j) (x : F.obj (Opposite.op j)) : F.map (homOfLE ⋯).op (self.succ j hj x) = x
• lift (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) : F.obj (Opposite.op j)

  When j is a limit element, and x is a compatible family of elements in F.obj (op i) for all i < j, this is a lifting to F.obj (op j).

• map_lift (j : J) (hj : Order.IsSuccLimit j) (x : ↑(⋯.functor.op.comp F).sections) (i : J) (hi : i < j) : F.map (homOfLE ⋯).op (self.lift j hj x) = ↑x (Opposite.op ⟨i, hi⟩)

structure CategoryTheory.Functor.WellOrderInductionData.Extension {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} (d : F.WellOrderInductionData) [OrderBot J] (val₀ : F.obj (Opposite.op ⊥)) (j : J) : Type v

Given d : F.WellOrderInductionData, val₀ : F.obj (op ⊥) and j : J, this is the data of an element val : F.obj (op j) such that the induced compatible family of elements in all F.obj (op i) for i ≤ j is determined by val₀ and the choice of "liftings" given by d.

• val : F.obj (Opposite.op j)

  An element in F.obj (op j), which, by restriction, induces elements in F.obj (op i) for all i ≤ j.

• map_zero : F.map (homOfLE ⋯).op self.val = val₀
• map_succ (i : J) (hi : i < j) : F.map (homOfLE ⋯).op self.val = d.succ i ⋯ (F.map (homOfLE ⋯).op self.val)
• map_limit (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) : F.map (homOfLE hij).op self.val = d.lift i hi ⟨fun (x : { x : J // x ∈ Set.Iio i }ᵒᵖ) => match x with | Opposite.op ⟨k, hk⟩ => F.map (homOfLE ⋯).op self.val, ⋯⟩

def CategoryTheory.Functor.WellOrderInductionData.Extension.ofLE {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} (e : d.Extension val₀ j) {i : J} (hij : i ≤ j) : d.Extension val₀ i

An element in d.Extension val₀ j induces an element in d.Extension val₀ i when i ≤ j.

Equations

• e.ofLE hij = { val := F.map (CategoryTheory.homOfLE hij).op e.val, map_zero := ⋯, map_succ := ⋯, map_limit := ⋯ }

@[simp]

theorem CategoryTheory.Functor.WellOrderInductionData.Extension.ofLE_val {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} (e : d.Extension val₀ j) {i : J} (hij : i ≤ j) : (e.ofLE hij).val = F.map (homOfLE hij).op e.val

theorem CategoryTheory.Functor.WellOrderInductionData.Extension.val_injective {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} {e e' : d.Extension val₀ j} (h : e.val = e'.val) : e = e'

instance CategoryTheory.Functor.WellOrderInductionData.Extension.instSubsingletonOfWellFoundedLT {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] (j : J) : Subsingleton (d.Extension val₀ j)

theorem CategoryTheory.Functor.WellOrderInductionData.Extension.compatibility {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] {j : J} (e : d.Extension val₀ j) {i : J} (e' : d.Extension val₀ i) (h : i ≤ j) : F.map (homOfLE h).op e.val = e'.val

def CategoryTheory.Functor.WellOrderInductionData.Extension.zero {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} (d : F.WellOrderInductionData) [OrderBot J] (val₀ : F.obj (Opposite.op ⊥)) : d.Extension val₀ ⊥

The obvious element in d.Extension val₀ ⊥.

Equations

• CategoryTheory.Functor.WellOrderInductionData.Extension.zero d val₀ = { val := val₀, map_zero := ⋯, map_succ := ⋯, map_limit := ⋯ }

@[simp]

theorem CategoryTheory.Functor.WellOrderInductionData.Extension.zero_val {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} (d : F.WellOrderInductionData) [OrderBot J] (val₀ : F.obj (Opposite.op ⊥)) : (zero d val₀).val = val₀

def CategoryTheory.Functor.WellOrderInductionData.Extension.succ {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J} (e : d.Extension val₀ j) (hj : ¬IsMax j) : d.Extension val₀ (Order.succ j)

The element in d.Extension val₀ (Order.succ j) obtained by extending an element in d.Extension val₀ j when j is not maximal.

Equations

• e.succ hj = { val := d.succ j hj e.val, map_zero := ⋯, map_succ := ⋯, map_limit := ⋯ }

def CategoryTheory.Functor.WellOrderInductionData.Extension.limit {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] (j : J) (hj : Order.IsSuccLimit j) (e : (i : J) → i < j → d.Extension val₀ i) : d.Extension val₀ j

When j is a limit element, this is the exntesion to d.Extension val₀ j of a family of elements in d.Extension val₀ i for all i < j.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Functor.WellOrderInductionData.Extension.instNonempty {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] (j : J) : Nonempty (d.Extension val₀ j)

noncomputable instance CategoryTheory.Functor.WellOrderInductionData.Extension.instUnique {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} {d : F.WellOrderInductionData} [OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} [WellFoundedLT J] (j : J) : Unique (d.Extension val₀ j)

Equations

• CategoryTheory.Functor.WellOrderInductionData.Extension.instUnique j = uniqueOfSubsingleton ⋯.some

noncomputable def CategoryTheory.Functor.WellOrderInductionData.sectionsMk {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} (d : F.WellOrderInductionData) [OrderBot J] [WellFoundedLT J] (val₀ : F.obj (Opposite.op ⊥)) : ↑F.sections

When J is a well-ordered type, F : Jᵒᵖ ⥤ Type v, and d : F.WellOrderInductionData, this is the section of F that is determined by val₀ : F.obj (op ⊥)

Equations

• d.sectionsMk val₀ = ⟨fun (j : Jᵒᵖ) => default.val, ⋯⟩

theorem CategoryTheory.Functor.WellOrderInductionData.sectionsMk_val_op_bot {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} (d : F.WellOrderInductionData) [OrderBot J] [WellFoundedLT J] (val₀ : F.obj (Opposite.op ⊥)) : ↑(d.sectionsMk val₀) (Opposite.op ⊥) = val₀

theorem CategoryTheory.Functor.WellOrderInductionData.surjective {J : Type u} [LinearOrder J] [SuccOrder J] {F : Functor Jᵒᵖ (Type v)} (d : F.WellOrderInductionData) [OrderBot J] [WellFoundedLT J] : Function.Surjective ((fun (s : (j : Jᵒᵖ) → F.obj j) => s (Opposite.op ⊥)) ∘ Subtype.val)