Documentation

Mathlib.CategoryTheory.Limits.Shapes.Preorder.HasIterationOfShape

An assumption for constructions by transfinite induction #

In this file, we introduce the typeclass HasIterationOfShape J C which is an assumption in order to do constructions by transfinite induction indexed by a well-ordered type J in a category C (see CategoryTheory.SmallObject).

class CategoryTheory.Limits.HasIterationOfShape (J : Type w) [LinearOrder J] (C : Type u) [Category.{v, u} C] :

A category C has iterations of shape a linearly ordered type J when certain specific shapes of colimits exists: colimits indexed by J, and by Set.Iio j for j : J.

hasColimitsOfShape_of_isSuccLimit (j : J) (hj : Order.IsSuccLimit j) : HasColimitsOfShape (↑(Set.Iio j)) C
hasColimitsOfShape : HasColimitsOfShape J C

Instances

instance CategoryTheory.Limits.instHasIterationOfShapeOfHasColimitsOfSize (J : Type w) [LinearOrder J] (C : Type u) [Category.{v, u} C] [HasColimitsOfSize.{w, w, v, u} C] :

HasIterationOfShape J C

theorem CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit {J : Type w} [LinearOrder J] (C : Type u) [Category.{v, u} C] [HasIterationOfShape J C] (j : J) (hj : Order.IsSuccLimit j) :

HasColimitsOfShape (↑(Set.Iio j)) C

theorem CategoryTheory.Limits.hasColimitsOfShape_of_isSuccLimit' {J : Type w} [LinearOrder J] (C : Type u) [Category.{v, u} C] [HasIterationOfShape J C] {α : Type u_1} [PartialOrder α] (h : (fun (x1 x2 : α) => x1 < x2) ≺i fun (x1 x2 : J) => x1 < x2) (hα : Order.IsSuccLimit h.top) :

HasColimitsOfShape α C

instance CategoryTheory.Limits.instHasIterationOfShapeArrow (J : Type w) [LinearOrder J] (C : Type u) [Category.{v, u} C] [HasIterationOfShape J C] :

HasIterationOfShape J (Arrow C)

instance CategoryTheory.Limits.instHasIterationOfShapeFunctor (J : Type w) [LinearOrder J] (C : Type u) [Category.{v, u} C] (K : Type u') [Category.{v', u'} K] [HasIterationOfShape J C] :

HasIterationOfShape J (Functor K C)

theorem CategoryTheory.Limits.hasColimitsOfShape_of_initialSeg {J : Type w} [LinearOrder J] (C : Type u) [Category.{v, u} C] [HasIterationOfShape J C] [SuccOrder J] [WellFoundedLT J] {α : Type u_1} [LinearOrder α] (f : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : J) => x1 < x2) [Nonempty α] :

HasColimitsOfShape α C

theorem CategoryTheory.Limits.hasIterationOfShape_of_initialSeg {J : Type w} [LinearOrder J] (C : Type u) [Category.{v, u} C] [HasIterationOfShape J C] [SuccOrder J] [WellFoundedLT J] {α : Type u_1} [LinearOrder α] (h : (fun (x1 x2 : α) => x1 < x2) ≼i fun (x1 x2 : J) => x1 < x2) [Nonempty α] :

HasIterationOfShape α C

instance CategoryTheory.Limits.instHasIterationOfShapeElemIic {J : Type w} [LinearOrder J] (C : Type u) [Category.{v, u} C] [HasIterationOfShape J C] [SuccOrder J] [WellFoundedLT J] (j : J) :

HasIterationOfShape (↑(Set.Iic j)) C