Loogle!

Result

Found 135 declarations mentioning CategoryTheory.Functor.mapCocone.

• CategoryTheory.Functor.mapCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Cocone (F.comp H)
• CategoryTheory.Functor.mapCocone_pt 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : (H.mapCocone c).pt = H.obj c.pt
• CategoryTheory.Functor.mapCoconeInvMapCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cocone F) : H.mapCoconeInv (H.mapCocone c) ≅ c
• CategoryTheory.Functor.mapCoconeMapCoconeInv 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D} (H : CategoryTheory.Functor D C) [H.IsEquivalence] (c : CategoryTheory.Limits.Cocone (F.comp H)) : H.mapCocone (H.mapCoconeInv c) ≅ c
• CategoryTheory.Functor.mapCoconeMapCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone F) : H'.mapCocone (H.mapCocone c) ≅ (H.comp H').mapCocone c
• CategoryTheory.Functor.mapCoconeWhisker 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F} : H.mapCocone (CategoryTheory.Limits.Cocone.whisker E c) ≅ CategoryTheory.Limits.Cocone.whisker E (H.mapCocone c)
• CategoryTheory.Functor.mapCoconeOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F) : (G.mapCocone t).op ≅ G.op.mapCone t.op
• CategoryTheory.Functor.mapConeOp 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (G.mapCone t).op ≅ G.op.mapCocone t.op
• CategoryTheory.Functor.mapCoconeMorphism 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c c' : CategoryTheory.Limits.Cocone F} (f : c' ⟶ c) : H.mapCocone c' ⟶ H.mapCocone c
• CategoryTheory.Functor.mapCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) (j : J) : (H.mapCocone c).ι.app j = H.map (c.ι.app j)
• CategoryTheory.Functor.precomposeWhiskerLeftMapCocone 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Limits.Cocone.precompose (F.whiskerLeft α.inv)).obj (H.mapCocone c) ≅ H'.mapCocone c
• CategoryTheory.Functor.mapCoconePrecompose 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : G ⟶ F} {c : CategoryTheory.Limits.Cocone F} : H.mapCocone ((CategoryTheory.Limits.Cocone.precompose α).obj c) ≅ (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Functor.whiskerRight α H)).obj (H.mapCocone c)
• CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone F} : H.mapCocone ((CategoryTheory.Limits.Cocone.precomposeEquivalence α).functor.obj c) ≅ (CategoryTheory.Limits.Cocone.precomposeEquivalence (CategoryTheory.Functor.isoWhiskerRight α H)).functor.obj (H.mapCocone c)
• CategoryTheory.Functor.mapCoconeMapCocone_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.mapCoconeMapCocone c).hom.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
• CategoryTheory.Functor.mapCoconeMapCocone_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {E : Type u₅} [CategoryTheory.Category.{v₅, u₅} E] {F : CategoryTheory.Functor J C} {H : CategoryTheory.Functor C D} {H' : CategoryTheory.Functor D E} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.mapCoconeMapCocone c).inv.hom = CategoryTheory.CategoryStruct.id (H'.obj (H.obj c.pt))
• CategoryTheory.Functor.mapCoconeWhisker_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F} : H.mapCoconeWhisker.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Functor.mapCoconeWhisker_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {E : CategoryTheory.Functor K J} {c : CategoryTheory.Limits.Cocone F} : H.mapCoconeWhisker.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Functor.mapCoconeOp_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.mapCoconeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Functor.mapCoconeOp_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.mapCoconeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Functor.mapConeOp_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeOp G t).hom.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Functor.mapConeOp_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} (G : CategoryTheory.Functor C D) (t : CategoryTheory.Limits.Cone F) : (CategoryTheory.Functor.mapConeOp G t).inv.hom = CategoryTheory.CategoryStruct.id (Opposite.op (G.obj t.pt))
• CategoryTheory.Functor.mapCoconePrecompose_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : G ⟶ F} {c : CategoryTheory.Limits.Cocone F} : H.mapCoconePrecompose.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Functor.mapCoconePrecompose_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : G ⟶ F} {c : CategoryTheory.Limits.Cocone F} : H.mapCoconePrecompose.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).hom.hom = α.hom.app c.pt
• CategoryTheory.Functor.precomposeWhiskerLeftMapCocone_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J C} {H H' : CategoryTheory.Functor C D} (α : H ≅ H') (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Functor.precomposeWhiskerLeftMapCocone α c).inv.hom = α.inv.app c.pt
• CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_hom_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone F} : H.mapCoconePrecomposeEquivalenceFunctor.hom.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Functor.mapCoconePrecomposeEquivalenceFunctor_inv_hom 📋 Mathlib.CategoryTheory.Limits.Cones
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (H : CategoryTheory.Functor C D) {F G : CategoryTheory.Functor J C} {α : F ≅ G} {c : CategoryTheory.Limits.Cocone F} : H.mapCoconePrecomposeEquivalenceFunctor.inv.hom = CategoryTheory.CategoryStruct.id (H.obj c.pt)
• CategoryTheory.Limits.IsColimit.mapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} {F G : CategoryTheory.Functor C D} (h : F ≅ G) {c : CategoryTheory.Limits.Cocone K} (t : CategoryTheory.Limits.IsColimit (F.mapCocone c)) : CategoryTheory.Limits.IsColimit (G.mapCocone c)
• CategoryTheory.Limits.IsColimit.ofFaithful 📋 Mathlib.CategoryTheory.Limits.IsLimit
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] (G : CategoryTheory.Functor C D) [G.Faithful] (ht : CategoryTheory.Limits.IsColimit (G.mapCocone t)) (desc : (s : CategoryTheory.Limits.Cocone F) → t.pt ⟶ s.pt) (h : ∀ (s : CategoryTheory.Limits.Cocone F), G.map (desc s) = ht.desc (G.mapCocone s)) : CategoryTheory.Limits.IsColimit t
• CategoryTheory.Limits.colimit.post_desc 📋 Mathlib.CategoryTheory.Limits.HasLimits
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasColimit F] (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasColimit (F.comp G)] (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.post F G) (G.map (CategoryTheory.Limits.colimit.desc F c)) = CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone c)
• CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.Products
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {ι : Type u_1} (X : ι → C) (c : CategoryTheory.Limits.Cofan X) : CategoryTheory.Limits.IsColimit (F.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (F.obj c.pt) fun i => F.map (c.inj i))
• CategoryTheory.Limits.BinaryCofan.isColimitMapConeEquiv 📋 Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts.BinaryFan
  {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] {F : CategoryTheory.Functor C D} {X Y : C} {s : CategoryTheory.Limits.BinaryCofan X Y} : CategoryTheory.Limits.IsColimit (F.mapCocone s) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.map F s)
