Limits and colimits in comma categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We build limits in the comma category comma L R provided that the two source categories have
limits and R preserves them.
This is used to construct limits in the arrow category, structured arrow category and under
category, and show that the appropriate forgetful functors create limits.
The duals of all the above are also given.
@[simp]
theorem
category_theory.comma.limit_auxiliary_cone_X
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R)) :
(category_theory.comma.limit_auxiliary_cone F c₁).X = L.obj c₁.X
def
category_theory.comma.limit_auxiliary_cone
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R)) :
category_theory.limits.cone ((F ⋙ category_theory.comma.snd L R) ⋙ R)
(Implementation). An auxiliary cone which is useful in order to construct limits in the comma category.
Equations
@[simp]
theorem
category_theory.comma.limit_auxiliary_cone_π_app
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R))
(X : J) :
def
category_theory.comma.cone_of_preserves
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R]
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R))
{c₂ : category_theory.limits.cone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_limit c₂) :
If R preserves the appropriate limit, then given a cone for F ⋙ fst L R : J ⥤ L and a
limit cone for F ⋙ snd L R : J ⥤ R we can build a cone for F which will turn out to be a limit
cone.
Equations
@[simp]
theorem
category_theory.comma.cone_of_preserves_X_hom
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R]
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R))
{c₂ : category_theory.limits.cone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_limit c₂) :
@[simp]
theorem
category_theory.comma.cone_of_preserves_π_app_left
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R]
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R))
{c₂ : category_theory.limits.cone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_limit c₂)
(j : J) :
@[simp]
theorem
category_theory.comma.cone_of_preserves_X_left
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R]
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R))
{c₂ : category_theory.limits.cone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_limit c₂) :
(category_theory.comma.cone_of_preserves F c₁ t₂).X.left = c₁.X
@[simp]
theorem
category_theory.comma.cone_of_preserves_π_app_right
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R]
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R))
{c₂ : category_theory.limits.cone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_limit c₂)
(j : J) :
@[simp]
theorem
category_theory.comma.cone_of_preserves_X_right
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R]
(c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R))
{c₂ : category_theory.limits.cone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_limit c₂) :
(category_theory.comma.cone_of_preserves F c₁ t₂).X.right = c₂.X
def
category_theory.comma.cone_of_preserves_is_limit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R]
{c₁ : category_theory.limits.cone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_limit c₁)
{c₂ : category_theory.limits.cone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_limit c₂) :
Provided that R preserves the appropriate limit, then the cone in cone_of_preserves is a
limit.
Equations
- category_theory.comma.cone_of_preserves_is_limit F t₁ t₂ = {lift := λ (s : category_theory.limits.cone F), {left := t₁.lift ((category_theory.comma.fst L R).map_cone s), right := t₂.lift ((category_theory.comma.snd L R).map_cone s), w' := _}, fac' := _, uniq' := _}
@[simp]
theorem
category_theory.comma.colimit_auxiliary_cocone_X
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R)) :
(category_theory.comma.colimit_auxiliary_cocone F c₂).X = R.obj c₂.X
def
category_theory.comma.colimit_auxiliary_cocone
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R)) :
category_theory.limits.cocone ((F ⋙ category_theory.comma.fst L R) ⋙ L)
(Implementation). An auxiliary cocone which is useful in order to construct colimits in the comma category.
Equations
@[simp]
theorem
category_theory.comma.colimit_auxiliary_cocone_ι_app
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R))
(X : J) :
def
category_theory.comma.cocone_of_preserves
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L]
{c₁ : category_theory.limits.cocone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_colimit c₁)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R)) :
If L preserves the appropriate colimit, then given a colimit cocone for F ⋙ fst L R : J ⥤ L and
a cocone for F ⋙ snd L R : J ⥤ R we can build a cocone for F which will turn out to be a
colimit cocone.
Equations
- category_theory.comma.cocone_of_preserves F t₁ c₂ = {X := {left := c₁.X, right := c₂.X, hom := (category_theory.limits.is_colimit_of_preserves L t₁).desc (category_theory.comma.colimit_auxiliary_cocone F c₂)}, ι := {app := λ (j : J), {left := c₁.ι.app j, right := c₂.ι.app j, w' := _}, naturality' := _}}
@[simp]
theorem
category_theory.comma.cocone_of_preserves_X_right
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L]
{c₁ : category_theory.limits.cocone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_colimit c₁)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R)) :
(category_theory.comma.cocone_of_preserves F t₁ c₂).X.right = c₂.X
@[simp]
theorem
category_theory.comma.cocone_of_preserves_ι_app_right
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L]
{c₁ : category_theory.limits.cocone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_colimit c₁)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R))
(j : J) :
@[simp]
theorem
category_theory.comma.cocone_of_preserves_X_hom
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L]
{c₁ : category_theory.limits.cocone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_colimit c₁)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R)) :
@[simp]
theorem
category_theory.comma.cocone_of_preserves_X_left
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L]
{c₁ : category_theory.limits.cocone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_colimit c₁)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R)) :
(category_theory.comma.cocone_of_preserves F t₁ c₂).X.left = c₁.X
@[simp]
theorem
category_theory.comma.cocone_of_preserves_ι_app_left
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L]
{c₁ : category_theory.limits.cocone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_colimit c₁)
(c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R))
(j : J) :
def
category_theory.comma.cocone_of_preserves_is_colimit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L]
{c₁ : category_theory.limits.cocone (F ⋙ category_theory.comma.fst L R)}
(t₁ : category_theory.limits.is_colimit c₁)
{c₂ : category_theory.limits.cocone (F ⋙ category_theory.comma.snd L R)}
(t₂ : category_theory.limits.is_colimit c₂) :
Provided that L preserves the appropriate colimit, then the cocone in cocone_of_preserves is
a colimit.
Equations
- category_theory.comma.cocone_of_preserves_is_colimit F t₁ t₂ = {desc := λ (s : category_theory.limits.cocone F), {left := t₁.desc ((category_theory.comma.fst L R).map_cocone s), right := t₂.desc ((category_theory.comma.snd L R).map_cocone s), w' := _}, fac' := _, uniq' := _}
@[protected, instance]
def
category_theory.comma.has_limit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.has_limit (F ⋙ category_theory.comma.fst L R)]
[category_theory.limits.has_limit (F ⋙ category_theory.comma.snd L R)]
[category_theory.limits.preserves_limit (F ⋙ category_theory.comma.snd L R) R] :
@[protected, instance]
def
category_theory.comma.has_limits_of_shape
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
[category_theory.limits.has_limits_of_shape J A]
[category_theory.limits.has_limits_of_shape J B]
[category_theory.limits.preserves_limits_of_shape J R] :
@[protected, instance]
def
category_theory.comma.has_limits
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
[category_theory.limits.has_limits A]
[category_theory.limits.has_limits B]
[category_theory.limits.preserves_limits R] :
@[protected, instance]
def
category_theory.comma.has_colimit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
(F : J ⥤ category_theory.comma L R)
[category_theory.limits.has_colimit (F ⋙ category_theory.comma.fst L R)]
[category_theory.limits.has_colimit (F ⋙ category_theory.comma.snd L R)]
[category_theory.limits.preserves_colimit (F ⋙ category_theory.comma.fst L R) L] :
@[protected, instance]
def
category_theory.comma.has_colimits_of_shape
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
[category_theory.limits.has_colimits_of_shape J A]
[category_theory.limits.has_colimits_of_shape J B]
[category_theory.limits.preserves_colimits_of_shape J L] :
@[protected, instance]
def
category_theory.comma.has_colimits
{A : Type u₁}
[category_theory.category A]
{B : Type u₂}
[category_theory.category B]
{T : Type u₃}
[category_theory.category T]
{L : A ⥤ T}
{R : B ⥤ T}
[category_theory.limits.has_colimits A]
[category_theory.limits.has_colimits B]
[category_theory.limits.preserves_colimits L] :
@[protected, instance]
def
category_theory.arrow.has_limit
{J : Type w}
[category_theory.category J]
{T : Type u₃}
[category_theory.category T]
(F : J ⥤ category_theory.arrow T)
[i₁ : category_theory.limits.has_limit (F ⋙ category_theory.arrow.left_func)]
[i₂ : category_theory.limits.has_limit (F ⋙ category_theory.arrow.right_func)] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.arrow.has_colimit
{J : Type w}
[category_theory.category J]
{T : Type u₃}
[category_theory.category T]
(F : J ⥤ category_theory.arrow T)
[i₁ : category_theory.limits.has_colimit (F ⋙ category_theory.arrow.left_func)]
[i₂ : category_theory.limits.has_colimit (F ⋙ category_theory.arrow.right_func)] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.structured_arrow.has_limit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
(F : J ⥤ category_theory.structured_arrow X G)
[i₁ : category_theory.limits.has_limit (F ⋙ category_theory.structured_arrow.proj X G)]
[i₂ : category_theory.limits.preserves_limit (F ⋙ category_theory.structured_arrow.proj X G) G] :
@[protected, instance]
def
category_theory.structured_arrow.has_limits_of_shape
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
[category_theory.limits.has_limits_of_shape J A]
[category_theory.limits.preserves_limits_of_shape J G] :
@[protected, instance]
def
category_theory.structured_arrow.has_limits
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
[category_theory.limits.has_limits A]
[category_theory.limits.preserves_limits G] :
@[protected, instance]
noncomputable
def
category_theory.structured_arrow.creates_limit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
(F : J ⥤ category_theory.structured_arrow X G)
[i : category_theory.limits.preserves_limit (F ⋙ category_theory.structured_arrow.proj X G) G] :
Equations
- category_theory.structured_arrow.creates_limit F = category_theory.creates_limit_of_reflects_iso (λ (c : category_theory.limits.cone (F ⋙ category_theory.structured_arrow.proj X G)) (t : category_theory.limits.is_limit c), {to_liftable_cone := {lifted_cone := category_theory.comma.cone_of_preserves F category_theory.limits.punit_cone t, valid_lift := category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.structured_arrow.proj X G).map_cone (category_theory.comma.cone_of_preserves F category_theory.limits.punit_cone t)).X) _}, makes_limit := category_theory.comma.cone_of_preserves_is_limit F category_theory.limits.punit_cone_is_limit t})
@[protected, instance]
noncomputable
def
category_theory.structured_arrow.creates_limits_of_shape
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
[category_theory.limits.preserves_limits_of_shape J G] :
@[protected, instance]
noncomputable
def
category_theory.structured_arrow.creates_limits
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
[category_theory.limits.preserves_limits G] :
Equations
@[protected, instance]
def
category_theory.structured_arrow.mono_right_of_mono
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
[category_theory.limits.has_pullbacks A]
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_cospan G]
{Y Z : category_theory.structured_arrow X G}
(f : Y ⟶ Z)
[category_theory.mono f] :
theorem
category_theory.structured_arrow.mono_iff_mono_right
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{X : T}
{G : A ⥤ T}
[category_theory.limits.has_pullbacks A]
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_cospan G]
{Y Z : category_theory.structured_arrow X G}
(f : Y ⟶ Z) :
@[protected, instance]
def
category_theory.costructured_arrow.has_colimit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
(F : J ⥤ category_theory.costructured_arrow G X)
[i₁ : category_theory.limits.has_colimit (F ⋙ category_theory.costructured_arrow.proj G X)]
[i₂ : category_theory.limits.preserves_colimit (F ⋙ category_theory.costructured_arrow.proj G X) G] :
@[protected, instance]
def
category_theory.costructured_arrow.has_colimits_of_shape
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
[category_theory.limits.has_colimits_of_shape J A]
[category_theory.limits.preserves_colimits_of_shape J G] :
@[protected, instance]
def
category_theory.costructured_arrow.has_colimits
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
[category_theory.limits.has_colimits A]
[category_theory.limits.preserves_colimits G] :
@[protected, instance]
noncomputable
def
category_theory.costructured_arrow.creates_colimit
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
(F : J ⥤ category_theory.costructured_arrow G X)
[i : category_theory.limits.preserves_colimit (F ⋙ category_theory.costructured_arrow.proj G X) G] :
Equations
- category_theory.costructured_arrow.creates_colimit F = category_theory.creates_colimit_of_reflects_iso (λ (c : category_theory.limits.cocone (F ⋙ category_theory.costructured_arrow.proj G X)) (t : category_theory.limits.is_colimit c), {to_liftable_cocone := {lifted_cocone := category_theory.comma.cocone_of_preserves F t category_theory.limits.punit_cocone, valid_lift := category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.costructured_arrow.proj G X).map_cocone (category_theory.comma.cocone_of_preserves F t category_theory.limits.punit_cocone)).X) _}, makes_colimit := category_theory.comma.cocone_of_preserves_is_colimit F t category_theory.limits.punit_cocone_is_colimit})
@[protected, instance]
noncomputable
def
category_theory.costructured_arrow.creates_colimits_of_shape
{J : Type w}
[category_theory.category J]
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
[category_theory.limits.preserves_colimits_of_shape J G] :
@[protected, instance]
noncomputable
def
category_theory.costructured_arrow.creates_colimits
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
[category_theory.limits.preserves_colimits G] :
Equations
@[protected, instance]
def
category_theory.costructured_arrow.epi_left_of_epi
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
[category_theory.limits.has_pushouts A]
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_span G]
{Y Z : category_theory.costructured_arrow G X}
(f : Y ⟶ Z)
[category_theory.epi f] :
theorem
category_theory.costructured_arrow.epi_iff_epi_left
{A : Type u₁}
[category_theory.category A]
{T : Type u₃}
[category_theory.category T]
{G : A ⥤ T}
{X : T}
[category_theory.limits.has_pushouts A]
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_span G]
{Y Z : category_theory.costructured_arrow G X}
(f : Y ⟶ Z) :