Creating (co)limits #
We say that F
creates limits of K
if, given any limit cone c
for K ⋙ F
(i.e. below) we can lift it to a cone "above", and further that F
reflects
limits for K
.
- lifted_cone : category_theory.limits.cone K
- valid_lift : F.map_cone self.lifted_cone ≅ c
Define the lift of a cone: For a cone c
for K ⋙ F
, give a cone for K
which is a lift of c
, i.e. the image of it under F
is (iso) to c
.
We will then use this as part of the definition of creation of limits: every limit cone has a lift.
Note this definition is really only useful when c
is a limit already.
Instances for category_theory.liftable_cone
- category_theory.liftable_cone.has_sizeof_inst
- category_theory.inhabited_liftable_cone
- lifted_cocone : category_theory.limits.cocone K
- valid_lift : F.map_cocone self.lifted_cocone ≅ c
Define the lift of a cocone: For a cocone c
for K ⋙ F
, give a cocone for
K
which is a lift of c
, i.e. the image of it under F
is (iso) to c
.
We will then use this as part of the definition of creation of colimits: every limit cocone has a lift.
Note this definition is really only useful when c
is a colimit already.
Instances for category_theory.liftable_cocone
- category_theory.liftable_cocone.has_sizeof_inst
- category_theory.inhabited_liftable_cocone
- to_reflects_limit : category_theory.limits.reflects_limit K F
- lifts : Π (c : category_theory.limits.cone (K ⋙ F)), category_theory.limits.is_limit c → category_theory.liftable_cone K F c
Definition 3.3.1 of [Riehl].
We say that F
creates limits of K
if, given any limit cone c
for K ⋙ F
(i.e. below) we can lift it to a cone "above", and further that F
reflects
limits for K
.
If F
reflects isomorphisms, it suffices to show only that the lifted cone is
a limit - see creates_limit_of_reflects_iso
.
Instances of this typeclass
- category_theory.creates_limits_of_shape.creates_limit
- category_theory.comp_creates_limit
- CommMon.category_theory.forget₂.category_theory.creates_limit
- AddCommMon.category_theory.forget₂.category_theory.creates_limit
- Group.forget₂.creates_limit
- AddGroup.forget₂.creates_limit
- CommGroup.forget₂.creates_limit
- AddCommGroup.forget₂.creates_limit
- CommSemiRing.category_theory.forget₂.category_theory.creates_limit
- Ring.category_theory.forget₂.category_theory.creates_limit
- CommRing.category_theory.forget₂.category_theory.creates_limit
- category_theory.structured_arrow.creates_limit
- category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limit
- algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_left
- algebraic_geometry.SheafedSpace.is_open_immersion.forget_creates_pullback_of_right
- algebraic_geometry.is_open_immersion.forget_creates_pullback_of_left
- algebraic_geometry.is_open_immersion.forget_creates_pullback_of_right
Instances of other typeclasses for category_theory.creates_limit
- category_theory.creates_limit.has_sizeof_inst
- creates_limit : (Π {K : J ⥤ C}, category_theory.creates_limit K F) . "apply_instance"
F
creates limits of shape J
if F
creates the limit of any diagram
K : J ⥤ C
.
Instances of this typeclass
- category_theory.creates_limits_of_size.creates_limits_of_shape
- category_theory.comp_creates_limits_of_shape
- category_theory.structured_arrow.creates_limits_of_shape
- FinVect.category_theory.forget₂.category_theory.creates_limits_of_shape
- category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits_of_shape
- category_theory.over.forget_creates_connected_limits
Instances of other typeclasses for category_theory.creates_limits_of_shape
- category_theory.creates_limits_of_shape.has_sizeof_inst
- creates_limits_of_shape : (Π {J : Type ?} [_inst_4 : category_theory.category J], category_theory.creates_limits_of_shape J F) . "apply_instance"
F
creates limits if it creates limits of shape J
for any J
.
Instances of this typeclass
- category_theory.adjunction.is_equivalence_creates_limits
- category_theory.id_creates_limits
- category_theory.comp_creates_limits
- category_theory.structured_arrow.creates_limits
- category_theory.under.creates_limits
- category_theory.Sheaf.category_theory.Sheaf_to_presheaf.category_theory.creates_limits
- category_theory.Sheaf_to_presheaf.creates_limits
- Top.sheaf.forget.category_theory.creates_limits
- category_theory.monad.forget_creates_limits
- CompHaus_to_Top.creates_limits
- Profinite.to_CompHaus.creates_limits
- Profinite.to_Top.creates_limits
- Compactum.forget.creates_limits
- CompHaus.forget_creates_limits
- Profinite.forget_creates_limits
Instances of other typeclasses for category_theory.creates_limits_of_size
- category_theory.creates_limits_of_size.has_sizeof_inst
F
creates small limits if it creates limits of shape J
for any small J
.
- to_reflects_colimit : category_theory.limits.reflects_colimit K F
- lifts : Π (c : category_theory.limits.cocone (K ⋙ F)), category_theory.limits.is_colimit c → category_theory.liftable_cocone K F c
Dual of definition 3.3.1 of [Riehl].
We say that F
creates colimits of K
if, given any limit cocone c
for
K ⋙ F
(i.e. below) we can lift it to a cocone "above", and further that F
reflects limits for K
.
If F
reflects isomorphisms, it suffices to show only that the lifted cocone is
a limit - see creates_limit_of_reflects_iso
.
Instances of this typeclass
- category_theory.creates_colimits_of_shape.creates_colimit
- category_theory.comp_creates_colimit
- category_theory.costructured_arrow.creates_colimit
- algebraic_geometry.Scheme.glue_data.algebraic_geometry.Scheme.forget_to_LocallyRingedSpace.category_theory.creates_colimit
- category_theory.monad.forget_creates_colimit
Instances of other typeclasses for category_theory.creates_colimit
- category_theory.creates_colimit.has_sizeof_inst
- creates_colimit : (Π {K : J ⥤ C}, category_theory.creates_colimit K F) . "apply_instance"
F
creates colimits of shape J
if F
creates the colimit of any diagram
K : J ⥤ C
.
Instances of this typeclass
Instances of other typeclasses for category_theory.creates_colimits_of_shape
- category_theory.creates_colimits_of_shape.has_sizeof_inst
- creates_colimits_of_shape : (Π {J : Type ?} [_inst_4 : category_theory.category J], category_theory.creates_colimits_of_shape J F) . "apply_instance"
F
creates colimits if it creates colimits of shape J
for any small J
.
Instances of this typeclass
- category_theory.adjunction.is_equivalence_creates_colimits
- category_theory.id_creates_colimits
- category_theory.comp_creates_colimits
- category_theory.costructured_arrow.creates_colimits
- category_theory.over.creates_colimits
- algebraic_geometry.SheafedSpace.forget_to_PresheafedSpace.category_theory.creates_colimits
- category_theory.monad.forget_creates_colimits
Instances of other typeclasses for category_theory.creates_colimits_of_size
- category_theory.creates_colimits_of_size.has_sizeof_inst
F
creates small colimits if it creates colimits of shape J
for any small J
.
lift_limit t
is the cone for K
given by lifting the limit t
for K ⋙ F
.
Equations
The lifted cone has an image isomorphic to the original cone.
The lifted cone is a limit.
If F
creates the limit of K
and K ⋙ F
has a limit, then K
has a limit.
If F
creates limits of shape J
, and D
has limits of shape J
, then
C
has limits of shape J
.
If F
creates limits, and D
has all limits, then C
has all limits.
lift_colimit t
is the cocone for K
given by lifting the colimit t
for K ⋙ F
.
Equations
The lifted cocone has an image isomorphic to the original cocone.
The lifted cocone is a colimit.
If F
creates the limit of K
and K ⋙ F
has a limit, then K
has a limit.
If F
creates colimits of shape J
, and D
has colimits of shape J
, then
C
has colimits of shape J
.
If F
creates colimits, and D
has all colimits, then C
has all colimits.
Equations
Equations
- category_theory.reflects_limits_of_creates_limits F = {reflects_limits_of_shape := λ {J : Type w'} [_inst_4_1 : category_theory.category J], category_theory.reflects_limits_of_shape_of_creates_limits_of_shape F}
Equations
- category_theory.reflects_colimits_of_creates_colimits F = {reflects_colimits_of_shape := λ {J : Type w'} [_inst_4_1 : category_theory.category J], category_theory.reflects_colimits_of_shape_of_creates_colimits_of_shape F}
- to_liftable_cone : category_theory.liftable_cone K F c
- makes_limit : category_theory.limits.is_limit self.to_liftable_cone.lifted_cone
A helper to show a functor creates limits. In particular, if we can show
that for any limit cone c
for K ⋙ F
, there is a lift of it which is
a limit and F
reflects isomorphisms, then F
creates limits.
Usually, F
creating limits says that any lift of c
is a limit, but
here we only need to show that our particular lift of c
is a limit.
Instances for category_theory.lifts_to_limit
- category_theory.lifts_to_limit.has_sizeof_inst
- category_theory.inhabited_lifts_to_limit
- to_liftable_cocone : category_theory.liftable_cocone K F c
- makes_colimit : category_theory.limits.is_colimit self.to_liftable_cocone.lifted_cocone
A helper to show a functor creates colimits. In particular, if we can show
that for any limit cocone c
for K ⋙ F
, there is a lift of it which is
a limit and F
reflects isomorphisms, then F
creates colimits.
Usually, F
creating colimits says that any lift of c
is a colimit, but
here we only need to show that our particular lift of c
is a colimit.
Instances for category_theory.lifts_to_colimit
- category_theory.lifts_to_colimit.has_sizeof_inst
- category_theory.inhabited_lifts_to_colimit
If F
reflects isomorphisms and we can lift any limit cone to a limit cone,
then F
creates limits.
In particular here we don't need to assume that F reflects limits.
Equations
- category_theory.creates_limit_of_reflects_iso h = {to_reflects_limit := {reflects := λ (d : category_theory.limits.cone K) (hd : category_theory.limits.is_limit (F.map_cone d)), let d' : category_theory.limits.cone K := (h (F.map_cone d) hd).to_liftable_cone.lifted_cone, i : F.map_cone d' ≅ F.map_cone d := (h (F.map_cone d) hd).to_liftable_cone.valid_lift, hd' : category_theory.limits.is_limit d' := (h (F.map_cone d) hd).makes_limit, f : d ⟶ d' := hd'.lift_cone_morphism d in hd'.of_iso_limit (category_theory.as_iso f).symm}, lifts := λ (c : category_theory.limits.cone (K ⋙ F)) (t : category_theory.limits.is_limit c), (h c t).to_liftable_cone}
When F
is fully faithful, to show that F
creates the limit for K
it suffices to exhibit a lift
of a limit cone for K ⋙ F
.
Equations
- category_theory.creates_limit_of_fully_faithful_of_lift' hl c i = category_theory.creates_limit_of_reflects_iso (λ (c' : category_theory.limits.cone (K ⋙ F)) (t : category_theory.limits.is_limit c'), {to_liftable_cone := {lifted_cone := c, valid_lift := i ≪≫ hl.unique_up_to_iso t}, makes_limit := category_theory.limits.is_limit.of_faithful F (hl.of_iso_limit i.symm) (λ (s : category_theory.limits.cone K), F.preimage ((hl.of_iso_limit i.symm).lift (F.map_cone s))) _})
When F
is fully faithful, and has_limit (K ⋙ F)
, to show that F
creates the limit for K
it suffices to exhibit a lift of the chosen limit cone for K ⋙ F
.
When F
is fully faithful, to show that F
creates the limit for K
it suffices to show that a
limit point is in the essential image of F
.
Equations
- category_theory.creates_limit_of_fully_faithful_of_iso' hl X i = category_theory.creates_limit_of_fully_faithful_of_lift' hl {X := X, π := {app := λ (j : J), F.preimage (i.hom ≫ l.π.app j), naturality' := _}} (category_theory.limits.cones.ext i _)
When F
is fully faithful, and has_limit (K ⋙ F)
, to show that F
creates the limit for K
it suffices to show that the chosen limit point is in the essential image of F
.
F
preserves the limit of K
if it creates the limit and K ⋙ F
has the limit.
Equations
- category_theory.preserves_limit_of_creates_limit_and_has_limit K F = {preserves := λ (c : category_theory.limits.cone K) (t : category_theory.limits.is_limit c), (category_theory.limits.limit.is_limit (K ⋙ F)).of_iso_limit ((category_theory.lifted_limit_maps_to_original (category_theory.limits.limit.is_limit (K ⋙ F))).symm ≪≫ (category_theory.limits.cones.functoriality K F).map_iso ((category_theory.lifted_limit_is_limit (category_theory.limits.limit.is_limit (K ⋙ F))).unique_up_to_iso t))}
F
preserves the limit of shape J
if it creates these limits and D
has them.
F
preserves limits if it creates limits and D
has limits.
Equations
If F
reflects isomorphisms and we can lift any colimit cocone to a colimit cocone,
then F
creates colimits.
In particular here we don't need to assume that F reflects colimits.
Equations
- category_theory.creates_colimit_of_reflects_iso h = {to_reflects_colimit := {reflects := λ (d : category_theory.limits.cocone K) (hd : category_theory.limits.is_colimit (F.map_cocone d)), let d' : category_theory.limits.cocone K := (h (F.map_cocone d) hd).to_liftable_cocone.lifted_cocone, i : F.map_cocone d' ≅ F.map_cocone d := (h (F.map_cocone d) hd).to_liftable_cocone.valid_lift, hd' : category_theory.limits.is_colimit d' := (h (F.map_cocone d) hd).makes_colimit, f : d' ⟶ d := hd'.desc_cocone_morphism d in hd'.of_iso_colimit (category_theory.as_iso f)}, lifts := λ (c : category_theory.limits.cocone (K ⋙ F)) (t : category_theory.limits.is_colimit c), (h c t).to_liftable_cocone}
When F
is fully faithful, to show that F
creates the colimit for K
it suffices to exhibit a
lift of a colimit cocone for K ⋙ F
.
Equations
- category_theory.creates_colimit_of_fully_faithful_of_lift' hl c i = category_theory.creates_colimit_of_reflects_iso (λ (c' : category_theory.limits.cocone (K ⋙ F)) (t : category_theory.limits.is_colimit c'), {to_liftable_cocone := {lifted_cocone := c, valid_lift := i ≪≫ hl.unique_up_to_iso t}, makes_colimit := category_theory.limits.is_colimit.of_faithful F (hl.of_iso_colimit i.symm) (λ (s : category_theory.limits.cocone K), F.preimage ((hl.of_iso_colimit i.symm).desc (F.map_cocone s))) _})
When F
is fully faithful, and has_colimit (K ⋙ F)
, to show that F
creates the colimit for K
it suffices to exhibit a lift of the chosen colimit cocone for K ⋙ F
.
When F
is fully faithful, to show that F
creates the colimit for K
it suffices to show that
a colimit point is in the essential image of F
.
Equations
- category_theory.creates_colimit_of_fully_faithful_of_iso' hl X i = category_theory.creates_colimit_of_fully_faithful_of_lift' hl {X := X, ι := {app := λ (j : J), F.preimage (l.ι.app j ≫ i.inv), naturality' := _}} (category_theory.limits.cocones.ext i _)
When F
is fully faithful, and has_colimit (K ⋙ F)
, to show that F
creates the colimit for K
it suffices to show that the chosen colimit point is in the essential image of F
.
F
preserves the colimit of K
if it creates the colimit and K ⋙ F
has the colimit.
Equations
- category_theory.preserves_colimit_of_creates_colimit_and_has_colimit K F = {preserves := λ (c : category_theory.limits.cocone K) (t : category_theory.limits.is_colimit c), (category_theory.limits.colimit.is_colimit (K ⋙ F)).of_iso_colimit ((category_theory.lifted_colimit_maps_to_original (category_theory.limits.colimit.is_colimit (K ⋙ F))).symm ≪≫ (category_theory.limits.cocones.functoriality K F).map_iso ((category_theory.lifted_colimit_is_colimit (category_theory.limits.colimit.is_colimit (K ⋙ F))).unique_up_to_iso t))}
F
preserves the colimit of shape J
if it creates these colimits and D
has them.
F
preserves limits if it creates limits and D
has limits.
Transfer creation of limits along a natural isomorphism in the diagram.
Equations
- category_theory.creates_limit_of_iso_diagram F h = {to_reflects_limit := {reflects := category_theory.limits.reflects_limit.reflects (category_theory.limits.reflects_limit_of_iso_diagram F h)}, lifts := λ (c : category_theory.limits.cone (K₂ ⋙ F)) (t : category_theory.limits.is_limit c), let t' : category_theory.limits.is_limit ((category_theory.limits.cones.postcompose (category_theory.iso_whisker_right h F).inv).obj c) := ⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.iso_whisker_right h F) c).symm) t in {lifted_cone := (category_theory.limits.cones.postcompose h.hom).obj (category_theory.lift_limit t'), valid_lift := F.map_cone_postcompose ≪≫ (category_theory.limits.cones.postcompose (category_theory.iso_whisker_right h F).hom).map_iso (category_theory.lifted_limit_maps_to_original t') ≪≫ category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.iso_whisker_right h F).hom).obj ((category_theory.limits.cones.postcompose (category_theory.iso_whisker_right h F).inv).obj c)).X) _}}
If F
creates the limit of K
and F ≅ G
, then G
creates the limit of K
.
Equations
- category_theory.creates_limit_of_nat_iso h = {to_reflects_limit := category_theory.limits.reflects_limit_of_nat_iso K h category_theory.creates_limit.to_reflects_limit, lifts := λ (c : category_theory.limits.cone (K ⋙ G)) (t : category_theory.limits.is_limit c), {lifted_cone := category_theory.lift_limit (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.iso_whisker_left K h) c).symm) t), valid_lift := (category_theory.limits.is_limit.map_cone_equiv h ((⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.iso_whisker_left K h) c).symm) t).of_iso_limit (category_theory.lifted_limit_maps_to_original (⇑((category_theory.limits.is_limit.postcompose_inv_equiv (category_theory.iso_whisker_left K h) c).symm) t)).symm)).unique_up_to_iso t}}
If F
creates limits of shape J
and F ≅ G
, then G
creates limits of shape J
.
Equations
If F
creates limits and F ≅ G
, then G
creates limits.
Equations
- category_theory.creates_limits_of_nat_iso h = {creates_limits_of_shape := λ (J : Type w') (𝒥₁ : category_theory.category J), category_theory.creates_limits_of_shape_of_nat_iso h}
Transfer creation of colimits along a natural isomorphism in the diagram.
Equations
- category_theory.creates_colimit_of_iso_diagram F h = {to_reflects_colimit := {reflects := category_theory.limits.reflects_colimit.reflects (category_theory.limits.reflects_colimit_of_iso_diagram F h)}, lifts := λ (c : category_theory.limits.cocone (K₂ ⋙ F)) (t : category_theory.limits.is_colimit c), let t' : category_theory.limits.is_colimit ((category_theory.limits.cocones.precompose (category_theory.iso_whisker_right h F).hom).obj c) := ⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.iso_whisker_right h F) c).symm) t in {lifted_cocone := (category_theory.limits.cocones.precompose h.inv).obj (category_theory.lift_colimit t'), valid_lift := F.map_cocone_precompose ≪≫ (category_theory.limits.cocones.precompose (category_theory.iso_whisker_right h F).inv).map_iso (category_theory.lifted_colimit_maps_to_original t') ≪≫ category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.iso_whisker_right h F).inv).obj ((category_theory.limits.cocones.precompose (category_theory.iso_whisker_right h F).hom).obj c)).X) _}}
If F
creates the colimit of K
and F ≅ G
, then G
creates the colimit of K
.
Equations
- category_theory.creates_colimit_of_nat_iso h = {to_reflects_colimit := category_theory.limits.reflects_colimit_of_nat_iso K h category_theory.creates_colimit.to_reflects_colimit, lifts := λ (c : category_theory.limits.cocone (K ⋙ G)) (t : category_theory.limits.is_colimit c), {lifted_cocone := category_theory.lift_colimit (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.iso_whisker_left K h) c).symm) t), valid_lift := (category_theory.limits.is_colimit.map_cocone_equiv h ((⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.iso_whisker_left K h) c).symm) t).of_iso_colimit (category_theory.lifted_colimit_maps_to_original (⇑((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.iso_whisker_left K h) c).symm) t)).symm)).unique_up_to_iso t}}
If F
creates colimits of shape J
and F ≅ G
, then G
creates colimits of shape J
.
Equations
If F
creates colimits and F ≅ G
, then G
creates colimits.
Equations
- category_theory.creates_colimits_of_nat_iso h = {creates_colimits_of_shape := λ (J : Type w') (𝒥₁ : category_theory.category J), category_theory.creates_colimits_of_shape_of_nat_iso h}
If F creates the limit of K, any cone lifts to a limit.
If F creates the colimit of K, any cocone lifts to a colimit.
Any cone lifts through the identity functor.
Equations
- category_theory.id_lifts_cone c = {lifted_cone := {X := c.X, π := c.π ≫ K.right_unitor.hom}, valid_lift := category_theory.limits.cones.ext (category_theory.iso.refl ((𝟭 C).map_cone {X := c.X, π := c.π ≫ K.right_unitor.hom}).X) _}
The identity functor creates all limits.
Equations
- category_theory.id_creates_limits = {creates_limits_of_shape := λ (J : Type w') (𝒥 : category_theory.category J), {creates_limit := λ (F : J ⥤ C), {to_reflects_limit := category_theory.limits.reflects_limit_of_reflects_limits_of_shape F (𝟭 C) (category_theory.limits.reflects_limits_of_shape_of_reflects_limits J (𝟭 C)), lifts := λ (c : category_theory.limits.cone (F ⋙ 𝟭 C)) (t : category_theory.limits.is_limit c), category_theory.id_lifts_cone c}}}
Any cocone lifts through the identity functor.
Equations
- category_theory.id_lifts_cocone c = {lifted_cocone := {X := c.X, ι := K.right_unitor.inv ≫ c.ι}, valid_lift := category_theory.limits.cocones.ext (category_theory.iso.refl ((𝟭 C).map_cocone {X := c.X, ι := K.right_unitor.inv ≫ c.ι}).X) _}
The identity functor creates all colimits.
Equations
- category_theory.id_creates_colimits = {creates_colimits_of_shape := λ (J : Type w') (𝒥 : category_theory.category J), {creates_colimit := λ (F : J ⥤ C), {to_reflects_colimit := category_theory.limits.reflects_colimit_of_reflects_colimits_of_shape F (𝟭 C) (category_theory.limits.reflects_colimits_of_shape_of_reflects_colimits J (𝟭 C)), lifts := λ (c : category_theory.limits.cocone (F ⋙ 𝟭 C)) (t : category_theory.limits.is_colimit c), category_theory.id_lifts_cocone c}}}
Satisfy the inhabited linter
Equations
Equations
Satisfy the inhabited linter
Equations
- category_theory.inhabited_lifts_to_limit K F c t = {default := category_theory.lifts_to_limit_of_creates K F c t}
Equations
Equations
- category_theory.comp_creates_limit F G = {to_reflects_limit := category_theory.limits.comp_reflects_limit F G category_theory.creates_limit.to_reflects_limit, lifts := λ (c : category_theory.limits.cone (K ⋙ F ⋙ G)) (t : category_theory.limits.is_limit c), {lifted_cone := category_theory.lift_limit (category_theory.lifted_limit_is_limit t), valid_lift := (category_theory.limits.cones.functoriality (K ⋙ F) G).map_iso (category_theory.lifted_limit_maps_to_original (category_theory.lifted_limit_is_limit t)) ≪≫ category_theory.lifted_limit_maps_to_original t}}
Equations
- category_theory.comp_creates_limits_of_shape F G = {creates_limit := infer_instance (λ {K : J ⥤ C}, category_theory.comp_creates_limit F G)}
Equations
- category_theory.comp_creates_limits F G = {creates_limits_of_shape := infer_instance (λ {J : Type w'} [_inst_4_1 : category_theory.category J], category_theory.comp_creates_limits_of_shape F G)}
Equations
- category_theory.comp_creates_colimit F G = {to_reflects_colimit := category_theory.limits.comp_reflects_colimit F G category_theory.creates_colimit.to_reflects_colimit, lifts := λ (c : category_theory.limits.cocone (K ⋙ F ⋙ G)) (t : category_theory.limits.is_colimit c), {lifted_cocone := category_theory.lift_colimit (category_theory.lifted_colimit_is_colimit t), valid_lift := (category_theory.limits.cocones.functoriality (K ⋙ F) G).map_iso (category_theory.lifted_colimit_maps_to_original (category_theory.lifted_colimit_is_colimit t)) ≪≫ category_theory.lifted_colimit_maps_to_original t}}
Equations
- category_theory.comp_creates_colimits_of_shape F G = {creates_colimit := infer_instance (λ {K : J ⥤ C}, category_theory.comp_creates_colimit F G)}
Equations
- category_theory.comp_creates_colimits F G = {creates_colimits_of_shape := infer_instance (λ {J : Type w'} [_inst_4_1 : category_theory.category J], category_theory.comp_creates_colimits_of_shape F G)}