Documentation

Mathlib.CategoryTheory.SmallObject.WellOrderInductionData

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₀.

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.

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.

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
@[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'
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

The obvious element in d.Extension val₀ ⊥.

Equations

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 < jd.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.

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