Documentation

Mathlib.CategoryTheory.Presentable.ColimitPresentation

Presentation of a colimit of objects equipped with a presentation #

Main definition: #

source
πŸ”Έ coverage
def CategoryTheory.Limits.ColimitPresentation.Total {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
    Instances For
      source
      πŸ”Έ coverage
      @[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.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
        Instances For
          source
          πŸ”Ά coverage
          structure CategoryTheory.Limits.ColimitPresentation.Total.Hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, u_2} (I j)] {D : Functor J C} {P : (j : J) β†’ ColimitPresentation (I j) (D.obj j)} (k l : Total P) :
          Type (max v v_1)

          Morphisms in the Total category.

          Instances For
            source
            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.{v_1, u_1} J} {inst✝² : (j : J) β†’ Category.{u_3, 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
            source
            πŸ“ coverage
            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.{v_1, u_1} J} {inst✝² : (j : J) β†’ Category.{u_3, 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
            source
            πŸ“ coverage
            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.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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)
            source
            πŸ”Έ coverage
            def CategoryTheory.Limits.ColimitPresentation.Total.Hom.comp {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
              Instances For
                source
                πŸ“ coverage
                @[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.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
                source
                πŸ“ coverage
                @[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.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
                source
                πŸ”Έ coverage
                instance CategoryTheory.Limits.ColimitPresentation.instCategoryTotal {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, u_2} (I j)] {D : Functor J C} {P : (j : J) β†’ ColimitPresentation (I j) (D.obj j)} :
                Category.{max v v_1, max u_2 u_1} (Total P)
                Equations
                  source
                  πŸ“ coverage
                  @[simp]
                  theorem CategoryTheory.Limits.ColimitPresentation.id_hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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)
                  source
                  πŸ“ coverage
                  @[simp]
                  theorem CategoryTheory.Limits.ColimitPresentation.comp_hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
                  source
                  πŸ“ coverage
                  @[simp]
                  theorem CategoryTheory.Limits.ColimitPresentation.id_base {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
                  source
                  πŸ“ coverage
                  @[simp]
                  theorem CategoryTheory.Limits.ColimitPresentation.comp_base {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, 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
                  source
                  πŸ“ coverage
                  instance CategoryTheory.Limits.ColimitPresentation.instLocallySmallTotal {C : Type u} [Category.{v, u} C] {J : Type u_1} {I : J β†’ Type u_2} [Category.{v_1, u_1} J] [(j : J) β†’ Category.{u_3, u_2} (I j)] {D : Functor J C} {P : (j : J) β†’ ColimitPresentation (I j) (D.obj j)} [LocallySmall.{w, v, u} C] [LocallySmall.{w, v_1, u_1} J] :
                  LocallySmall.{w, max v v_1, max u_2 u_1} (Total P)
                  source
                  πŸ“ coverage
                  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
                  source
                  πŸ“ coverage
                  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)
                  source
                  πŸ“ coverage
                  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)
                  source
                  πŸ”Έ coverage
                  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
                    Instances For
                      source
                      πŸ“ coverage
                      @[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
                      source
                      πŸ“ coverage
                      @[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)
                      source
                      πŸ“ coverage
                      @[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