Limits in C
give colimits in Cᵒᵖ
. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We also give special cases for (co)products, (co)equalizers, and pullbacks / pushouts.
Turn a colimit for F : J ⥤ C
into a limit for F.op : Jᵒᵖ ⥤ Cᵒᵖ
.
Turn a limit for F : J ⥤ C
into a colimit for F.op : Jᵒᵖ ⥤ Cᵒᵖ
.
Turn a colimit for F : J ⥤ Cᵒᵖ
into a limit for F.left_op : Jᵒᵖ ⥤ C
.
Equations
- category_theory.limits.is_limit_cone_left_op_of_cocone F hc = {lift := λ (s : category_theory.limits.cone F.left_op), (hc.desc (category_theory.limits.cocone_of_cone_left_op s)).unop, fac' := _, uniq' := _}
Turn a limit of F : J ⥤ Cᵒᵖ
into a colimit of F.left_op : Jᵒᵖ ⥤ C
.
Equations
- category_theory.limits.is_colimit_cocone_left_op_of_cone F hc = {desc := λ (s : category_theory.limits.cocone F.left_op), (hc.lift (category_theory.limits.cone_of_cocone_left_op s)).unop, fac' := _, uniq' := _}
Turn a colimit for F : Jᵒᵖ ⥤ C
into a limit for F.right_op : J ⥤ Cᵒᵖ
.
Equations
- category_theory.limits.is_limit_cone_right_op_of_cocone F hc = {lift := λ (s : category_theory.limits.cone F.right_op), (hc.desc (category_theory.limits.cocone_of_cone_right_op s)).op, fac' := _, uniq' := _}
Turn a limit for F : Jᵒᵖ ⥤ C
into a colimit for F.right_op : J ⥤ Cᵒᵖ
.
Equations
- category_theory.limits.is_colimit_cocone_right_op_of_cone F hc = {desc := λ (s : category_theory.limits.cocone F.right_op), (hc.lift (category_theory.limits.cone_of_cocone_right_op s)).op, fac' := _, uniq' := _}
Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
into a limit for F.unop : J ⥤ C
.
Equations
- category_theory.limits.is_limit_cone_unop_of_cocone F hc = {lift := λ (s : category_theory.limits.cone F.unop), (hc.desc (category_theory.limits.cocone_of_cone_unop s)).unop, fac' := _, uniq' := _}
Turn a limit of F : Jᵒᵖ ⥤ Cᵒᵖ
into a colimit of F.unop : J ⥤ C
.
Equations
- category_theory.limits.is_colimit_cocone_unop_of_cone F hc = {desc := λ (s : category_theory.limits.cocone F.unop), (hc.lift (category_theory.limits.cone_of_cocone_unop s)).unop, fac' := _, uniq' := _}
Turn a colimit for F.op : Jᵒᵖ ⥤ Cᵒᵖ
into a limit for F : J ⥤ C
.
Equations
- category_theory.limits.is_limit_cocone_unop F hc = {lift := λ (s : category_theory.limits.cone F), (hc.desc s.op).unop, fac' := _, uniq' := _}
Turn a limit for F.op : Jᵒᵖ ⥤ Cᵒᵖ
into a colimit for F : J ⥤ C
.
Equations
- category_theory.limits.is_colimit_cone_unop F hc = {desc := λ (s : category_theory.limits.cocone F), (hc.lift s.op).unop, fac' := _, uniq' := _}
Turn a colimit for F.left_op : Jᵒᵖ ⥤ C
into a limit for F : J ⥤ Cᵒᵖ
.
Equations
- category_theory.limits.is_limit_cone_of_cocone_left_op F hc = {lift := λ (s : category_theory.limits.cone F), (hc.desc (category_theory.limits.cocone_left_op_of_cone s)).op, fac' := _, uniq' := _}
Turn a limit of F.left_op : Jᵒᵖ ⥤ C
into a colimit of F : J ⥤ Cᵒᵖ
.
Equations
- category_theory.limits.is_colimit_cocone_of_cone_left_op F hc = {desc := λ (s : category_theory.limits.cocone F), (hc.lift (category_theory.limits.cone_left_op_of_cocone s)).op, fac' := _, uniq' := _}
Turn a colimit for F.right_op : J ⥤ Cᵒᵖ
into a limit for F : Jᵒᵖ ⥤ C
.
Equations
- category_theory.limits.is_limit_cone_of_cocone_right_op F hc = {lift := λ (s : category_theory.limits.cone F), (hc.desc (category_theory.limits.cocone_right_op_of_cone s)).unop, fac' := _, uniq' := _}
Turn a limit for F.right_op : J ⥤ Cᵒᵖ
into a limit for F : Jᵒᵖ ⥤ C
.
Equations
- category_theory.limits.is_colimit_cocone_of_cone_right_op F hc = {desc := λ (s : category_theory.limits.cocone F), (hc.lift (category_theory.limits.cone_right_op_of_cocone s)).unop, fac' := _, uniq' := _}
Turn a colimit for F.unop : J ⥤ C
into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
- category_theory.limits.is_limit_cone_of_cocone_unop F hc = {lift := λ (s : category_theory.limits.cone F), (hc.desc (category_theory.limits.cocone_unop_of_cone s)).op, fac' := _, uniq' := _}
Turn a limit for F.unop : J ⥤ C
into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ
.
Equations
- category_theory.limits.is_colimit_cone_of_cocone_unop F hc = {desc := λ (s : category_theory.limits.cocone F), (hc.lift (category_theory.limits.cone_unop_of_cocone s)).op, fac' := _, uniq' := _}
If F.left_op : Jᵒᵖ ⥤ C
has a colimit, we can construct a limit for F : J ⥤ Cᵒᵖ
.
If C
has colimits of shape Jᵒᵖ
, we can construct limits in Cᵒᵖ
of shape J
.
If C
has colimits, we can construct limits for Cᵒᵖ
.
If F.left_op : Jᵒᵖ ⥤ C
has a limit, we can construct a colimit for F : J ⥤ Cᵒᵖ
.
If C
has colimits of shape Jᵒᵖ
, we can construct limits in Cᵒᵖ
of shape J
.
If C
has limits, we can construct colimits for Cᵒᵖ
.
If C
has products indexed by X
, then Cᵒᵖ
has coproducts indexed by X
.
If C
has coproducts indexed by X
, then Cᵒᵖ
has products indexed by X
.
The canonical isomorphism relating span f.op g.op
and (cospan f g).op
Equations
- category_theory.limits.span_op f g = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_span), option.cases_on X_1 (category_theory.iso.refl ((category_theory.limits.span f.op g.op).obj option.none)) (λ (X_1 : category_theory.limits.walking_pair), X_1.cases_on (category_theory.iso.refl ((category_theory.limits.span f.op g.op).obj (option.some category_theory.limits.walking_pair.left))) (category_theory.iso.refl ((category_theory.limits.span f.op g.op).obj (option.some category_theory.limits.walking_pair.right))))) _
The canonical isomorphism relating (cospan f g).op
and span f.op g.op
Equations
- category_theory.limits.op_cospan f g = ((category_theory.iso.refl (category_theory.limits.cospan f g).op ≪≫ category_theory.iso_whisker_right category_theory.limits.walking_cospan_op_equiv.unit_iso (category_theory.limits.cospan f g).op) ≪≫ category_theory.limits.walking_cospan_op_equiv.functor.associator category_theory.limits.walking_cospan_op_equiv.inverse (category_theory.limits.cospan f g).op) ≪≫ category_theory.iso_whisker_left category_theory.limits.walking_cospan_op_equiv.functor (category_theory.limits.span_op f g).symm
The canonical isomorphism relating cospan f.op g.op
and (span f g).op
Equations
- category_theory.limits.cospan_op f g = category_theory.nat_iso.of_components (λ (X_1 : category_theory.limits.walking_cospan), option.cases_on X_1 (category_theory.iso.refl ((category_theory.limits.cospan f.op g.op).obj option.none)) (λ (X_1 : category_theory.limits.walking_pair), X_1.cases_on (category_theory.iso.refl ((category_theory.limits.cospan f.op g.op).obj (option.some category_theory.limits.walking_pair.left))) (category_theory.iso.refl ((category_theory.limits.cospan f.op g.op).obj (option.some category_theory.limits.walking_pair.right))))) _
The canonical isomorphism relating (span f g).op
and cospan f.op g.op
Equations
- category_theory.limits.op_span f g = ((category_theory.iso.refl (category_theory.limits.span f g).op ≪≫ category_theory.iso_whisker_right category_theory.limits.walking_span_op_equiv.unit_iso (category_theory.limits.span f g).op) ≪≫ category_theory.limits.walking_span_op_equiv.functor.associator category_theory.limits.walking_span_op_equiv.inverse (category_theory.limits.span f g).op) ≪≫ category_theory.iso_whisker_left category_theory.limits.walking_span_op_equiv.functor (category_theory.limits.cospan_op f g).symm
The obvious map pushout_cocone f g → pullback_cone f.unop g.unop
The obvious map pushout_cocone f.op g.op → pullback_cone f g
The obvious map pullback_cone f g → pushout_cocone f.unop g.unop
The obvious map pullback_cone f g → pushout_cocone f.op g.op
If c
is a pullback cone, then c.op.unop
is isomorphic to c
.
Equations
If c
is a pullback cone in Cᵒᵖ
, then c.unop.op
is isomorphic to c
.
Equations
If c
is a pushout cocone, then c.op.unop
is isomorphic to c
.
Equations
If c
is a pushout cocone in Cᵒᵖ
, then c.unop.op
is isomorphic to c
.
Equations
A pushout cone is a colimit cocone if and only if the corresponding pullback cone in the opposite category is a limit cone.
Equations
- c.is_colimit_equiv_is_limit_op = equiv_of_subsingleton_of_subsingleton (λ (h : category_theory.limits.is_colimit c), (category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.cospan_op f g).symm (category_theory.limits.cone.whisker category_theory.limits.walking_span_op_equiv.inverse (category_theory.limits.cocone.op c))).inv_fun ((category_theory.limits.is_limit.whisker_equivalence_equiv category_theory.limits.walking_span_op_equiv.symm).symm.inv_fun (category_theory.limits.is_limit_cocone_op (category_theory.limits.span f g) h))) (λ (h : category_theory.limits.is_limit c.op), (category_theory.limits.is_colimit.equiv_iso_colimit c.op_unop.symm).inv_fun (category_theory.limits.is_colimit_cone_unop (category_theory.limits.span f g) ((category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.limits.op_span f.op.unop g.op.unop).symm (category_theory.limits.cone.whisker category_theory.limits.walking_span_op_equiv.functor c.op)).inv_fun ((category_theory.limits.is_limit.whisker_equivalence_equiv category_theory.limits.walking_span_op_equiv).symm.inv_fun h))))
A pushout cone is a colimit cocone in Cᵒᵖ
if and only if the corresponding pullback cone
in C
is a limit cone.
Equations
- c.is_colimit_equiv_is_limit_unop = equiv_of_subsingleton_of_subsingleton (λ (h : category_theory.limits.is_colimit c), category_theory.limits.is_limit_cocone_unop (category_theory.limits.cospan f.unop g.unop) ((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.op_cospan f.unop g.unop) (category_theory.limits.cocone.whisker category_theory.limits.walking_cospan_op_equiv.functor c)).inv_fun ((category_theory.limits.is_colimit.whisker_equivalence_equiv category_theory.limits.walking_cospan_op_equiv).symm.inv_fun h))) (λ (h : category_theory.limits.is_limit c.unop), (category_theory.limits.is_colimit.equiv_iso_colimit c.unop_op.symm).inv_fun ((category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.limits.span_op f.unop g.unop) (category_theory.limits.cocone.whisker category_theory.limits.walking_cospan_op_equiv.inverse (category_theory.limits.cone.op c.unop))).inv_fun ((category_theory.limits.is_colimit.whisker_equivalence_equiv category_theory.limits.walking_cospan_op_equiv.symm).symm.inv_fun (category_theory.limits.is_colimit_cone_op (category_theory.limits.cospan f.unop g.unop) h))))
A pullback cone is a limit cone if and only if the corresponding pushout cocone in the opposite category is a colimit cocone.
A pullback cone is a limit cone in Cᵒᵖ
if and only if the corresponding pushout cocone
in C
is a colimit cocone.
The pullback of f
and g
in C
is isomorphic to the pushout of
f.op
and g.op
in Cᵒᵖ
.
Equations
- category_theory.limits.pullback_iso_unop_pushout f g = (category_theory.limits.limit.is_limit (category_theory.limits.cospan f.op.unop g.op.unop)).cone_point_unique_up_to_iso (⇑(category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_unop (category_theory.limits.colimit.cocone (category_theory.limits.span f.op g.op))) (category_theory.limits.colimit.is_colimit (category_theory.limits.span f.op g.op)))
The pushout of f
and g
in C
is isomorphic to the pullback of
f.op
and g.op
in Cᵒᵖ
.
Equations
- category_theory.limits.pushout_iso_unop_pullback f g = (category_theory.limits.colimit.is_colimit (category_theory.limits.span f.op.unop g.op.unop)).cocone_point_unique_up_to_iso (⇑(category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_unop (category_theory.limits.limit.cone (category_theory.limits.cospan f.op g.op))) (category_theory.limits.limit.is_limit (category_theory.limits.cospan f.op g.op)))