• CategoryTheory.Limits.isColimitOfPreserves 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cocone K} (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit K F] : CategoryTheory.Limits.IsColimit (F.mapCocone c)
• CategoryTheory.Limits.isColimitOfReflects 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} (F : CategoryTheory.Functor C D) {c : CategoryTheory.Limits.Cocone K} (t : CategoryTheory.Limits.IsColimit (F.mapCocone c)) [CategoryTheory.Limits.ReflectsColimit K F] : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.preservesColimit_of_preserves_colimit_cocone 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cocone K} (h : CategoryTheory.Limits.IsColimit t) (hF : CategoryTheory.Limits.IsColimit (F.mapCocone t)) : CategoryTheory.Limits.PreservesColimit K F
• CategoryTheory.Limits.PreservesColimit.mk 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} (preserves : ∀ {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c), Nonempty (CategoryTheory.Limits.IsColimit (F.mapCocone c))) : CategoryTheory.Limits.PreservesColimit K F
• CategoryTheory.Limits.PreservesColimit.preserves 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {J : Type w} {inst✝² : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.PreservesColimit K F] {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) : Nonempty (CategoryTheory.Limits.IsColimit (F.mapCocone c))
• CategoryTheory.Limits.ReflectsColimit.mk 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} (reflects : ∀ {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit (F.mapCocone c)), Nonempty (CategoryTheory.Limits.IsColimit c)) : CategoryTheory.Limits.ReflectsColimit K F
• CategoryTheory.Limits.ReflectsColimit.reflects 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {J : Type w} {inst✝² : CategoryTheory.Category.{w', w} J} {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [self : CategoryTheory.Limits.ReflectsColimit K F] {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit (F.mapCocone c)) : Nonempty (CategoryTheory.Limits.IsColimit c)
• CategoryTheory.Limits.preservesColimit_iff_isColimit_mapCocone 📋 Mathlib.CategoryTheory.Limits.Preserves.Basic
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} {t : CategoryTheory.Limits.Cocone K} (h : CategoryTheory.Limits.IsColimit t) : CategoryTheory.Limits.PreservesColimit K F ↔ Nonempty (CategoryTheory.Limits.IsColimit (F.mapCocone t))
• CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (X : C) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.asEmptyCocone X)) ≃ CategoryTheory.Limits.IsInitial (G.obj X)
• CategoryTheory.Limits.isColimitMapCoconeBinaryCofanEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {P X Y : C} (f : X ⟶ P) (g : Y ⟶ P) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.BinaryCofan.mk f g)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk (G.map f) (G.map g))
• CategoryTheory.Limits.isColimitMapCoconeCofanMkEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} (f : J → C) {P : C} (g : (j : J) → f j ⟶ P) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.Cofan.mk P g)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk (G.obj P) fun j => G.map (g j))
• CategoryTheory.preserves_desc_mapCocone 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] (c₁ c₂ : CategoryTheory.Limits.Cocone F) (t : CategoryTheory.Limits.IsColimit c₁) : (CategoryTheory.Limits.isColimitOfPreserves G t).desc (G.mapCocone c₂) = G.map (t.desc c₂)
• CategoryTheory.preservesColimitIso_inv_comp_desc 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F) : CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv (G.map (CategoryTheory.Limits.colimit.desc F t)) = CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone t)
• CategoryTheory.preservesColimitIso_inv_comp_desc_assoc 📋 Mathlib.CategoryTheory.Limits.Preserves.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {J : Type w} [CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor J C) [CategoryTheory.Limits.PreservesColimit F G] [CategoryTheory.Limits.HasColimit F] (t : CategoryTheory.Limits.Cocone F) {Z : D} (h : G.obj t.pt ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.desc F t)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.desc (F.comp G) (G.mapCocone t)) h
• CategoryTheory.Limits.evaluationJointlyReflectsColimits 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (c : CategoryTheory.Limits.Cocone F) (t : (k : K) → CategoryTheory.Limits.IsColimit (((CategoryTheory.evaluation K C).obj k).mapCocone c)) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.evaluateCombinedCocones 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (c : (k : K) → CategoryTheory.Limits.ColimitCocone (F.flip.obj k)) (k : K) : ((CategoryTheory.evaluation K C).obj k).mapCocone (CategoryTheory.Limits.combineCocones F c) ≅ (c k).cocone
• CategoryTheory.LiftableCocone.mk 📋 Mathlib.CategoryTheory.Limits.Creates
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)} (liftedCocone : CategoryTheory.Limits.Cocone K) (validLift : F.mapCocone liftedCocone ≅ c) : CategoryTheory.LiftableCocone K F c
• CategoryTheory.LiftableCocone.validLift 📋 Mathlib.CategoryTheory.Limits.Creates
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} {c : CategoryTheory.Limits.Cocone (K.comp F)} (self : CategoryTheory.LiftableCocone K F c) : F.mapCocone self.liftedCocone ≅ c
• CategoryTheory.liftedColimitMapsToOriginal 📋 Mathlib.CategoryTheory.Limits.Creates
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [CategoryTheory.CreatesColimit K F] {c : CategoryTheory.Limits.Cocone (K.comp F)} (t : CategoryTheory.Limits.IsColimit c) : F.mapCocone (CategoryTheory.liftColimit t) ≅ c
• CategoryTheory.createsColimitOfFullyFaithfulOfLift 📋 Mathlib.CategoryTheory.Limits.Creates
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [F.Full] [F.Faithful] [CategoryTheory.Limits.HasColimit (K.comp F)] (c : CategoryTheory.Limits.Cocone K) (i : F.mapCocone c ≅ CategoryTheory.Limits.colimit.cocone (K.comp F)) : CategoryTheory.CreatesColimit K F
• CategoryTheory.createsColimitOfFullyFaithfulOfLift' 📋 Mathlib.CategoryTheory.Limits.Creates
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {J : Type w} [CategoryTheory.Category.{w', w} J] {K : CategoryTheory.Functor J C} {F : CategoryTheory.Functor C D} [F.Full] [F.Faithful] {l : CategoryTheory.Limits.Cocone (K.comp F)} (hl : CategoryTheory.Limits.IsColimit l) (c : CategoryTheory.Limits.Cocone K) (i : F.mapCocone c ≅ l) : CategoryTheory.CreatesColimit K F
• CategoryTheory.Limits.PushoutCocone.isColimitMapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {W X Y : C} {f : W ⟶ X} {g : W ⟶ Y} (c : CategoryTheory.Limits.PushoutCocone f g) (G : CategoryTheory.Functor C D) : CategoryTheory.Limits.IsColimit (G.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map G)
• CategoryTheory.Limits.isColimitMapCoconePushoutCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Pullbacks
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {W X Y Z : C} {h : X ⟶ Z} {k : Y ⟶ Z} {f : W ⟶ X} {g : W ⟶ Y} (comm : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.PushoutCocone.mk h k comm)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk (G.map h) (G.map k) ⋯)
• AddCommGrpCat.Colimits.Quot.desc_quotQuotUliftAddEquiv 📋 Mathlib.Algebra.Category.Grp.Colimits
  {J : Type u} [CategoryTheory.Category.{v, u} J] (F : CategoryTheory.Functor J AddCommGrpCat) [DecidableEq J] (c : CategoryTheory.Limits.Cocone F) : (AddCommGrpCat.Colimits.Quot.desc (F.comp AddCommGrpCat.uliftFunctor) (AddCommGrpCat.uliftFunctor.mapCocone c)).comp (AddCommGrpCat.Colimits.quotQuotUliftAddEquiv F).toAddMonoidHom = AddEquiv.ulift.symm.toAddMonoidHom.comp (AddCommGrpCat.Colimits.Quot.desc F c)
• CategoryTheory.Comma.fstSndJointlyReflectColimit 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {F : CategoryTheory.Functor J (CategoryTheory.Comma L R)} {c : CategoryTheory.Limits.Cocone F} [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] (h₁ : CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.fst L R).mapCocone c)) (h₂ : CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.snd L R).mapCocone c)) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Comma.coconeOfPreserves_pt_hom 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) : (CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).pt.hom = (CategoryTheory.Limits.isColimitOfPreserves L t₁).desc (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂)
• CategoryTheory.Comma.colimitAuxiliaryCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (X : J) : (CategoryTheory.Comma.colimitAuxiliaryCocone F c₂).ι.app X = CategoryTheory.CategoryStruct.comp (F.obj X).hom (R.map (c₂.ι.app X))
• CategoryTheory.Comma.coconeOfPreserves_ι_app_left 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).left = c₁.ι.app j
• CategoryTheory.Comma.coconeOfPreserves_ι_app_right 📋 Mathlib.CategoryTheory.Limits.Comma
  {J : Type w} [CategoryTheory.Category.{w', w} J] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [CategoryTheory.Category.{v₂, u₂} B] {T : Type u₃} [CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} (F : CategoryTheory.Functor J (CategoryTheory.Comma L R)) [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] {c₁ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.fst L R))} (t₁ : CategoryTheory.Limits.IsColimit c₁) (c₂ : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.Comma.snd L R))) (j : J) : ((CategoryTheory.Comma.coconeOfPreserves F t₁ c₂).ι.app j).right = c₂.ι.app j
• CategoryTheory.Limits.Cocone.mapCoconeToOver 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : (CategoryTheory.Over.forget c.pt).mapCocone c.toOver ≅ c
• CategoryTheory.Limits.Cocone.toCostructuredArrowCocone 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : CategoryTheory.Limits.Cocone ((F.mapCocone c).toCostructuredArrow.comp ((CategoryTheory.CostructuredArrow.map f).comp (CategoryTheory.CostructuredArrow.pre K F X)))
• CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_pt 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) : (c.toCostructuredArrowCocone F f).pt = CategoryTheory.CostructuredArrow.mk f
• CategoryTheory.Limits.Cocone.mapCoconeToOver_hom_hom 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : c.mapCoconeToOver.hom.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.Cocone.mapCoconeToOver_inv_hom 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) : c.mapCoconeToOver.inv.hom = CategoryTheory.CategoryStruct.id c.pt
• CategoryTheory.Limits.Cocone.toCostructuredArrowCocone_ι_app 📋 Mathlib.CategoryTheory.Limits.ConeCategory
  {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄} [CategoryTheory.Category.{v₄, u₄} D] {K : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone K) (F : CategoryTheory.Functor C D) {X : D} (f : F.obj c.pt ⟶ X) (j : J) : (c.toCostructuredArrowCocone F f).ι.app j = CategoryTheory.CostructuredArrow.homMk (c.ι.app j) ⋯
• CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) {X Y Z : C} {f g : X ⟶ Y} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g h) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.Cofork.ofπ h w)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofork.ofπ (G.map h) ⋯)
• CategoryTheory.Limits.CokernelCofork.isColimitMapCoconeEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : C} {f : X ⟶ Y} (c : CategoryTheory.Limits.CokernelCofork f) (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] : CategoryTheory.Limits.IsColimit (G.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map G)
• CategoryTheory.Limits.isColimitMapCoconeCoforkEquiv' 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D) [G.PreservesZeroMorphisms] {X Y Z : C} {f : X ⟶ Y} {h : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f h = 0) : CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.CokernelCofork.ofπ h w)) ≃ CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (G.map h) ⋯)
• CategoryTheory.Abelian.isColimitMapCoconeOfCokernelCoforkOfπ 📋 Mathlib.CategoryTheory.Abelian.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{v_1, u_1} D] [CategoryTheory.Limits.HasZeroMorphisms D] {X Y : D} (p : X ⟶ Y) [CategoryTheory.Limits.HasKernel p] (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [CategoryTheory.Epi (F.map p)] [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair p 0) F] : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.CokernelCofork.ofπ p ⋯))
• CategoryTheory.ShortComplex.isColimitπ₁MapCoconeColimitCocone 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₁.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))
• CategoryTheory.ShortComplex.isColimitπ₂MapCoconeColimitCocone 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₂.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))
• CategoryTheory.ShortComplex.isColimitπ₃MapCoconeColimitCocone 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)) [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₁)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₂)] [CategoryTheory.Limits.HasColimit (F.comp CategoryTheory.ShortComplex.π₃)] : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₃.mapCocone (CategoryTheory.ShortComplex.colimitCocone F))
• CategoryTheory.ShortComplex.isColimitOfIsColimitπ 📋 Mathlib.Algebra.Homology.ShortComplex.Limits
  {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.Category.{v_2, u_2} C] [CategoryTheory.Limits.HasZeroMorphisms C] {F : CategoryTheory.Functor J (CategoryTheory.ShortComplex C)} (c : CategoryTheory.Limits.Cocone F) (h₁ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₁.mapCocone c)) (h₂ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₂.mapCocone c)) (h₃ : CategoryTheory.Limits.IsColimit (CategoryTheory.ShortComplex.π₃.mapCocone c)) : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Functor.isColimitMapCoconeBinaryCofanOfPreservesCokernels 📋 Mathlib.CategoryTheory.Preadditive.LeftExact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D) [F.PreservesZeroMorphisms] {X Y Z : C} (ι₁ : X ⟶ Z) (ι₂ : Y ⟶ Z) [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair ι₂ 0) F] (i : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂)) : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂))
