(Co)limit presentations

Let J and C be categories and X : C. We define type ColimitPresentation J X that contains the data of objects Dⱼ and natural maps sⱼ : Dⱼ ⟶ X that make X the colimit of the Dⱼ.

Main definitions:

• CategoryTheory.Limits.ColimitPresentation: A colimit presentation of X over J is a diagram {Dᵢ} in C and natural maps sᵢ : Dᵢ ⟶ X making X into the colimit of the Dᵢ.
• CategoryTheory.Limits.ColimitPresentation.bind: Given a colimit presentation of X and colimit presentations of the components, this is the colimit presentation over the sigma type.
• CategoryTheory.Limits.LimitPresentation: A limit presentation of X over J is a diagram {Dᵢ} in C and natural maps sᵢ : X ⟶ Dᵢ making X into the limit of the Dᵢ.

TODOs:

• Refactor TransfiniteCompositionOfShape so that it extends ColimitPresentation.

structure CategoryTheory.Limits.ColimitPresentation {C : Type u} [Category.{v, u} C] (J : Type w) [Category.{t, w} J] (X : C) : Type (max (max (max t u) v) w)

A colimit presentation of X over J is a diagram {Dᵢ} in C and natural maps sᵢ : Dᵢ ⟶ X making X into the colimit of the Dᵢ.

• diag : Functor J C

  The diagram {Dᵢ}.

• ι : self.diag ⟶ (Functor.const J).obj X

  The natural maps sᵢ : Dᵢ ⟶ X.

• isColimit : IsColimit { pt := X, ι := self.ι }

  X is the colimit of the Dᵢ via sᵢ.

@[reducible, inline]

