Theorems · Definition · category theory

CategoryTheory.Limits.IndObjectPresentation.extend

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      CategoryTheory.Limits.IndObjectPresentation A →
        (η : A ⟶ B) → [CategoryTheory.IsIso η] → CategoryTheory.Limits.IndObjectPresentation B

If A and B are isomorphic, then an ind-object presentation of A can be extended to an ind-object presentation of B.

Defined in

Mathlib.CategoryTheory.Limits.Indization.IndObject

Cited by

6 results in Mathlib

Foundations

Depth 32 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.IsIso