• CategoryTheory.Monad.ForgetCreatesColimits.lambda 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] : (T.mapCocone c).pt ⟶ c.pt
• CategoryTheory.Monad.ForgetCreatesColimits.coconePoint_a 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] : (CategoryTheory.Monad.ForgetCreatesColimits.coconePoint c t).a = CategoryTheory.Monad.ForgetCreatesColimits.lambda c t
• CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit_desc_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [CategoryTheory.Category.{v, u} J] {T : CategoryTheory.Comonad C} (D : CategoryTheory.Functor J T.Coalgebra) (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone D) : ((CategoryTheory.Comonad.ForgetCreatesColimits'.liftedCoconeIsColimit D c t).desc s).f = t.desc (T.forget.mapCocone s)
• CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit_desc_f 📋 Mathlib.CategoryTheory.Monad.Limits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u} [CategoryTheory.Category.{v, u} J] {D : CategoryTheory.Functor J T.Algebra} (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) (t : CategoryTheory.Limits.IsColimit c) [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] [CategoryTheory.Limits.PreservesColimit ((D.comp T.forget).comp T.toFunctor) T.toFunctor] (s : CategoryTheory.Limits.Cocone D) : ((CategoryTheory.Monad.ForgetCreatesColimits.liftedCoconeIsColimit c t).desc s).f = t.desc (T.forget.mapCocone s)
• HomologicalComplex.isColimitOfEval 📋 Mathlib.Algebra.Homology.HomologicalComplexLimits
  {C : Type u_1} {ι : Type u_2} {J : Type u_3} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι} [CategoryTheory.Limits.HasZeroMorphisms C] (F : CategoryTheory.Functor J (HomologicalComplex C c)) (s : CategoryTheory.Limits.Cocone F) (hs : (i : ι) → CategoryTheory.Limits.IsColimit ((HomologicalComplex.eval C c i).mapCocone s)) : CategoryTheory.Limits.IsColimit s
• PresheafOfModules.evaluationJointlyReflectsColimits 📋 Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂} [CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R)) (c : CategoryTheory.Limits.Cocone F) (hc : (X : Cᵒᵖ) → CategoryTheory.Limits.IsColimit ((PresheafOfModules.evaluation R X).mapCocone c)) : CategoryTheory.Limits.IsColimit c
• TopCat.nonempty_isColimit_iff_eq_coinduced 📋 Mathlib.Topology.Category.TopCat.Limits.Basic
  {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J TopCat} (c : CategoryTheory.Limits.Cocone F) (hc : CategoryTheory.Limits.IsColimit ((CategoryTheory.forget TopCat).mapCocone c)) : Nonempty (CategoryTheory.Limits.IsColimit c) ↔ c.pt.str = ⨆ j, TopologicalSpace.coinduced (⇑(CategoryTheory.ConcreteCategory.hom (c.ι.app j))) (F.obj j).str
