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.
def
category_theory.limits.is_limit_cocone_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c) :
Turn a colimit for F : J ⥤ C into a limit for F.op : Jᵒᵖ ⥤ Cᵒᵖ.
@[simp]
theorem
category_theory.limits.is_limit_cocone_op_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F.op) :
def
category_theory.limits.is_colimit_cone_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c) :
Turn a limit for F : J ⥤ C into a colimit for F.op : Jᵒᵖ ⥤ Cᵒᵖ.
@[simp]
theorem
category_theory.limits.is_colimit_cone_op_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F.op) :
def
category_theory.limits.is_limit_cone_left_op_of_cocone
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit 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' := _}
@[simp]
theorem
category_theory.limits.is_limit_cone_left_op_of_cocone_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F.left_op) :
def
category_theory.limits.is_colimit_cocone_left_op_of_cone
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_colimit_cocone_left_op_of_cone_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F.left_op) :
@[simp]
theorem
category_theory.limits.is_limit_cone_right_op_of_cocone_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F.right_op) :
def
category_theory.limits.is_limit_cone_right_op_of_cocone
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c) :
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' := _}
def
category_theory.limits.is_colimit_cocone_right_op_of_cone
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_colimit_cocone_right_op_of_cone_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F.right_op) :
def
category_theory.limits.is_limit_cone_unop_of_cocone
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_limit_cone_unop_of_cocone_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F.unop) :
@[simp]
theorem
category_theory.limits.is_colimit_cocone_unop_of_cone_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F.unop) :
def
category_theory.limits.is_colimit_cocone_unop_of_cone
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F}
(hc : category_theory.limits.is_limit c) :
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' := _}
def
category_theory.limits.is_limit_cocone_unop
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cocone F.op}
(hc : category_theory.limits.is_colimit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_limit_cocone_unop_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cocone F.op}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.is_colimit_cone_unop_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cone F.op}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F) :
def
category_theory.limits.is_colimit_cone_unop
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
{c : category_theory.limits.cone F.op}
(hc : category_theory.limits.is_limit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_limit_cone_of_cocone_left_op_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F.left_op}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F) :
def
category_theory.limits.is_limit_cone_of_cocone_left_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F.left_op}
(hc : category_theory.limits.is_colimit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_colimit_cocone_of_cone_left_op_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F.left_op}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F) :
def
category_theory.limits.is_colimit_cocone_of_cone_left_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F.left_op}
(hc : category_theory.limits.is_limit c) :
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' := _}
def
category_theory.limits.is_limit_cone_of_cocone_right_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cocone F.right_op}
(hc : category_theory.limits.is_colimit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_limit_cone_of_cocone_right_op_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cocone F.right_op}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F) :
@[simp]
theorem
category_theory.limits.is_colimit_cocone_of_cone_right_op_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cone F.right_op}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F) :
def
category_theory.limits.is_colimit_cocone_of_cone_right_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ C)
{c : category_theory.limits.cone F.right_op}
(hc : category_theory.limits.is_limit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_limit_cone_of_cocone_unop_lift
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F.unop}
(hc : category_theory.limits.is_colimit c)
(s : category_theory.limits.cone F) :
def
category_theory.limits.is_limit_cone_of_cocone_unop
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cocone F.unop}
(hc : category_theory.limits.is_colimit c) :
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' := _}
def
category_theory.limits.is_colimit_cone_of_cocone_unop
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F.unop}
(hc : category_theory.limits.is_limit c) :
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' := _}
@[simp]
theorem
category_theory.limits.is_colimit_cone_of_cocone_unop_desc
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : Jᵒᵖ ⥤ Cᵒᵖ)
{c : category_theory.limits.cone F.unop}
(hc : category_theory.limits.is_limit c)
(s : category_theory.limits.cocone F) :
theorem
category_theory.limits.has_limit_of_has_colimit_left_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
[category_theory.limits.has_colimit F.left_op] :
If F.left_op : Jᵒᵖ ⥤ C has a colimit, we can construct a limit for F : J ⥤ Cᵒᵖ.
theorem
category_theory.limits.has_limit_of_has_colimit_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.has_colimit F.op] :
theorem
category_theory.limits.has_limits_of_shape_op_of_has_colimits_of_shape
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
[category_theory.limits.has_colimits_of_shape Jᵒᵖ C] :
If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
@[protected, instance]
def
category_theory.limits.has_limits_op_of_has_colimits
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_colimits C] :
If C has colimits, we can construct limits for Cᵒᵖ.
@[protected, instance]
theorem
category_theory.limits.has_colimit_of_has_limit_left_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ Cᵒᵖ)
[category_theory.limits.has_limit F.left_op] :
If F.left_op : Jᵒᵖ ⥤ C has a limit, we can construct a colimit for F : J ⥤ Cᵒᵖ.
theorem
category_theory.limits.has_colimit_of_has_limit_op
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
(F : J ⥤ C)
[category_theory.limits.has_limit F.op] :
@[protected, instance]
def
category_theory.limits.has_colimits_of_shape_op_of_has_limits_of_shape
{C : Type u₁}
[category_theory.category C]
{J : Type u₂}
[category_theory.category J]
[category_theory.limits.has_limits_of_shape Jᵒᵖ C] :
If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
@[protected, instance]
def
category_theory.limits.has_colimits_op_of_has_limits
{C : Type u₁}
[category_theory.category C]
[category_theory.limits.has_limits C] :
If C has limits, we can construct colimits for Cᵒᵖ.
@[protected, instance]
@[protected, instance]
def
category_theory.limits.has_coproducts_of_shape_opposite
{C : Type u₁}
[category_theory.category C]
(X : Type v₂)
[category_theory.limits.has_products_of_shape X C] :
If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.
theorem
category_theory.limits.has_coproducts_of_shape_of_opposite
{C : Type u₁}
[category_theory.category C]
(X : Type v₂)
[category_theory.limits.has_products_of_shape X Cᵒᵖ] :
@[protected, instance]
def
category_theory.limits.has_products_of_shape_opposite
{C : Type u₁}
[category_theory.category C]
(X : Type v₂)
[category_theory.limits.has_coproducts_of_shape X C] :
If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.
theorem
category_theory.limits.has_products_of_shape_of_opposite
{C : Type u₁}
[category_theory.category C]
(X : Type v₂)
[category_theory.limits.has_coproducts_of_shape X Cᵒᵖ] :
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
theorem
category_theory.limits.span_op_inv_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X_1 : category_theory.limits.walking_span) :
(category_theory.limits.span_op f g).inv.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) X_1).inv
@[simp]
theorem
category_theory.limits.span_op_hom_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X_1 : category_theory.limits.walking_span) :
(category_theory.limits.span_op f g).hom.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) X_1).hom
def
category_theory.limits.span_op
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
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))))) _
@[simp]
theorem
category_theory.limits.op_cospan_inv_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X_1 : category_theory.limits.walking_cospanᵒᵖ) :
(category_theory.limits.op_cospan f g).inv.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) (opposite.unop X_1)).hom ≫ (𝟙 (category_theory.limits.cospan f g).op).app X_1
@[simp]
theorem
category_theory.limits.op_cospan_hom_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X_1 : category_theory.limits.walking_cospanᵒᵖ) :
(category_theory.limits.op_cospan f g).hom.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) (opposite.unop X_1)).inv
def
category_theory.limits.op_cospan
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z) :
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
def
category_theory.limits.cospan_op
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
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))))) _
@[simp]
theorem
category_theory.limits.cospan_op_inv_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X_1 : category_theory.limits.walking_cospan) :
(category_theory.limits.cospan_op f g).inv.app X_1 = (option.rec (category_theory.iso.refl (opposite.op X)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op Y)) (category_theory.iso.refl (opposite.op Z))) X_1).inv
@[simp]
theorem
category_theory.limits.cospan_op_hom_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X_1 : category_theory.limits.walking_cospan) :
(category_theory.limits.cospan_op f g).hom.app X_1 = (option.rec (category_theory.iso.refl (opposite.op X)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op Y)) (category_theory.iso.refl (opposite.op Z))) X_1).hom
def
category_theory.limits.op_span
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z) :
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
@[simp]
theorem
category_theory.limits.op_span_inv_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X_1 : category_theory.limits.walking_spanᵒᵖ) :
(category_theory.limits.op_span f g).inv.app X_1 = (option.rec (category_theory.iso.refl (opposite.op X)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op Y)) (category_theory.iso.refl (opposite.op Z))) (opposite.unop X_1)).hom ≫ (𝟙 (category_theory.limits.span f g).op).app X_1
@[simp]
theorem
category_theory.limits.op_span_hom_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X_1 : category_theory.limits.walking_spanᵒᵖ) :
(category_theory.limits.op_span f g).hom.app X_1 = (option.rec (category_theory.iso.refl (opposite.op X)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op Y)) (category_theory.iso.refl (opposite.op Z))) (opposite.unop X_1)).inv
theorem
category_theory.limits.pushout_cocone.unop_π_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g)
(X_1 : category_theory.limits.walking_cospan) :
c.unop.π.app X_1 = (c.ι.app X_1).unop ≫ (option.rec (category_theory.iso.refl (opposite.op (opposite.unop X))) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op (opposite.unop Y))) (category_theory.iso.refl (opposite.op (opposite.unop Z)))) (opposite.unop (opposite.op X_1))).inv.unop
def
category_theory.limits.pushout_cocone.unop
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
The obvious map pushout_cocone f g → pullback_cone f.unop g.unop
theorem
category_theory.limits.pushout_cocone.unop_X
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
c.unop.X = opposite.unop c.X
@[simp]
theorem
category_theory.limits.pushout_cocone.unop_fst
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
@[simp]
theorem
category_theory.limits.pushout_cocone.unop_snd
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
theorem
category_theory.limits.pushout_cocone.op_π_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g)
(X_1 : category_theory.limits.walking_cospan) :
c.op.π.app X_1 = (c.ι.app X_1).op ≫ (option.rec (category_theory.iso.refl (opposite.op X)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op Y)) (category_theory.iso.refl (opposite.op Z))) X_1).inv
theorem
category_theory.limits.pushout_cocone.op_X
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
c.op.X = opposite.op c.X
def
category_theory.limits.pushout_cocone.op
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
The obvious map pushout_cocone f.op g.op → pullback_cone f g
@[simp]
theorem
category_theory.limits.pushout_cocone.op_fst
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
@[simp]
theorem
category_theory.limits.pushout_cocone.op_snd
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
def
category_theory.limits.pullback_cone.unop
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
The obvious map pullback_cone f g → pushout_cocone f.unop g.unop
theorem
category_theory.limits.pullback_cone.unop_X
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
c.unop.X = opposite.unop c.X
theorem
category_theory.limits.pullback_cone.unop_ι_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g)
(X_1 : category_theory.limits.walking_span) :
c.unop.ι.app X_1 = ((𝟙 (category_theory.limits.span f.unop g.unop).op).app (opposite.op X_1)).unop ≫ (option.rec (category_theory.iso.refl (opposite.op (opposite.unop Z))) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op (opposite.unop X))) (category_theory.iso.refl (opposite.op (opposite.unop Y)))) (opposite.unop (opposite.op X_1))).hom.unop ≫ (c.π.app X_1).unop
@[simp]
theorem
category_theory.limits.pullback_cone.unop_inl
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
@[simp]
theorem
category_theory.limits.pullback_cone.unop_inr
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
def
category_theory.limits.pullback_cone.op
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
The obvious map pullback_cone f g → pushout_cocone f.op g.op
theorem
category_theory.limits.pullback_cone.op_ι_app
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g)
(X_1 : category_theory.limits.walking_span) :
c.op.ι.app X_1 = (option.rec (category_theory.iso.refl (opposite.op Z)) (category_theory.limits.walking_pair.rec (category_theory.iso.refl (opposite.op X)) (category_theory.iso.refl (opposite.op Y))) X_1).hom ≫ (c.π.app X_1).op
theorem
category_theory.limits.pullback_cone.op_X
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
c.op.X = opposite.op c.X
@[simp]
theorem
category_theory.limits.pullback_cone.op_inl
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
@[simp]
theorem
category_theory.limits.pullback_cone.op_inr
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
def
category_theory.limits.pullback_cone.op_unop
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
If c is a pullback cone, then c.op.unop is isomorphic to c.
Equations
def
category_theory.limits.pullback_cone.unop_op
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
If c is a pullback cone in Cᵒᵖ, then c.unop.op is isomorphic to c.
Equations
def
category_theory.limits.pushout_cocone.op_unop
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
If c is a pushout cocone, then c.op.unop is isomorphic to c.
Equations
def
category_theory.limits.pushout_cocone.unop_op
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
If c is a pushout cocone in Cᵒᵖ, then c.unop.op is isomorphic to c.
Equations
def
category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_op
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
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))))
def
category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_unop
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : category_theory.limits.pushout_cocone f g) :
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))))
def
category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_op
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
A pullback cone is a limit cone if and only if the corresponding pushout cocone in the opposite category is a colimit cocone.
def
category_theory.limits.pullback_cone.is_limit_equiv_is_colimit_unop
{C : Type u₁}
[category_theory.category C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : category_theory.limits.pullback_cone f g) :
A pullback cone is a limit cone in Cᵒᵖ if and only if the corresponding pushout cocone
in C is a colimit cocone.
noncomputable
def
category_theory.limits.pullback_iso_unop_pushout
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op] :
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)))
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_inv_fst_assoc
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op]
{X' : C}
(f' : X ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_inv_fst
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op] :
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_inv_snd
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op] :
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_inv_snd_assoc
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op]
{X' : C}
(f' : Y ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_hom_inl
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op] :
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_hom_inl_assoc
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op]
{X' : Cᵒᵖ}
(f' : opposite.op (category_theory.limits.pullback f g) ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_hom_inr_assoc
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op]
{X' : Cᵒᵖ}
(f' : opposite.op (category_theory.limits.pullback f g) ⟶ X') :
@[simp]
theorem
category_theory.limits.pullback_iso_unop_pushout_hom_inr
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[category_theory.limits.has_pullback f g]
[category_theory.limits.has_pushout f.op g.op] :
noncomputable
def
category_theory.limits.pushout_iso_unop_pullback
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pullback 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)))
@[simp]
theorem
category_theory.limits.pushout_iso_unop_pullback_inl_hom_assoc
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pullback f.op g.op]
{X' : C}
(f' : opposite.unop (category_theory.limits.pullback f.op g.op) ⟶ X') :
@[simp]
theorem
category_theory.limits.pushout_iso_unop_pullback_inl_hom
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pullback f.op g.op] :
@[simp]
theorem
category_theory.limits.pushout_iso_unop_pullback_inr_hom
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pullback f.op g.op] :
@[simp]
theorem
category_theory.limits.pushout_iso_unop_pullback_inr_hom_assoc
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pullback f.op g.op]
{X' : C}
(f' : opposite.unop (category_theory.limits.pullback f.op g.op) ⟶ X') :
@[simp]
theorem
category_theory.limits.pushout_iso_unop_pullback_inv_fst
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pullback f.op g.op] :
@[simp]
theorem
category_theory.limits.pushout_iso_unop_pullback_inv_snd
{C : Type u₁}
[category_theory.category C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[category_theory.limits.has_pushout f g]
[category_theory.limits.has_pullback f.op g.op] :