abbrev CategoryTheory.Limits.ColimitPresentation.cocone {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (pres : ColimitPresentation J X) : Cocone pres.diag

The cocone associated to a colimit presentation.

Equations

• pres.cocone = { pt := X, ι := pres.ι }

theorem CategoryTheory.Limits.ColimitPresentation.hasColimit {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (pres : ColimitPresentation J X) : HasColimit pres.diag

noncomputable def CategoryTheory.Limits.ColimitPresentation.self {C : Type u} [Category.{v, u} C] (X : C) : ColimitPresentation PUnit.{s + 1} X

The canonical colimit presentation of any object over a point.

Equations

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

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.self_diag {C : Type u} [Category.{v, u} C] (X : C) : (self X).diag = (Functor.const PUnit.{s + 1}).obj X

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.self_ι {C : Type u} [Category.{v, u} C] (X : C) : (self X).ι = CategoryStruct.id ((Functor.const PUnit.{s + 1}).obj X)

noncomputable def CategoryTheory.Limits.ColimitPresentation.colimit {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] (F : Functor J C) [HasColimit F] : ColimitPresentation J (Limits.colimit F)

If F : J ⥤ C is a functor that has a colimit, then this is the obvious colimit presentation of colimit F.

Equations

• CategoryTheory.Limits.ColimitPresentation.colimit F = { diag := F, ι := (CategoryTheory.Limits.getColimitCocone F).1.ι, isColimit := CategoryTheory.Limits.colimit.isColimit F }

noncomputable def CategoryTheory.Limits.ColimitPresentation.map {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [PreservesColimitsOfShape J F] : ColimitPresentation J (F.obj X)

If F preserves colimits of shape J, it maps colimit presentations of X to colimit presentations of F(X).

Equations

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

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.map_ι {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [PreservesColimitsOfShape J F] : (P.map F).ι = CategoryStruct.comp (Functor.whiskerRight P.ι F) (Functor.constComp J X F).hom

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.map_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [PreservesColimitsOfShape J F] : (P.map F).diag = P.diag.comp F

def CategoryTheory.Limits.ColimitPresentation.changeDiag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {F : Functor J C} (e : F ≅ P.diag) : ColimitPresentation J X

If P is a colimit presentation of X, it is possible to define another colimit presentation of X where P.diag is replaced by an isomorphic functor.

Equations

• P.changeDiag e = { diag := F, ι := CategoryTheory.CategoryStruct.comp e.hom P.ι, isColimit := (CategoryTheory.Limits.IsColimit.precomposeHomEquiv e { pt := X, ι := P.ι }).invFun P.isColimit }

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.changeDiag_ι {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {F : Functor J C} (e : F ≅ P.diag) : (P.changeDiag e).ι = CategoryStruct.comp e.hom P.ι

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.changeDiag_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {F : Functor J C} (e : F ≅ P.diag) : (P.changeDiag e).diag = F

def CategoryTheory.Limits.ColimitPresentation.ofIso {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {Y : C} (e : X ≅ Y) : ColimitPresentation J Y

Map a colimit presentation under an isomorphism.

Equations

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

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.ofIso_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {Y : C} (e : X ≅ Y) : (P.ofIso e).diag = P.diag

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.ofIso_ι {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {Y : C} (e : X ≅ Y) : (P.ofIso e).ι = CategoryStruct.comp P.ι ((Functor.const J).map e.hom)

noncomputable def CategoryTheory.Limits.ColimitPresentation.reindex {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {J' : Type u_1} [Category.{u_2, u_1} J'] (F : Functor J' J) [F.Final] : ColimitPresentation J' X

Change the index category of a colimit presentation.

Equations

• P.reindex F = { diag := F.comp P.diag, ι := F.whiskerLeft P.ι, isColimit := (CategoryTheory.Functor.Final.isColimitWhiskerEquiv F { pt := X, ι := P.ι }).symm P.isColimit }

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.reindex_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {J' : Type u_1} [Category.{u_2, u_1} J'] (F : Functor J' J) [F.Final] : (P.reindex F).diag = F.comp P.diag

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.reindex_ι {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : ColimitPresentation J X) {J' : Type u_1} [Category.{u_2, u_1} J'] (F : Functor J' J) [F.Final] : (P.reindex F).ι = F.whiskerLeft P.ι

def CategoryTheory.Limits.ColimitPresentation.Total {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} (P : (j : J) → ColimitPresentation (I j) (D.obj j)) : Type (max u_2 u_1)

The type underlying the category used in the construction of the composition of colimit presentations. This is simply Σ j, I j but with a different category structure.

Equations

• CategoryTheory.Limits.ColimitPresentation.Total P = ((j : J) × I j)

@[reducible, inline]

abbrev CategoryTheory.Limits.ColimitPresentation.Total.mk {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} (P : (j : J) → ColimitPresentation (I j) (D.obj j)) (i : J) (k : I i) : Total P

Constructor for Total to guide type checking.

Equations

• CategoryTheory.Limits.ColimitPresentation.Total.mk P i k = ⟨i, k⟩

structure CategoryTheory.Limits.ColimitPresentation.Total.Hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} (k l : Total P) : Type (max u_3 v)

Morphisms in the Total category.

• base : k.fst ⟶ l.fst

  The underlying morphism in the first component.

• hom : (P k.fst).diag.obj k.snd ⟶ (P l.fst).diag.obj l.snd

  A morphism in C.

• w : CategoryStruct.comp ((P k.fst).ι.app k.snd) (D.map self.base) = CategoryStruct.comp self.hom ((P l.fst).ι.app l.snd)

theorem CategoryTheory.Limits.ColimitPresentation.Total.Hom.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {J : Type u_1} {I : J → Type u_2} {inst✝¹ : Category.{u_3, u_1} J} {inst✝² : (j : J) → Category.{u_4, u_2} (I j)} {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {k l : Total P} {x y : k.Hom l} : x = y ↔ x.base = y.base ∧ x.hom = y.hom

theorem CategoryTheory.Limits.ColimitPresentation.Total.Hom.ext {C : Type u} {inst✝ : Category.{v, u} C} {J : Type u_1} {I : J → Type u_2} {inst✝¹ : Category.{u_3, u_1} J} {inst✝² : (j : J) → Category.{u_4, u_2} (I j)} {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {k l : Total P} {x y : k.Hom l} (base : x.base = y.base) (hom : x.hom = y.hom) : x = y

theorem CategoryTheory.Limits.ColimitPresentation.Total.Hom.w_assoc {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {k l : Total P} (self : k.Hom l) {Z : C} (h : D.obj l.fst ⟶ Z) : CategoryStruct.comp ((P k.fst).ι.app k.snd) (CategoryStruct.comp (D.map self.base) h) = CategoryStruct.comp self.hom (CategoryStruct.comp ((P l.fst).ι.app l.snd) h)

def CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {k l m : Total P} (f : k.Hom l) (g : l.Hom m) : k.Hom m

Composition of morphisms in the Total category.

Equations

• f.comp g = { base := CategoryTheory.CategoryStruct.comp f.base g.base, hom := CategoryTheory.CategoryStruct.comp f.hom g.hom, w := ⋯ }

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp_base {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {k l m : Total P} (f : k.Hom l) (g : l.Hom m) : (f.comp g).base = CategoryStruct.comp f.base g.base

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp_hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {k l m : Total P} (f : k.Hom l) (g : l.Hom m) : (f.comp g).hom = CategoryStruct.comp f.hom g.hom

instance CategoryTheory.Limits.ColimitPresentation.instCategoryTotal {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} : Category.{max v u_3, max u_2 u_1} (Total P)

Equations

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

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.id_base {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} (x✝ : Total P) : (CategoryStruct.id x✝).base = CategoryStruct.id x✝.fst

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.comp_hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {X✝ Y✝ Z✝ : Total P} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).hom = CategoryStruct.comp f.hom g.hom

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.comp_base {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {X✝ Y✝ Z✝ : Total P} (f : X✝.Hom Y✝) (g : Y✝.Hom Z✝) : (CategoryStruct.comp f g).base = CategoryStruct.comp f.base g.base

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.id_hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} (x✝ : Total P) : (CategoryStruct.id x✝).hom = CategoryStruct.id ((P x✝.fst).diag.obj x✝.snd)

instance CategoryTheory.Limits.ColimitPresentation.instLocallySmallTotal {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J → Type u_2} [Category.{u_3, u_1} J] [(j : J) → Category.{u_4, u_2} (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} [LocallySmall.{w, v, u} C] [LocallySmall.{w, u_3, u_1} J] : LocallySmall.{w, max v u_3, max u_2 u_1} (Total P)

theorem CategoryTheory.Limits.ColimitPresentation.Total.exists_hom_of_hom {C : Type u} [Category.{v, u} C] {J : Type w} {I : J → Type w} [SmallCategory J] [(j : J) → SmallCategory (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} {j j' : J} (i : I j) (u : j ⟶ j') [IsFiltered (I j')] [IsFinitelyPresentable ((P j).diag.obj i)] : ∃ (i' : I j') (f : mk P j i ⟶ mk P j' i'), f.base = u

instance CategoryTheory.Limits.ColimitPresentation.instNonemptyTotalOfIsFiltered {C : Type u} [Category.{v, u} C] {J : Type w} {I : J → Type w} [SmallCategory J] [(j : J) → SmallCategory (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} [IsFiltered J] [∀ (j : J), IsFiltered (I j)] : Nonempty (Total P)

instance CategoryTheory.Limits.ColimitPresentation.instIsFilteredTotalOfIsFinitelyPresentableObjDiag {C : Type u} [Category.{v, u} C] {J : Type w} {I : J → Type w} [SmallCategory J] [(j : J) → SmallCategory (I j)] {D : Functor J C} {P : (j : J) → ColimitPresentation (I j) (D.obj j)} [IsFiltered J] [∀ (j : J), IsFiltered (I j)] [∀ (j : J) (i : I j), IsFinitelyPresentable ((P j).diag.obj i)] : IsFiltered (Total P)

def CategoryTheory.Limits.ColimitPresentation.bind {C : Type u} [Category.{v, u} C] {J : Type w} {I : J → Type w} [SmallCategory J] [(j : J) → SmallCategory (I j)] {X : C} (P : ColimitPresentation J X) (Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), IsFiltered (I j)] [∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)] : ColimitPresentation (Total Q) X

If P is a colimit presentation over J of X and for every j we are given a colimit presentation Qⱼ over I j of the P.diag.obj j, this is the refined colimit presentation of X over Total Q.

Equations

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

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.bind_diag_obj {C : Type u} [Category.{v, u} C] {J : Type w} {I : J → Type w} [SmallCategory J] [(j : J) → SmallCategory (I j)] {X : C} (P : ColimitPresentation J X) (Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), IsFiltered (I j)] [∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)] (k : Total Q) : (P.bind Q).diag.obj k = (Q k.fst).diag.obj k.snd

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.bind_ι_app {C : Type u} [Category.{v, u} C] {J : Type w} {I : J → Type w} [SmallCategory J] [(j : J) → SmallCategory (I j)] {X : C} (P : ColimitPresentation J X) (Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), IsFiltered (I j)] [∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)] (k : Total Q) : (P.bind Q).ι.app k = CategoryStruct.comp ((Q k.fst).ι.app k.snd) (P.ι.app k.fst)

@[simp]

theorem CategoryTheory.Limits.ColimitPresentation.bind_diag_map {C : Type u} [Category.{v, u} C] {J : Type w} {I : J → Type w} [SmallCategory J] [(j : J) → SmallCategory (I j)] {X : C} (P : ColimitPresentation J X) (Q : (j : J) → ColimitPresentation (I j) (P.diag.obj j)) [∀ (j : J), IsFiltered (I j)] [∀ (j : J) (i : I j), IsFinitelyPresentable ((Q j).diag.obj i)] {k l : Total Q} (f : k ⟶ l) : (P.bind Q).diag.map f = f.hom

structure CategoryTheory.Limits.LimitPresentation {C : Type u} [Category.{v, u} C] (J : Type w) [Category.{t, w} J] (X : C) : Type (max (max (max t u) v) w)

A limit presentation of X over J is a diagram {Dᵢ} in C and natural maps sᵢ : X ⟶ Dᵢ making X into the limit of the Dᵢ.

• diag : Functor J C

  The diagram {Dᵢ}.

• π : (Functor.const J).obj X ⟶ self.diag

  The natural maps sᵢ : X ⟶ Dᵢ.

• isLimit : IsLimit { pt := X, π := self.π }

  X is the limit of the Dᵢ via sᵢ.

@[reducible, inline]

abbrev CategoryTheory.Limits.LimitPresentation.cone {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (pres : LimitPresentation J X) : Cone pres.diag

The cone associated to a limit presentation.

Equations

• pres.cone = { pt := X, π := pres.π }

theorem CategoryTheory.Limits.LimitPresentation.hasLimit {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (pres : LimitPresentation J X) : HasLimit pres.diag

noncomputable def CategoryTheory.Limits.LimitPresentation.self {C : Type u} [Category.{v, u} C] (X : C) : LimitPresentation PUnit.{s + 1} X

The canonical limit presentation of any object over a point.

Equations

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

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.self_π {C : Type u} [Category.{v, u} C] (X : C) : (self X).π = CategoryStruct.id ((Functor.const PUnit.{s + 1}).obj X)

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.self_diag {C : Type u} [Category.{v, u} C] (X : C) : (self X).diag = (Functor.const PUnit.{s + 1}).obj X

noncomputable def CategoryTheory.Limits.LimitPresentation.limit {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] (F : Functor J C) [HasLimit F] : LimitPresentation J (Limits.limit F)

If F : J ⥤ C is a functor that has a limit, then this is the obvious limit presentation of limit F.

Equations

• CategoryTheory.Limits.LimitPresentation.limit F = { diag := F, π := (CategoryTheory.Limits.getLimitCone F).1.π, isLimit := CategoryTheory.Limits.limit.isLimit F }

noncomputable def CategoryTheory.Limits.LimitPresentation.map {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [PreservesLimitsOfShape J F] : LimitPresentation J (F.obj X)

If F preserves limits of shape J, it maps limit presentations of X to limit presentations of F(X).

Equations

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

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.map_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [PreservesLimitsOfShape J F] : (P.map F).diag = P.diag.comp F

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.map_π {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {D : Type u_1} [Category.{u_2, u_1} D] (F : Functor C D) [PreservesLimitsOfShape J F] : (P.map F).π = CategoryStruct.comp (Functor.constComp J X F).inv (Functor.whiskerRight P.π F)

def CategoryTheory.Limits.LimitPresentation.changeDiag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {F : Functor J C} (e : F ≅ P.diag) : LimitPresentation J X

If P is a limit presentation of X, it is possible to define another limit presentation of X where P.diag is replaced by an isomorphic functor.

Equations

• P.changeDiag e = { diag := F, π := CategoryTheory.CategoryStruct.comp P.π e.inv, isLimit := (CategoryTheory.Limits.IsLimit.postcomposeHomEquiv e.symm { pt := X, π := P.π }).invFun P.isLimit }

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.changeDiag_π {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {F : Functor J C} (e : F ≅ P.diag) : (P.changeDiag e).π = CategoryStruct.comp P.π e.inv

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.changeDiag_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {F : Functor J C} (e : F ≅ P.diag) : (P.changeDiag e).diag = F

def CategoryTheory.Limits.LimitPresentation.ofIso {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {Y : C} (e : X ≅ Y) : LimitPresentation J Y

Map a limit presentation under an isomorphism.

Equations

• P.ofIso e = { diag := P.diag, π := CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.const J).map e.inv) P.π, isLimit := P.isLimit.ofIsoLimit (CategoryTheory.Limits.Cones.ext e ⋯) }

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.ofIso_π {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {Y : C} (e : X ≅ Y) : (P.ofIso e).π = CategoryStruct.comp ((Functor.const J).map e.inv) P.π

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.ofIso_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {Y : C} (e : X ≅ Y) : (P.ofIso e).diag = P.diag

noncomputable def CategoryTheory.Limits.LimitPresentation.reindex {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {J' : Type u_1} [Category.{u_2, u_1} J'] (F : Functor J' J) [F.Initial] : LimitPresentation J' X

Change the index category of a limit presentation.

Equations

• P.reindex F = { diag := F.comp P.diag, π := F.whiskerLeft P.π, isLimit := (CategoryTheory.Functor.Initial.isLimitWhiskerEquiv F { pt := X, π := P.π }).symm P.isLimit }

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.reindex_diag {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {J' : Type u_1} [Category.{u_2, u_1} J'] (F : Functor J' J) [F.Initial] : (P.reindex F).diag = F.comp P.diag

@[simp]

theorem CategoryTheory.Limits.LimitPresentation.reindex_π {C : Type u} [Category.{v, u} C] {J : Type w} [Category.{t, w} J] {X : C} (P : LimitPresentation J X) {J' : Type u_1} [Category.{u_2, u_1} J'] (F : Functor J' J) [F.Initial] : (P.reindex F).π = F.whiskerLeft P.π