• CategoryTheory.IsVanKampenColimit.mapCocone_iff 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} [G.IsEquivalence] : CategoryTheory.IsVanKampenColimit (G.mapCocone c) ↔ CategoryTheory.IsVanKampenColimit c
• CategoryTheory.IsUniversalColimit.of_mapCocone 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan G] [CategoryTheory.Limits.ReflectsColimitsOfShape J G] (hc : CategoryTheory.IsUniversalColimit (G.mapCocone c)) : CategoryTheory.IsUniversalColimit c
• CategoryTheory.isVanKampenColimit_of_evaluation 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasPullbacks D] [CategoryTheory.Limits.HasColimitsOfShape J D] (F : CategoryTheory.Functor J (CategoryTheory.Functor C D)) (c : CategoryTheory.Limits.Cocone F) (hc : ∀ (x : C), CategoryTheory.IsVanKampenColimit (((CategoryTheory.evaluation C D).obj x).mapCocone c)) : CategoryTheory.IsVanKampenColimit c
• CategoryTheory.IsVanKampenColimit.of_mapCocone 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D) {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} [∀ (i j : J) (X : C) (f : X ⟶ F.obj j) (g : i ⟶ j), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (F.map g)) G] [∀ (i : J) (X : C) (f : X ⟶ c.pt), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) G] [CategoryTheory.Limits.ReflectsLimitsOfShape CategoryTheory.Limits.WalkingCospan G] [CategoryTheory.Limits.PreservesColimitsOfShape J G] [CategoryTheory.Limits.ReflectsColimitsOfShape J G] (H : CategoryTheory.IsVanKampenColimit (G.mapCocone c)) : CategoryTheory.IsVanKampenColimit c
• CategoryTheory.IsUniversalColimit.map_reflective 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {Gl : CategoryTheory.Functor C D} {Gr : CategoryTheory.Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] {F : CategoryTheory.Functor J D} {c : CategoryTheory.Limits.Cocone (F.comp Gr)} (H : CategoryTheory.IsUniversalColimit c) [∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)] [∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl] : CategoryTheory.IsUniversalColimit (Gl.mapCocone c)
• CategoryTheory.IsVanKampenColimit.map_reflective 📋 Mathlib.CategoryTheory.Limits.VanKampen
  {J : Type v'} [CategoryTheory.Category.{u', v'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Limits.HasColimitsOfShape J C] {Gl : CategoryTheory.Functor C D} {Gr : CategoryTheory.Functor D C} (adj : Gl ⊣ Gr) [Gr.Full] [Gr.Faithful] {F : CategoryTheory.Functor J D} {c : CategoryTheory.Limits.Cocone (F.comp Gr)} (H : CategoryTheory.IsVanKampenColimit c) [∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.HasPullback (Gr.map f) (adj.unit.app c.pt)] [∀ (X : D) (f : X ⟶ Gl.obj c.pt), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (Gr.map f) (adj.unit.app c.pt)) Gl] [∀ (X : C) (i : J) (f : X ⟶ c.pt), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f (c.ι.app i)) Gl] : CategoryTheory.IsVanKampenColimit (Gl.mapCocone c)
• CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B) (L : CategoryTheory.Functor A C) (E : L.LeftExtension F) (c : C) : ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj E).coconeAt c ≅ G.mapCocone (E.coconeAt c)
• CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_hom_hom 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B) (L : CategoryTheory.Functor A C) (E : L.LeftExtension F) (c : C) : (CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso G F L E c).hom.hom = CategoryTheory.CategoryStruct.id (G.obj (E.right.obj c))
• CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso_inv_hom 📋 Mathlib.CategoryTheory.Functor.KanExtension.Preserves
  {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [CategoryTheory.Category.{v_1, u_1} A] [CategoryTheory.Category.{v_2, u_2} B] [CategoryTheory.Category.{v_3, u_3} C] [CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B) (L : CategoryTheory.Functor A C) (E : L.LeftExtension F) (c : C) : (CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso G F L E c).inv.hom = CategoryTheory.CategoryStruct.id (G.obj (E.right.obj c))
• SheafOfModules.Presentation.map_relations_I 📋 Mathlib.Algebra.Category.ModuleCat.Sheaf.Quasicoherent
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C} {R : CategoryTheory.Sheaf J RingCat} [CategoryTheory.HasSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {C' : Type u₂} [CategoryTheory.Category.{v₂, u₂} C'] {J' : CategoryTheory.GrothendieckTopology C'} {S : CategoryTheory.Sheaf J' RingCat} [CategoryTheory.HasSheafify J' AddCommGrpCat] [J'.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} (P : M.Presentation) (F : CategoryTheory.Functor (SheafOfModules R) (SheafOfModules S)) [CategoryTheory.Limits.PreservesColimitsOfSize.{u, u, max u u₁, max u u₂, max (max (u + 1) u₁) v₁, max (max (u + 1) u₂) v₂} F] (η : SheafOfModules.unit S ≅ F.obj (SheafOfModules.unit R)) : (P.map F η).relations.I = P.relations.I
• AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
  {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J TopCat] [∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F) (U : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ) : s.pt.presheaf.obj U ⟶ ((TopCat.Presheaf.pushforward C (CategoryTheory.Limits.colimit.desc (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)) ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).obj (CategoryTheory.Limits.limit (AlgebraicGeometry.PresheafedSpace.pushforwardDiagramToColimit F).leftOp)).obj U
• AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.desc_c_naturality 📋 Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
  {J : Type u'} [CategoryTheory.Category.{v', u'} J] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasColimitsOfShape J TopCat] [∀ (X : TopCat), CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ (TopCat.Presheaf C X)] [CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C] (F : CategoryTheory.Functor J (AlgebraicGeometry.PresheafedSpace C)) (s : CategoryTheory.Limits.Cocone F) {U V : (TopologicalSpace.Opens ↑↑s.pt)ᵒᵖ} (i : U ⟶ V) : CategoryTheory.CategoryStruct.comp (s.pt.presheaf.map i) (AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s V) = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.ColimitCoconeIsColimit.descCApp F s U) (((TopCat.Presheaf.pushforward C (CategoryTheory.Limits.colimit.desc (F.comp (AlgebraicGeometry.PresheafedSpace.forget C)) ((AlgebraicGeometry.PresheafedSpace.forget C).mapCocone s))).obj (AlgebraicGeometry.PresheafedSpace.colimitCocone F).pt.presheaf).map i)
• AlgebraicGeometry.Scheme.IsLocallyDirected.isColimitForgetToLocallyRingedSpace 📋 Mathlib.AlgebraicGeometry.Gluing
  {J : Type w} [CategoryTheory.Category.{v, w} J] (F : CategoryTheory.Functor J AlgebraicGeometry.Scheme) [∀ {i j : J} (f : i ⟶ j), AlgebraicGeometry.IsOpenImmersion (F.map f)] [(F.comp AlgebraicGeometry.Scheme.forget).IsLocallyDirected] [Quiver.IsThin J] [Small.{u, w} J] : CategoryTheory.Limits.IsColimit (AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace.mapCocone (AlgebraicGeometry.Scheme.IsLocallyDirected.cocone F))
• AlgebraicGeometry.nonempty_isColimit_Γ_mapCocone 📋 Mathlib.AlgebraicGeometry.AffineTransitionLimit
  {I : Type u} [CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I] [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), CompactSpace ↥(D.obj i)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)] : Nonempty (CategoryTheory.Limits.IsColimit (AlgebraicGeometry.Scheme.Γ.mapCocone c.op))
• CategoryTheory.IsGrothendieckAbelian.isColimitMapCoconeOfSubobjectMkEqISup 📋 Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Subobject
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C] {X : C} {J : Type w} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (CategoryTheory.MonoOver X)) [CategoryTheory.IsFiltered J] (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.MonoOver.forget X))) [CategoryTheory.Mono c.pt.hom] (h : CategoryTheory.Subobject.mk c.pt.hom = ⨆ j, CategoryTheory.Subobject.mk (F.obj j).obj.hom) : CategoryTheory.Limits.IsColimit ((CategoryTheory.Over.forget X).mapCocone c)
• CategoryTheory.Limits.Multicofork.isColimitMapEquiv 📋 Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.Limits.MultispanShape} {d : CategoryTheory.Limits.MultispanIndex J C} (c : CategoryTheory.Limits.Multicofork d) (F : CategoryTheory.Functor C D) : CategoryTheory.Limits.IsColimit (F.mapCocone c) ≃ CategoryTheory.Limits.IsColimit (c.map F)
• SSet.relativeCellComplexOfMono_isColimit 📋 Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
  {X Y : SSet} (i : X ⟶ Y) [CategoryTheory.Mono i] : (SSet.relativeCellComplexOfMono i).isColimit = (CategoryTheory.Limits.isColimitOfPreserves SSet.Subcomplex.toSSetFunctor (CategoryTheory.Limits.CompleteLattice.colimitCocone ⋯.functor).isColimit).ofIsoColimit (CategoryTheory.Limits.Cocone.ext (SSet.Subcomplex.eqToIso ⋯ ≪≫ SSet.Subcomplex.topIso Y) ⋯)
• CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone 📋 Mathlib.CategoryTheory.Presentable.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : Type u'} [CategoryTheory.Category.{v', u'} K] {F : CategoryTheory.Functor K (CategoryTheory.Functor C (Type w'))} (c : CategoryTheory.Limits.Cone F) (hc : (Y : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation C (Type w')).obj Y).mapCone c)) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hK : HasCardinalLT (CategoryTheory.Arrow K) κ) {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ] {X : CategoryTheory.Functor J C} (cX : CategoryTheory.Limits.Cocone X) (hF : (k : K) → CategoryTheory.Limits.IsColimit ((F.obj k).mapCocone cX)) : CategoryTheory.Limits.IsColimit (c.pt.mapCocone cX)
• CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.surjective 📋 Mathlib.CategoryTheory.Presentable.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : Type u'} [CategoryTheory.Category.{v', u'} K] {F : CategoryTheory.Functor K (CategoryTheory.Functor C (Type w'))} (c : CategoryTheory.Limits.Cone F) (hc : (Y : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation C (Type w')).obj Y).mapCone c)) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hK : HasCardinalLT (CategoryTheory.Arrow K) κ) {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ] {X : CategoryTheory.Functor J C} (cX : CategoryTheory.Limits.Cocone X) (hF : (k : K) → CategoryTheory.Limits.IsColimit ((F.obj k).mapCocone cX)) (x : c.pt.obj cX.pt) : ∃ j x', x = (CategoryTheory.ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j)) x'
• CategoryTheory.Functor.Accessible.Limits.isColimitMapCocone.injective 📋 Mathlib.CategoryTheory.Presentable.Limits
  {C : Type u} [CategoryTheory.Category.{v, u} C] {K : Type u'} [CategoryTheory.Category.{v', u'} K] {F : CategoryTheory.Functor K (CategoryTheory.Functor C (Type w'))} (c : CategoryTheory.Limits.Cone F) (hc : (Y : C) → CategoryTheory.Limits.IsLimit (((CategoryTheory.evaluation C (Type w')).obj Y).mapCone c)) (κ : Cardinal.{w}) [Fact κ.IsRegular] (hK : HasCardinalLT (CategoryTheory.Arrow K) κ) {J : Type w} [CategoryTheory.SmallCategory J] [CategoryTheory.IsCardinalFiltered J κ] {X : CategoryTheory.Functor J C} (cX : CategoryTheory.Limits.Cocone X) (hF : (k : K) → CategoryTheory.Limits.IsColimit ((F.obj k).mapCocone cX)) (j : J) (x₁ x₂ : c.pt.obj (X.obj j)) (h : (CategoryTheory.ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (CategoryTheory.ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂) : ∃ j' α, (CategoryTheory.ConcreteCategory.hom (c.pt.map (X.map α))) x₁ = (CategoryTheory.ConcreteCategory.hom (c.pt.map (X.map α))) x₂
• CategoryTheory.Limits.evaluationCoconePointwiseProductIso 📋 Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4} [(i : α) → CategoryTheory.Category.{u_5, u_4} (I i)] [CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C] (F : (i : α) → CategoryTheory.Functor (I i) (CategoryTheory.Functor D C)) (X : D) (c : (i : α) → CategoryTheory.Limits.Cocone (F i)) : ((CategoryTheory.evaluation D C).obj X).mapCocone (CategoryTheory.Limits.coconePointwiseProduct c) ≅ (CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Limits.pointwiseProductCompEvaluation F X).hom).obj (CategoryTheory.Limits.coconePointwiseProduct fun i => ((CategoryTheory.evaluation D C).obj X).mapCocone (c i))
• CategoryTheory.JointlyReflectIsomorphisms.jointlyReflectsColimit 📋 Mathlib.CategoryTheory.Functor.ReflectsIso.Limits
  {C : Type u_1} [CategoryTheory.Category.{u_5, u_1} C] {I : Type u_2} {D : I → Type u_3} [(i : I) → CategoryTheory.Category.{u_6, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)} (hF : CategoryTheory.JointlyReflectIsomorphisms F) {J : Type u_4} [CategoryTheory.Category.{v_1, u_4} J] {G : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone G} (hc : (i : I) → CategoryTheory.Limits.IsColimit ((F i).mapCocone c)) [CategoryTheory.Limits.HasColimit G] [∀ (i : I), CategoryTheory.Limits.PreservesColimit G (F i)] : CategoryTheory.Limits.IsColimit c
• CategoryTheory.Limits.FormalCoproduct.isColimitEvalMapCoconeCofan 📋 Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
  {C : Type u} [CategoryTheory.Category.{v, u} C] {A : Type u₁} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Limits.HasCoproducts A] (J : Type w) (f : J → CategoryTheory.Limits.FormalCoproduct C) (F : CategoryTheory.Functor C A) : CategoryTheory.Limits.IsColimit (((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F).mapCocone (CategoryTheory.Limits.FormalCoproduct.cofan J f))
• CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit_isColimit 📋 Mathlib.CategoryTheory.Limits.FunctorCategory.BinaryBiproducts
  {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.Limits.HasBinaryBiproducts C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (F G : CategoryTheory.Functor D C) : (CategoryTheory.Limits.pointwiseBinaryBicone.isBilimit F G).isColimit = CategoryTheory.Limits.evaluationJointlyReflectsColimits (CategoryTheory.Limits.pointwiseBinaryBicone F G).toCocone fun d => (CategoryTheory.Limits.IsColimit.equivOfNatIsoOfIso (CategoryTheory.Limits.pairComp F G ((CategoryTheory.evaluation D C).obj d)).symm (CategoryTheory.Limits.BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone (((CategoryTheory.evaluation D C).obj d).mapCocone (CategoryTheory.Limits.pointwiseBinaryBicone F G).toCocone) (CategoryTheory.Limits.Cocone.ext (CategoryTheory.Iso.refl ((CategoryTheory.Limits.Cocone.precompose (CategoryTheory.Limits.pairComp F G ((CategoryTheory.evaluation D C).obj d)).symm.inv).obj (CategoryTheory.Limits.BinaryBiproduct.bicone (F.obj d) (G.obj d)).toCocone).pt) ⋯)) (CategoryTheory.Limits.BinaryBiproduct.isColimit (F.obj d) (G.obj d))
• Profinite.Extend.isColimitCocone 📋 Mathlib.Topology.Category.Profinite.Extend
  {I : Type u} [CategoryTheory.SmallCategory I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor Profiniteᵒᵖ C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] (hc' : CategoryTheory.Limits.IsColimit (G.mapCocone c.op)) : CategoryTheory.Limits.IsColimit (Profinite.Extend.cocone G c.pt)
• LightProfinite.Extend.isColimitCocone 📋 Mathlib.Topology.Category.LightProfinite.Extend
  {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (G : CategoryTheory.Functor LightProfiniteᵒᵖ C) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (hc' : CategoryTheory.Limits.IsColimit (G.mapCocone c.op)) : CategoryTheory.Limits.IsColimit (LightProfinite.Extend.cocone G c.pt)
• LightCondensed.isColimitLocallyConstantPresheafDiagram 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type u) (S : LightProfinite) : CategoryTheory.Limits.IsColimit ((LightCondensed.locallyConstantPresheaf X).mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))
• LightCondensed.lanPresheafNatIso 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : LightCondensed.lanPresheaf F ≅ F
• LightCondensed.lanPresheafIso 📋 Mathlib.Condensed.Discrete.Colimit
  {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (LightCondensed.lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S)
• LightCondensed.isoLocallyConstantOfIsColimit 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : F ≅ LightCondensed.locallyConstantPresheaf (F.obj (FintypeCat.toLightProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))
• Condensed.isColimitLocallyConstantPresheaf 📋 Mathlib.Condensed.Discrete.Colimit
  {I : Type u} [CategoryTheory.Category.{u, u} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Type (u + 1)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] : CategoryTheory.Limits.IsColimit ((Condensed.locallyConstantPresheaf X).mapCocone c.op)
• LightCondensed.isoLocallyConstantOfIsColimit_inv 📋 Mathlib.Condensed.Discrete.Colimit
  (X : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)) [CategoryTheory.Limits.PreservesFiniteProducts X] (hX : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (X.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (LightCondensed.isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X
• LightCondensed.lanPresheafIso_hom 📋 Mathlib.Condensed.Discrete.Colimit
  {S : LightProfinite} {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : (LightCondensed.lanPresheafIso hF).hom = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op S)).comp (FintypeCat.toLightProfinite.op.comp F)) (LightProfinite.Extend.cocone F S)
• Condensed.isColimitLocallyConstantPresheafDiagram 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type (u + 1)) (S : Profinite) : CategoryTheory.Limits.IsColimit ((Condensed.locallyConstantPresheaf X).mapCocone S.asLimitCone.op)
• LightCondensed.lanPresheafNatIso_hom_app 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor LightProfiniteᵒᵖ (Type u)} (hF : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (F.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) (S : LightProfiniteᵒᵖ) : (LightCondensed.lanPresheafNatIso hF).hom.app S = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toLightProfinite.op (Opposite.op (Opposite.unop S))).comp (FintypeCat.toLightProfinite.op.comp F)) (LightProfinite.Extend.cocone F (Opposite.unop S))
• Condensed.lanPresheafNatIso 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : Condensed.lanPresheaf F ≅ F
• Condensed.lanPresheafIso 📋 Mathlib.Condensed.Discrete.Colimit
  {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (Condensed.lanPresheaf F).obj (Opposite.op S) ≅ F.obj (Opposite.op S)
• Condensed.isoLocallyConstantOfIsColimit 📋 Mathlib.Condensed.Discrete.Colimit
  (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts F] (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : F ≅ Condensed.locallyConstantPresheaf (F.obj (FintypeCat.toProfinite.op.obj (Opposite.op (FintypeCat.of PUnit.{u + 1}))))
• LightCondensed.isColimitLocallyConstantPresheaf 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (X : Type u) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] : CategoryTheory.Limits.IsColimit ((LightCondensed.locallyConstantPresheaf X).mapCocone c.op)
• Condensed.isoLocallyConstantOfIsColimit_inv 📋 Mathlib.Condensed.Discrete.Colimit
  (X : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [CategoryTheory.Limits.PreservesFiniteProducts X] (hX : (S : Profinite) → CategoryTheory.Limits.IsColimit (X.mapCocone S.asLimitCone.op)) : (Condensed.isoLocallyConstantOfIsColimit X hX).inv = CompHausLike.LocallyConstant.counitApp X
• Condensed.lanPresheafIso_hom 📋 Mathlib.Condensed.Discrete.Colimit
  {S : Profinite} {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) : (Condensed.lanPresheafIso hF).hom = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op S)).comp (FintypeCat.toProfinite.op.comp F)) (Profinite.Extend.cocone F S)
• Condensed.lanPresheafNatIso_hom_app 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))} (hF : (S : Profinite) → CategoryTheory.Limits.IsColimit (F.mapCocone S.asLimitCone.op)) (S : Profiniteᵒᵖ) : (Condensed.lanPresheafNatIso hF).hom.app S = CategoryTheory.Limits.colimit.desc ((CategoryTheory.CostructuredArrow.proj FintypeCat.toProfinite.op (Opposite.op (Opposite.unop S))).comp (FintypeCat.toProfinite.op.comp F)) (Profinite.Extend.cocone F (Opposite.unop S))
• LightCondensed.isColimitLocallyConstantPresheafDiagram_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type u) (S : LightProfinite) (s : CategoryTheory.Limits.Cocone (S.diagram.rightOp.comp (LightCondensed.locallyConstantPresheaf X))) (n : ℕ) (f : LocallyConstant (↑(S.diagram.obj (Opposite.op n)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheafDiagram X S).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app (Opposite.op n)).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app n)) f
• Condensed.isColimitLocallyConstantPresheaf_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  {I : Type u} [CategoryTheory.Category.{u, u} I] [CategoryTheory.IsCofiltered I] {F : CategoryTheory.Functor I FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toProfinite)) (X : Type (u + 1)) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : I), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toProfinite).op.comp (Condensed.locallyConstantPresheaf X))) (i : I) (f : LocallyConstant (↑(FintypeCat.toProfinite.obj (F.obj i)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheaf c X hc).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (c.π.app i).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) f
• LightCondensed.isColimitLocallyConstantPresheaf_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  {F : CategoryTheory.Functor ℕᵒᵖ FintypeCat} (c : CategoryTheory.Limits.Cone (F.comp FintypeCat.toLightProfinite)) (X : Type u) (hc : CategoryTheory.Limits.IsLimit c) [∀ (i : ℕᵒᵖ), CategoryTheory.Epi (c.π.app i)] (s : CategoryTheory.Limits.Cocone ((F.comp FintypeCat.toLightProfinite).op.comp (LightCondensed.locallyConstantPresheaf X))) (n : ℕᵒᵖ) (f : LocallyConstant (↑(FintypeCat.toLightProfinite.obj (F.obj n)).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((LightCondensed.isColimitLocallyConstantPresheaf c X hc).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (c.π.app n).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op n))) f
• Condensed.isColimitLocallyConstantPresheafDiagram_desc_apply 📋 Mathlib.Condensed.Discrete.Colimit
  (X : Type (u + 1)) (S : Profinite) (s : CategoryTheory.Limits.Cocone (S.diagram.op.comp (Condensed.locallyConstantPresheaf X))) (i : DiscreteQuotient ↑S.toTop) (f : LocallyConstant (↑(S.diagram.obj i).toTop) X) : (CategoryTheory.ConcreteCategory.hom ((Condensed.isColimitLocallyConstantPresheafDiagram X S).desc s)) (LocallyConstant.comap (TopCat.Hom.hom (S.asLimitCone.π.app i).hom) f) = (CategoryTheory.ConcreteCategory.hom (s.ι.app (Opposite.op i))) f
• LightCondSet.mem_locallyConstant_essImage_of_isColimit_mapCocone 📋 Mathlib.Condensed.Discrete.Characterization
  (X : LightCondSet) (h : (S : LightProfinite) → CategoryTheory.Limits.IsColimit (X.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone))) : LightCondSet.LocallyConstant.functor.essImage X
• CondensedSet.mem_locallyConstant_essImage_of_isColimit_mapCocone 📋 Mathlib.Condensed.Discrete.Characterization
  (X : CondensedSet) (h : (S : Profinite) → CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.obj).mapCocone S.asLimitCone.op)) : CondensedSet.LocallyConstant.functor.essImage X
• LightCondSet.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (X : LightCondSet) : [LightCondensed.IsDiscrete X, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X), (LightCondensed.discrete (Type u)).essImage X, LightCondSet.LocallyConstant.functor.essImage X, CategoryTheory.IsIso (LightCondSet.LocallyConstant.adjunction.counit.app X), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (X.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
• LightCondMod.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (R : Type u) [Ring R] (M : LightCondMod R) : [LightCondensed.IsDiscrete M, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (LightCondensed.discrete (ModuleCat R)).essImage M, (LightCondMod.LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (M.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
• CondensedSet.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (X : CondensedSet) : [Condensed.IsDiscrete X, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (Type (u + 1))).counit.app X), (Condensed.discrete (Type (u + 1))).essImage X, CondensedSet.LocallyConstant.functor.essImage X, CategoryTheory.IsIso (CondensedSet.LocallyConstant.adjunction.counit.app X), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.obj).mapCocone S.asLimitCone.op))].TFAE
• CondensedMod.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (R : Type (u + 1)) [Ring R] (M : CondensedMod R) : [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (Condensed.discrete (ModuleCat R)).essImage M, (CondensedMod.LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.obj).mapCocone S.asLimitCone.op))].TFAE

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
would find all lemmas which mention the constants Real.sin and tsum, have "two" as a substring of the lemma name, include a product and a power somewhere in the type, and have a hypothesis of the form _ < _ (if there were any such lemmas). Metavariables (?a) are assigned independently in each filter.

The #lucky button will directly send you to the documentation of the first hit.

Source code

You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is provided by the Lean FRO. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision ce5dd8c