Limits in C give colimits in Cᵒᵖ. #
We also give special cases for (co)products, (co)equalizers, and pullbacks / pushouts.
def
CategoryTheory.Limits.isLimitConeLeftOpOfCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F}
(hc : IsColimit c)
:
Turn a colimit for F : J ⥤ Cᵒᵖ into a limit for F.leftOp : Jᵒᵖ ⥤ C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitConeLeftOpOfCocone_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F}
(hc : IsColimit c)
(s : Cone F.leftOp)
:
(isLimitConeLeftOpOfCocone F hc).lift s = (hc.desc (coconeOfConeLeftOp s)).unop
def
CategoryTheory.Limits.isColimitCoconeLeftOpOfCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F}
(hc : IsLimit c)
:
Turn a limit of F : J ⥤ Cᵒᵖ into a colimit of F.leftOp : Jᵒᵖ ⥤ C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitCoconeLeftOpOfCone_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F}
(hc : IsLimit c)
(s : Cocone F.leftOp)
:
(isColimitCoconeLeftOpOfCone F hc).desc s = (hc.lift (coneOfCoconeLeftOp s)).unop
def
CategoryTheory.Limits.isLimitConeRightOpOfCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F}
(hc : IsColimit c)
:
Turn a colimit for F : Jᵒᵖ ⥤ C into a limit for F.rightOp : J ⥤ Cᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitConeRightOpOfCocone_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F}
(hc : IsColimit c)
(s : Cone F.rightOp)
:
(isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (coconeOfConeRightOp s)).op
def
CategoryTheory.Limits.isColimitCoconeRightOpOfCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F}
(hc : IsLimit c)
:
Turn a limit for F : Jᵒᵖ ⥤ C into a colimit for F.rightOp : J ⥤ Cᵒᵖ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitCoconeRightOpOfCone_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F}
(hc : IsLimit c)
(s : Cocone F.rightOp)
:
(isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (coneOfCoconeRightOp s)).op
def
CategoryTheory.Limits.isLimitConeUnopOfCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F}
(hc : IsColimit c)
:
Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ into a limit for F.unop : J ⥤ C.
Equations
- CategoryTheory.Limits.isLimitConeUnopOfCocone F hc = { lift := fun (s : CategoryTheory.Limits.Cone F.unop) => (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop, fac := ⋯, uniq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitConeUnopOfCocone_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F}
(hc : IsColimit c)
(s : Cone F.unop)
:
(isLimitConeUnopOfCocone F hc).lift s = (hc.desc (coconeOfConeUnop s)).unop
def
CategoryTheory.Limits.isColimitCoconeUnopOfCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F}
(hc : IsLimit c)
:
Turn a limit of F : Jᵒᵖ ⥤ Cᵒᵖ into a colimit of F.unop : J ⥤ C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitCoconeUnopOfCone_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F}
(hc : IsLimit c)
(s : Cocone F.unop)
:
(isColimitCoconeUnopOfCone F hc).desc s = (hc.lift (coneOfCoconeUnop s)).unop
def
CategoryTheory.Limits.isLimitConeOfCoconeLeftOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F.leftOp}
(hc : IsColimit c)
:
Turn a colimit for F.leftOp : Jᵒᵖ ⥤ C into a limit for F : J ⥤ Cᵒᵖ.
Equations
- CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitConeOfCoconeLeftOp_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F.leftOp}
(hc : IsColimit c)
(s : Cone F)
:
(isLimitConeOfCoconeLeftOp F hc).lift s = (hc.desc (coconeLeftOpOfCone s)).op
def
CategoryTheory.Limits.isColimitCoconeOfConeLeftOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F.leftOp}
(hc : IsLimit c)
:
Turn a limit of F.leftOp : Jᵒᵖ ⥤ C into a colimit of F : J ⥤ Cᵒᵖ.
Equations
- CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc = { desc := fun (s : CategoryTheory.Limits.Cocone F) => (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitCoconeOfConeLeftOp_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F.leftOp}
(hc : IsLimit c)
(s : Cocone F)
:
(isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (coneLeftOpOfCocone s)).op
def
CategoryTheory.Limits.isLimitConeOfCoconeRightOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F.rightOp}
(hc : IsColimit c)
:
Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ into a limit for F : Jᵒᵖ ⥤ C.
Equations
- CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop, fac := ⋯, uniq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitConeOfCoconeRightOp_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F.rightOp}
(hc : IsColimit c)
(s : Cone F)
:
(isLimitConeOfCoconeRightOp F hc).lift s = (hc.desc (coconeRightOpOfCone s)).unop
def
CategoryTheory.Limits.isColimitCoconeOfConeRightOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F.rightOp}
(hc : IsLimit c)
:
Turn a limit for F.rightOp : J ⥤ Cᵒᵖ into a colimit for F : Jᵒᵖ ⥤ C.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitCoconeOfConeRightOp_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F.rightOp}
(hc : IsLimit c)
(s : Cocone F)
:
(isColimitCoconeOfConeRightOp F hc).desc s = (hc.lift (coneRightOpOfCocone s)).unop
def
CategoryTheory.Limits.isLimitConeOfCoconeUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F.unop}
(hc : IsColimit c)
:
Turn a colimit for F.unop : J ⥤ C into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ.
Equations
- CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc = { lift := fun (s : CategoryTheory.Limits.Cone F) => (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitConeOfCoconeUnop_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F.unop}
(hc : IsColimit c)
(s : Cone F)
:
(isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (coconeUnopOfCone s)).op
def
CategoryTheory.Limits.isColimitCoconeOfConeUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F.unop}
(hc : IsLimit c)
:
Turn a limit for F.unop : J ⥤ C into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ.
Equations
- CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc = { desc := fun (s : CategoryTheory.Limits.Cocone F) => (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op, fac := ⋯, uniq := ⋯ }
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitCoconeOfConeUnop_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F.unop}
(hc : IsLimit c)
(s : Cocone F)
:
(isColimitCoconeOfConeUnop F hc).desc s = (hc.lift (coneUnopOfCocone s)).op
def
CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F}
(hc : IsLimit (coneLeftOpOfCocone c))
:
Turn a limit for F.leftOp : Jᵒᵖ ⥤ C into a colimit for F : J ⥤ Cᵒᵖ.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F}
(hc : IsLimit (coneLeftOpOfCocone c))
(s : Cocone F)
:
(isColimitOfConeLeftOpOfCocone F hc).desc s = (hc.lift (coneLeftOpOfCocone s)).op
def
CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F}
(hc : IsColimit (coconeLeftOpOfCone c))
:
IsLimit c
Turn a colimit for F.leftOp : Jᵒᵖ ⥤ C into a limit for F : J ⥤ Cᵒᵖ.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F}
(hc : IsColimit (coconeLeftOpOfCone c))
(s : Cone F)
:
(isLimitOfCoconeLeftOpOfCone F hc).lift s = (hc.desc (coconeLeftOpOfCone s)).op
def
CategoryTheory.Limits.isColimitOfConeRightOpOfCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F}
(hc : IsLimit (coneRightOpOfCocone c))
:
Turn a limit for F.rightOp : J ⥤ Cᵒᵖ into a colimit for F : Jᵒᵖ ⥤ C.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitOfConeRightOpOfCocone_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F}
(hc : IsLimit (coneRightOpOfCocone c))
(s : Cocone F)
:
(isColimitOfConeRightOpOfCocone F hc).desc s = (hc.lift (coneRightOpOfCocone s)).unop
def
CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F}
(hc : IsColimit (coconeRightOpOfCone c))
:
IsLimit c
Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ into a limit for F : Jᵒᵖ ⥤ C.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F}
(hc : IsColimit (coconeRightOpOfCone c))
(s : Cone F)
:
(isLimitOfCoconeRightOpOfCone F hc).lift s = (hc.desc (coconeRightOpOfCone s)).unop
def
CategoryTheory.Limits.isColimitOfConeUnopOfCocone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F}
(hc : IsLimit (coneUnopOfCocone c))
:
Turn a limit for F.unop : J ⥤ C into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitOfConeUnopOfCocone_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F}
(hc : IsLimit (coneUnopOfCocone c))
(s : Cocone F)
:
(isColimitOfConeUnopOfCocone F hc).desc s = (hc.lift (coneUnopOfCocone s)).op
def
CategoryTheory.Limits.isLimitOfCoconeUnopOfCone
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F}
(hc : IsColimit (coconeUnopOfCone c))
:
IsLimit c
Turn a colimit for F.unop : J ⥤ C into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitOfCoconeUnopOfCone_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F}
(hc : IsColimit (coconeUnopOfCone c))
(s : Cone F)
:
(isLimitOfCoconeUnopOfCone F hc).lift s = (hc.desc (coconeUnopOfCone s)).op
def
CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F.leftOp}
(hc : IsLimit (coneOfCoconeLeftOp c))
:
Turn a limit for F : J ⥤ Cᵒᵖ into a colimit for F.leftOp : Jᵒᵖ ⥤ C.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cocone F.leftOp}
(hc : IsLimit (coneOfCoconeLeftOp c))
(s : Cocone F.leftOp)
:
(isColimitOfConeOfCoconeLeftOp F hc).desc s = (hc.lift (coneOfCoconeLeftOp s)).unop
def
CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F.leftOp}
(hc : IsColimit (coconeOfConeLeftOp c))
:
IsLimit c
Turn a colimit for F : J ⥤ Cᵒᵖ into a limit for F.leftOp : Jᵒᵖ ⥤ C.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
{c : Cone F.leftOp}
(hc : IsColimit (coconeOfConeLeftOp c))
(s : Cone F.leftOp)
:
(isLimitOfCoconeOfConeLeftOp F hc).lift s = (hc.desc (coconeOfConeLeftOp s)).unop
def
CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F.rightOp}
(hc : IsLimit (coneOfCoconeRightOp c))
:
Turn a limit for F : Jᵒᵖ ⥤ C into a colimit for F.rightOp : J ⥤ Cᵒᵖ.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cocone F.rightOp}
(hc : IsLimit (coneOfCoconeRightOp c))
(s : Cocone F.rightOp)
:
(isColimitOfConeOfCoconeRightOp F hc).desc s = (hc.lift (coneOfCoconeRightOp s)).op
def
CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F.rightOp}
(hc : IsColimit (coconeOfConeRightOp c))
:
IsLimit c
Turn a colimit for F : Jᵒᵖ ⥤ C into a limit for F.rightOp : J ⥤ Cᵒᵖ.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
{c : Cone F.rightOp}
(hc : IsColimit (coconeOfConeRightOp c))
(s : Cone F.rightOp)
:
(isLimitOfCoconeOfConeRightOp F hc).lift s = (hc.desc (coconeOfConeRightOp s)).op
def
CategoryTheory.Limits.isColimitOfConeOfCoconeUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F.unop}
(hc : IsLimit (coneOfCoconeUnop c))
:
Turn a limit for F : Jᵒᵖ ⥤ Cᵒᵖ into a colimit for F.unop : J ⥤ C.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isColimitOfConeOfCoconeUnop_desc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cocone F.unop}
(hc : IsLimit (coneOfCoconeUnop c))
(s : Cocone F.unop)
:
(isColimitOfConeOfCoconeUnop F hc).desc s = (hc.lift (coneOfCoconeUnop s)).unop
def
CategoryTheory.Limits.isLimitOfCoconeOfConeUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F.unop}
(hc : IsColimit (coconeOfConeUnop c))
:
IsLimit c
Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ into a limit for F.unop : J ⥤ C.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Limits.isLimitOfCoconeOfConeUnop_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F.unop}
(hc : IsColimit (coconeOfConeUnop c))
(s : Cone F.unop)
:
(isLimitOfCoconeOfConeUnop F hc).lift s = (hc.desc (coconeOfConeUnop s)).unop
@[deprecated CategoryTheory.Limits.isColimitCoconeOfConeUnop (since := "2024-11-01")]
def
CategoryTheory.Limits.isColimitConeOfCoconeUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
{c : Cone F.unop}
(hc : IsLimit c)
:
Alias of CategoryTheory.Limits.isColimitCoconeOfConeUnop.
Turn a limit for F.unop : J ⥤ C into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ.
Equations
Instances For
theorem
CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasColimit F.leftOp]
:
HasLimit F
If F.leftOp : Jᵒᵖ ⥤ C has a colimit, we can construct a limit for F : J ⥤ Cᵒᵖ.
theorem
CategoryTheory.Limits.hasLimit_of_hasColimit_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasColimit F.op]
:
HasLimit F
theorem
CategoryTheory.Limits.hasLimit_of_hasColimit_rightOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasColimit F.rightOp]
:
HasLimit F
theorem
CategoryTheory.Limits.hasLimit_of_hasColimit_unop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasColimit F.unop]
:
HasLimit F
instance
CategoryTheory.Limits.hasLimit_op_of_hasColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasColimit F]
:
HasLimit F.op
instance
CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasColimit F]
:
HasLimit F.leftOp
instance
CategoryTheory.Limits.hasLimit_rightOp_of_hasColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasColimit F]
:
HasLimit F.rightOp
instance
CategoryTheory.Limits.hasLimit_unop_of_hasColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasColimit F]
:
HasLimit F.unop
def
CategoryTheory.Limits.limitOpIsoOpColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasColimit F]
:
limit F.op ≅ Opposite.op (colimit F)
The limit of F.op is the opposite of colimit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasColimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (limitOpIsoOpColimit F).inv (limit.π F.op j) = (colimit.ι F (Opposite.unop j)).op
@[simp]
theorem
CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasColimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : F.op.obj j ⟶ Z)
:
CategoryStruct.comp (limitOpIsoOpColimit F).inv (CategoryStruct.comp (limit.π F.op j) h) = CategoryStruct.comp (colimit.ι F (Opposite.unop j)).op h
@[simp]
theorem
CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasColimit F]
(j : J)
:
CategoryStruct.comp (limitOpIsoOpColimit F).hom (colimit.ι F j).op = limit.π F.op (Opposite.op j)
@[simp]
theorem
CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasColimit F]
(j : J)
{Z : Cᵒᵖ}
(h : Opposite.op (F.obj j) ⟶ Z)
:
CategoryStruct.comp (limitOpIsoOpColimit F).hom (CategoryStruct.comp (colimit.ι F j).op h) = CategoryStruct.comp (limit.π F.op (Opposite.op j)) h
def
CategoryTheory.Limits.limitLeftOpIsoUnopColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasColimit F]
:
limit F.leftOp ≅ Opposite.unop (colimit F)
The limit of F.leftOp is the unopposite of colimit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_inv_comp_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasColimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (limitLeftOpIsoUnopColimit F).inv (limit.π F.leftOp j) = (colimit.ι F (Opposite.unop j)).unop
@[simp]
theorem
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_inv_comp_π_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasColimit F]
(j : Jᵒᵖ)
{Z : C}
(h : F.leftOp.obj j ⟶ Z)
:
CategoryStruct.comp (limitLeftOpIsoUnopColimit F).inv (CategoryStruct.comp (limit.π F.leftOp j) h) = CategoryStruct.comp (colimit.ι F (Opposite.unop j)).unop h
@[simp]
theorem
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasColimit F]
(j : J)
:
CategoryStruct.comp (limitLeftOpIsoUnopColimit F).hom (colimit.ι F j).unop = limit.π F.leftOp (Opposite.op j)
@[simp]
theorem
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasColimit F]
(j : J)
{Z : C}
(h : Opposite.unop (F.obj j) ⟶ Z)
:
CategoryStruct.comp (limitLeftOpIsoUnopColimit F).hom (CategoryStruct.comp (colimit.ι F j).unop h) = CategoryStruct.comp (limit.π F.leftOp (Opposite.op j)) h
def
CategoryTheory.Limits.limitRightOpIsoOpColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasColimit F]
:
limit F.rightOp ≅ Opposite.op (colimit F)
The limit of F.rightOp is the opposite of colimit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasColimit F]
(j : J)
:
CategoryStruct.comp (limitRightOpIsoOpColimit F).inv (limit.π F.rightOp j) = (colimit.ι F (Opposite.op j)).op
@[simp]
theorem
CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasColimit F]
(j : J)
{Z : Cᵒᵖ}
(h : F.rightOp.obj j ⟶ Z)
:
CategoryStruct.comp (limitRightOpIsoOpColimit F).inv (CategoryStruct.comp (limit.π F.rightOp j) h) = CategoryStruct.comp (colimit.ι F (Opposite.op j)).op h
@[simp]
theorem
CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasColimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (limitRightOpIsoOpColimit F).hom (colimit.ι F j).op = limit.π F.rightOp (Opposite.unop j)
@[simp]
theorem
CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasColimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : Opposite.op (F.obj j) ⟶ Z)
:
CategoryStruct.comp (limitRightOpIsoOpColimit F).hom (CategoryStruct.comp (colimit.ι F j).op h) = CategoryStruct.comp (limit.π F.rightOp (Opposite.unop j)) h
def
CategoryTheory.Limits.limitUnopIsoUnopColimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasColimit F]
:
limit F.unop ≅ Opposite.unop (colimit F)
The limit of F.unop is the unopposite of colimit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.limitUnopIsoUnopColimit_inv_comp_π
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasColimit F]
(j : J)
:
CategoryStruct.comp (limitUnopIsoUnopColimit F).inv (limit.π F.unop j) = (colimit.ι F (Opposite.op j)).unop
@[simp]
theorem
CategoryTheory.Limits.limitUnopIsoUnopColimit_inv_comp_π_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasColimit F]
(j : J)
{Z : C}
(h : F.unop.obj j ⟶ Z)
:
CategoryStruct.comp (limitUnopIsoUnopColimit F).inv (CategoryStruct.comp (limit.π F.unop j) h) = CategoryStruct.comp (colimit.ι F (Opposite.op j)).unop h
@[simp]
theorem
CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasColimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (limitUnopIsoUnopColimit F).hom (colimit.ι F j).unop = limit.π F.unop (Opposite.unop j)
@[simp]
theorem
CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasColimit F]
(j : Jᵒᵖ)
{Z : C}
(h : Opposite.unop (F.obj j) ⟶ Z)
:
CategoryStruct.comp (limitUnopIsoUnopColimit F).hom (CategoryStruct.comp (colimit.ι F j).unop h) = CategoryStruct.comp (limit.π F.unop (Opposite.unop j)) h
theorem
CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
[HasColimitsOfShape Jᵒᵖ C]
:
If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
theorem
CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
[HasColimitsOfShape Jᵒᵖ Cᵒᵖ]
:
HasLimitsOfShape J C
instance
CategoryTheory.Limits.hasLimits_op_of_hasColimits
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasColimitsOfSize.{v₂, u₂, v₁, u₁} C]
:
If C has colimits, we can construct limits for Cᵒᵖ.
theorem
CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasLimit F.leftOp]
:
If F.leftOp : Jᵒᵖ ⥤ C has a limit, we can construct a colimit for F : J ⥤ Cᵒᵖ.
theorem
CategoryTheory.Limits.hasColimit_of_hasLimit_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasLimit F.op]
:
theorem
CategoryTheory.Limits.hasColimit_of_hasLimit_rightOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasLimit F.rightOp]
:
theorem
CategoryTheory.Limits.hasColimit_of_hasLimit_unop
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasLimit F.unop]
:
instance
CategoryTheory.Limits.hasColimit_op_of_hasLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasLimit F]
:
HasColimit F.op
instance
CategoryTheory.Limits.hasColimit_leftOp_of_hasLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasLimit F]
:
HasColimit F.leftOp
instance
CategoryTheory.Limits.hasColimit_rightOp_of_hasLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasLimit F]
:
HasColimit F.rightOp
instance
CategoryTheory.Limits.hasColimit_unop_of_hasLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasLimit F]
:
HasColimit F.unop
def
CategoryTheory.Limits.colimitOpIsoOpLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasLimit F]
:
colimit F.op ≅ Opposite.op (limit F)
The colimit of F.op is the opposite of limit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasLimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (colimit.ι F.op j) (colimitOpIsoOpLimit F).hom = (limit.π F (Opposite.unop j)).op
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasLimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : Opposite.op (limit F) ⟶ Z)
:
CategoryStruct.comp (colimit.ι F.op j) (CategoryStruct.comp (colimitOpIsoOpLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.unop j)).op h
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasLimit F]
(j : J)
:
CategoryStruct.comp (limit.π F j).op (colimitOpIsoOpLimit F).inv = colimit.ι F.op (Opposite.op j)
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J C)
[HasLimit F]
(j : J)
{Z : Cᵒᵖ}
(h : colimit F.op ⟶ Z)
:
CategoryStruct.comp (limit.π F j).op (CategoryStruct.comp (colimitOpIsoOpLimit F).inv h) = CategoryStruct.comp (colimit.ι F.op (Opposite.op j)) h
def
CategoryTheory.Limits.colimitLeftOpIsoUnopLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasLimit F]
:
colimit F.leftOp ≅ Opposite.unop (limit F)
The colimit of F.leftOp is the unopposite of limit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitLeftOpIsoUnopLimit_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasLimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (colimit.ι F.leftOp j) (colimitLeftOpIsoUnopLimit F).hom = (limit.π F (Opposite.unop j)).unop
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasLimit F]
(j : Jᵒᵖ)
{Z : C}
(h : Opposite.unop (limit F) ⟶ Z)
:
CategoryStruct.comp (colimit.ι F.leftOp j) (CategoryStruct.comp (colimitLeftOpIsoUnopLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.unop j)).unop h
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasLimit F]
(j : J)
:
CategoryStruct.comp (limit.π F j).unop (colimitLeftOpIsoUnopLimit F).inv = colimit.ι F.leftOp (Opposite.op j)
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor J Cᵒᵖ)
[HasLimit F]
(j : J)
{Z : C}
(h : colimit F.leftOp ⟶ Z)
:
CategoryStruct.comp (limit.π F j).unop (CategoryStruct.comp (colimitLeftOpIsoUnopLimit F).inv h) = CategoryStruct.comp (colimit.ι F.leftOp (Opposite.op j)) h
def
CategoryTheory.Limits.colimitRightOpIsoUnopLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasLimit F]
:
colimit F.rightOp ≅ Opposite.op (limit F)
The colimit of F.rightOp is the opposite of limit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasLimit F]
(j : J)
:
CategoryStruct.comp (colimit.ι F.rightOp j) (colimitRightOpIsoUnopLimit F).hom = (limit.π F (Opposite.op j)).op
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasLimit F]
(j : J)
{Z : Cᵒᵖ}
(h : Opposite.op (limit F) ⟶ Z)
:
CategoryStruct.comp (colimit.ι F.rightOp j) (CategoryStruct.comp (colimitRightOpIsoUnopLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.op j)).op h
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasLimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (limit.π F j).op (colimitRightOpIsoUnopLimit F).inv = colimit.ι F.rightOp (Opposite.unop j)
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ C)
[HasLimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : colimit F.rightOp ⟶ Z)
:
CategoryStruct.comp (limit.π F j).op (CategoryStruct.comp (colimitRightOpIsoUnopLimit F).inv h) = CategoryStruct.comp (colimit.ι F.rightOp (Opposite.unop j)) h
def
CategoryTheory.Limits.colimitUnopIsoOpLimit
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasLimit F]
:
colimit F.unop ≅ Opposite.unop (limit F)
The colimit of F.unop is the unopposite of limit F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitUnopIsoOpLimit_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasLimit F]
(j : J)
:
CategoryStruct.comp (colimit.ι F.unop j) (colimitUnopIsoOpLimit F).hom = (limit.π F (Opposite.op j)).unop
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitUnopIsoOpLimit_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasLimit F]
(j : J)
{Z : C}
(h : Opposite.unop (limit F) ⟶ Z)
:
CategoryStruct.comp (colimit.ι F.unop j) (CategoryStruct.comp (colimitUnopIsoOpLimit F).hom h) = CategoryStruct.comp (limit.π F (Opposite.op j)).unop h
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasLimit F]
(j : Jᵒᵖ)
:
CategoryStruct.comp (limit.π F j).unop (colimitUnopIsoOpLimit F).inv = colimit.ι F.unop (Opposite.unop j)
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
(F : Functor Jᵒᵖ Cᵒᵖ)
[HasLimit F]
(j : Jᵒᵖ)
{Z : C}
(h : colimit F.unop ⟶ Z)
:
CategoryStruct.comp (limit.π F j).unop (CategoryStruct.comp (colimitUnopIsoOpLimit F).inv h) = CategoryStruct.comp (colimit.ι F.unop (Opposite.unop j)) h
instance
CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
[HasLimitsOfShape Jᵒᵖ C]
:
If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
theorem
CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op
{C : Type u₁}
[Category.{v₁, u₁} C]
{J : Type u₂}
[Category.{v₂, u₂} J]
[HasLimitsOfShape Jᵒᵖ Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasColimits_op_of_hasLimits
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasLimitsOfSize.{v₂, u₂, v₁, u₁} C]
:
If C has limits, we can construct colimits for Cᵒᵖ.
instance
CategoryTheory.Limits.hasCoproductsOfShape_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Type v₂)
[HasProductsOfShape X C]
:
If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.
theorem
CategoryTheory.Limits.hasCoproductsOfShape_of_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Type v₂)
[HasProductsOfShape X Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasProductsOfShape_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Type v₂)
[HasCoproductsOfShape X C]
:
If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.
theorem
CategoryTheory.Limits.hasProductsOfShape_of_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
(X : Type v₂)
[HasCoproductsOfShape X Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasProducts_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasCoproducts C]
:
theorem
CategoryTheory.Limits.hasProducts_of_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasCoproducts Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasCoproducts_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasProducts C]
:
theorem
CategoryTheory.Limits.hasCoproducts_of_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasProducts Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasFiniteCoproducts_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasFiniteProducts C]
:
theorem
CategoryTheory.Limits.hasFiniteCoproducts_of_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasFiniteProducts Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasFiniteProducts_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasFiniteCoproducts C]
:
theorem
CategoryTheory.Limits.hasFiniteProducts_of_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasFiniteCoproducts Cᵒᵖ]
:
instance
CategoryTheory.Limits.instHasLimitOppositeDiscreteOpFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasCoproduct Z]
:
HasLimit (Discrete.functor Z).op
instance
CategoryTheory.Limits.instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasCoproduct Z]
:
HasLimit ((Discrete.opposite α).inverse.comp (Discrete.functor Z).op)
instance
CategoryTheory.Limits.instHasProductOppositeOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasCoproduct Z]
:
HasProduct fun (x : α) => Opposite.op (Z x)
def
CategoryTheory.Limits.Cofan.op
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
(c : Cofan Z)
:
Fan fun (x : α) => Opposite.op (Z x)
A Cofan gives a Fan in the opposite category.
Equations
- c.op = CategoryTheory.Limits.Fan.mk (Opposite.op c.pt) fun (a : α) => (c.inj a).op
Instances For
noncomputable def
CategoryTheory.Limits.Cofan.IsColimit.op
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : Cofan Z}
(hc : IsColimit c)
:
IsLimit c.op
If a Cofan is colimit, then its opposite is limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.opCoproductIsoProduct'
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : Cofan Z}
{f : Fan fun (x : α) => Opposite.op (Z x)}
(hc : IsColimit c)
(hf : IsLimit f)
:
Opposite.op c.pt ≅ f.pt
The canonical isomorphism from the opposite of an abstract coproduct to the corresponding product in the opposite category.
Equations
- CategoryTheory.Limits.opCoproductIsoProduct' hc hf = (CategoryTheory.Limits.Cofan.IsColimit.op hc).conePointUniqueUpToIso hf
Instances For
def
CategoryTheory.Limits.opCoproductIsoProduct
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[HasCoproduct Z]
:
Opposite.op (∐ Z) ≅ ∏ᶜ fun (x : α) => Opposite.op (Z x)
The canonical isomorphism from the opposite of the coproduct to the product in the opposite category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : Cofan Z}
{f : Fan fun (x : α) => Opposite.op (Z x)}
(hc : IsColimit c)
(hf : IsLimit f)
(b : α)
:
CategoryStruct.comp (opCoproductIsoProduct' hc hf).inv (c.inj b).op = f.proj b
theorem
CategoryTheory.Limits.opCoproductIsoProduct'_comp_self
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c c' : Cofan Z}
{f : Fan fun (x : α) => Opposite.op (Z x)}
(hc : IsColimit c)
(hc' : IsColimit c')
(hf : IsLimit f)
:
CategoryStruct.comp (opCoproductIsoProduct' hc hf).hom (opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv
theorem
CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[HasCoproduct Z]
(b : α)
:
CategoryStruct.comp (opCoproductIsoProduct Z).inv (Sigma.ι Z b).op = Pi.π (fun (x : α) => Opposite.op (Z x)) b
theorem
CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : Cofan Z}
{f : Fan fun (x : α) => Opposite.op (Z x)}
(hc : IsColimit c)
(hf : IsLimit f)
(c' : Cofan Z)
:
CategoryStruct.comp (hc.desc c').op (opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
theorem
CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasCoproduct Z]
{X : C}
(π : (a : α) → Z a ⟶ X)
:
CategoryStruct.comp (Sigma.desc π).op (opCoproductIsoProduct Z).hom = Pi.lift fun (a : α) => (π a).op
instance
CategoryTheory.Limits.instHasColimitOppositeDiscreteOpFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasProduct Z]
:
HasColimit (Discrete.functor Z).op
instance
CategoryTheory.Limits.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasProduct Z]
:
HasColimit ((Discrete.opposite α).inverse.comp (Discrete.functor Z).op)
instance
CategoryTheory.Limits.instHasCoproductOppositeOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasProduct Z]
:
HasCoproduct fun (x : α) => Opposite.op (Z x)
def
CategoryTheory.Limits.Fan.op
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
(f : Fan Z)
:
Cofan fun (x : α) => Opposite.op (Z x)
A Fan gives a Cofan in the opposite category.
Equations
- f.op = CategoryTheory.Limits.Cofan.mk (Opposite.op f.pt) fun (a : α) => (f.proj a).op
Instances For
noncomputable def
CategoryTheory.Limits.Fan.IsLimit.op
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : Fan Z}
(hf : IsLimit f)
:
IsColimit f.op
If a Fan is limit, then its opposite is colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.opProductIsoCoproduct'
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : Fan Z}
{c : Cofan fun (x : α) => Opposite.op (Z x)}
(hf : IsLimit f)
(hc : IsColimit c)
:
Opposite.op f.pt ≅ c.pt
The canonical isomorphism from the opposite of an abstract product to the corresponding coproduct in the opposite category.
Equations
- CategoryTheory.Limits.opProductIsoCoproduct' hf hc = (CategoryTheory.Limits.Fan.IsLimit.op hf).coconePointUniqueUpToIso hc
Instances For
def
CategoryTheory.Limits.opProductIsoCoproduct
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[HasProduct Z]
:
Opposite.op (∏ᶜ Z) ≅ ∐ fun (x : α) => Opposite.op (Z x)
The canonical isomorphism from the opposite of the product to the coproduct in the opposite category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : Fan Z}
{c : Cofan fun (x : α) => Opposite.op (Z x)}
(hf : IsLimit f)
(hc : IsColimit c)
(b : α)
:
CategoryStruct.comp (f.proj b).op (opProductIsoCoproduct' hf hc).hom = c.inj b
theorem
CategoryTheory.Limits.opProductIsoCoproduct'_comp_self
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f f' : Fan Z}
{c : Cofan fun (x : α) => Opposite.op (Z x)}
(hf : IsLimit f)
(hf' : IsLimit f')
(hc : IsColimit c)
:
CategoryStruct.comp (opProductIsoCoproduct' hf hc).hom (opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv
theorem
CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[HasProduct Z]
(b : α)
:
CategoryStruct.comp (Pi.π Z b).op (opProductIsoCoproduct Z).hom = Sigma.ι (fun (x : α) => Opposite.op (Z x)) b
theorem
CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : Fan Z}
{c : Cofan fun (x : α) => Opposite.op (Z x)}
(hf : IsLimit f)
(hc : IsColimit c)
(f' : Fan Z)
:
CategoryStruct.comp (opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op
theorem
CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift
{C : Type u₁}
[Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[HasProduct Z]
{X : C}
(π : (a : α) → X ⟶ Z a)
:
CategoryStruct.comp (opProductIsoCoproduct Z).inv (Pi.lift π).op = Sigma.desc fun (a : α) => (π a).op
instance
CategoryTheory.Limits.instHasBinaryCoproductOppositeOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
HasBinaryCoproduct (Opposite.op A) (Opposite.op B)
def
CategoryTheory.Limits.opProdIsoCoprod
{C : Type u₁}
[Category.{v₁, u₁} C]
(A B : C)
[HasBinaryProduct A B]
:
Opposite.op (A ⨯ B) ≅ Opposite.op A ⨿ Opposite.op B
The canonical isomorphism from the opposite of the binary product to the coproduct in the opposite category.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.fst_opProdIsoCoprod_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp prod.fst.op (opProdIsoCoprod A B).hom = coprod.inl
@[simp]
theorem
CategoryTheory.Limits.fst_opProdIsoCoprod_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op A ⨿ Opposite.op B ⟶ Z)
:
CategoryStruct.comp prod.fst.op (CategoryStruct.comp (opProdIsoCoprod A B).hom h) = CategoryStruct.comp coprod.inl h
@[simp]
theorem
CategoryTheory.Limits.snd_opProdIsoCoprod_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp prod.snd.op (opProdIsoCoprod A B).hom = coprod.inr
@[simp]
theorem
CategoryTheory.Limits.snd_opProdIsoCoprod_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op A ⨿ Opposite.op B ⟶ Z)
:
CategoryStruct.comp prod.snd.op (CategoryStruct.comp (opProdIsoCoprod A B).hom h) = CategoryStruct.comp coprod.inr h
@[simp]
theorem
CategoryTheory.Limits.inl_opProdIsoCoprod_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp coprod.inl (opProdIsoCoprod A B).inv = prod.fst.op
@[simp]
theorem
CategoryTheory.Limits.inl_opProdIsoCoprod_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op (A ⨯ B) ⟶ Z)
:
CategoryStruct.comp coprod.inl (CategoryStruct.comp (opProdIsoCoprod A B).inv h) = CategoryStruct.comp prod.fst.op h
@[simp]
theorem
CategoryTheory.Limits.inr_opProdIsoCoprod_inv
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp coprod.inr (opProdIsoCoprod A B).inv = prod.snd.op
@[simp]
theorem
CategoryTheory.Limits.inr_opProdIsoCoprod_inv_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op (A ⨯ B) ⟶ Z)
:
CategoryStruct.comp coprod.inr (CategoryStruct.comp (opProdIsoCoprod A B).inv h) = CategoryStruct.comp prod.snd.op h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp (opProdIsoCoprod A B).hom.unop prod.fst = coprod.inl.unop
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_fst_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : C}
(h : A ⟶ Z)
:
CategoryStruct.comp (opProdIsoCoprod A B).hom.unop (CategoryStruct.comp prod.fst h) = CategoryStruct.comp coprod.inl.unop h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp (opProdIsoCoprod A B).hom.unop prod.snd = coprod.inr.unop
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_snd_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : C}
(h : B ⟶ Z)
:
CategoryStruct.comp (opProdIsoCoprod A B).hom.unop (CategoryStruct.comp prod.snd h) = CategoryStruct.comp coprod.inr.unop h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inl
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp (opProdIsoCoprod A B).inv.unop coprod.inl.unop = prod.fst
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inl_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : C}
(h : A ⟶ Z)
:
CategoryStruct.comp (opProdIsoCoprod A B).inv.unop (CategoryStruct.comp coprod.inl.unop h) = CategoryStruct.comp prod.fst h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inr
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
:
CategoryStruct.comp (opProdIsoCoprod A B).inv.unop coprod.inr.unop = prod.snd
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inr_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{A B : C}
[HasBinaryProduct A B]
{Z : C}
(h : B ⟶ Z)
:
CategoryStruct.comp (opProdIsoCoprod A B).inv.unop (CategoryStruct.comp coprod.inr.unop h) = CategoryStruct.comp prod.snd h
instance
CategoryTheory.Limits.hasEqualizers_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasCoequalizers C]
:
instance
CategoryTheory.Limits.hasCoequalizers_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasEqualizers C]
:
instance
CategoryTheory.Limits.hasFiniteColimits_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasFiniteLimits C]
:
instance
CategoryTheory.Limits.hasFiniteLimits_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasFiniteColimits C]
:
instance
CategoryTheory.Limits.hasPullbacks_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasPushouts C]
:
instance
CategoryTheory.Limits.hasPushouts_opposite
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasPullbacks C]
:
def
CategoryTheory.Limits.spanOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
span f.op g.op ≅ walkingCospanOpEquiv.inverse.comp (cospan f g).op
The canonical isomorphism relating Span f.op g.op and (Cospan f g).op
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.spanOp_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : WalkingSpan)
:
(spanOp f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op Z))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).hom
@[simp]
theorem
CategoryTheory.Limits.spanOp_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : WalkingSpan)
:
(spanOp f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op Z))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).inv
def
CategoryTheory.Limits.opCospan
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
(cospan f g).op ≅ walkingCospanOpEquiv.functor.comp (span f.op g.op)
The canonical isomorphism relating (Cospan f g).op and Span f.op g.op
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.opCospan_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : WalkingCospanᵒᵖ)
:
(opCospan f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op Z))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val)
(Opposite.unop X✝)).hom
@[simp]
theorem
CategoryTheory.Limits.opCospan_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : WalkingCospanᵒᵖ)
:
(opCospan f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op Z))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val)
(Opposite.unop X✝)).inv
def
CategoryTheory.Limits.cospanOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
cospan f.op g.op ≅ walkingSpanOpEquiv.inverse.comp (span f g).op
The canonical isomorphism relating Cospan f.op g.op and (Span f g).op
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.cospanOp_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : WalkingCospan)
:
(cospanOp f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op X))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).inv
@[simp]
theorem
CategoryTheory.Limits.cospanOp_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : WalkingCospan)
:
(cospanOp f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op X))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).hom
def
CategoryTheory.Limits.opSpan
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
(span f g).op ≅ walkingSpanOpEquiv.functor.comp (cospan f.op g.op)
The canonical isomorphism relating (Span f g).op and Cospan f.op g.op
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.opSpan_hom_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : WalkingSpanᵒᵖ)
:
(opSpan f g).hom.app X✝ = (Option.rec (Iso.refl (Opposite.op X))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val)
(Opposite.unop X✝)).inv
@[simp]
theorem
CategoryTheory.Limits.opSpan_inv_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : WalkingSpanᵒᵖ)
:
(opSpan f g).inv.app X✝ = (Option.rec (Iso.refl (Opposite.op X))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val)
(Opposite.unop X✝)).hom
def
CategoryTheory.Limits.PushoutCocone.unop
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
PullbackCone f.unop g.unop
The obvious map PushoutCocone f g → PullbackCone f.unop g.unop
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.unop_π_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
(X✝ : WalkingCospan)
:
c.unop.π.app X✝ = CategoryStruct.comp (c.ι.app X✝).unop
(Option.rec (Iso.refl X) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl Y) (Iso.refl Z) val) X✝).inv.unop
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.unop_pt
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.unop.pt = Opposite.unop c.pt
theorem
CategoryTheory.Limits.PushoutCocone.unop_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.unop.fst = c.inl.unop
theorem
CategoryTheory.Limits.PushoutCocone.unop_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.unop.snd = c.inr.unop
def
CategoryTheory.Limits.PushoutCocone.op
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
PullbackCone f.op g.op
The obvious map PushoutCocone f.op g.op → PullbackCone f g
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.op_pt
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.op.pt = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.op_π_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
(X✝ : WalkingCospan)
:
c.op.π.app X✝ = CategoryStruct.comp (c.ι.app X✝).op
(Option.rec (Iso.refl (Opposite.op X))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op Y)) (Iso.refl (Opposite.op Z)) val) X✝).inv
theorem
CategoryTheory.Limits.PushoutCocone.op_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.op.fst = c.inl.op
theorem
CategoryTheory.Limits.PushoutCocone.op_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.op.snd = c.inr.op
def
CategoryTheory.Limits.PullbackCone.unop
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
PushoutCocone f.unop g.unop
The obvious map PullbackCone f g → PushoutCocone f.unop g.unop
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.unop_ι_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
(X✝ : WalkingSpan)
:
c.unop.ι.app X✝ = CategoryStruct.comp
(Option.rec (Iso.refl Z) (fun (val : WalkingPair) => WalkingPair.rec (Iso.refl X) (Iso.refl Y) val) X✝).hom.unop
(c.π.app X✝).unop
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.unop_pt
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.unop.pt = Opposite.unop c.pt
theorem
CategoryTheory.Limits.PullbackCone.unop_inl
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.unop.inl = c.fst.unop
theorem
CategoryTheory.Limits.PullbackCone.unop_inr
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.unop.inr = c.snd.unop
def
CategoryTheory.Limits.PullbackCone.op
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
PushoutCocone f.op g.op
The obvious map PullbackCone f g → PushoutCocone f.op g.op
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.op_pt
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.op.pt = Opposite.op c.pt
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.op_ι_app
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
(X✝ : WalkingSpan)
:
c.op.ι.app X✝ = CategoryStruct.comp
(Option.rec (Iso.refl (Opposite.op Z))
(fun (val : WalkingPair) => WalkingPair.rec (Iso.refl (Opposite.op X)) (Iso.refl (Opposite.op Y)) val) X✝).hom
(c.π.app X✝).op
theorem
CategoryTheory.Limits.PullbackCone.op_inl
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.op.inl = c.fst.op
theorem
CategoryTheory.Limits.PullbackCone.op_inr
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.op.inr = c.snd.op
def
CategoryTheory.Limits.PullbackCone.opUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.op.unop ≅ c
If c is a pullback cone, then c.op.unop is isomorphic to c.
Equations
- c.opUnop = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl c.op.unop.pt) ⋯ ⋯
Instances For
def
CategoryTheory.Limits.PullbackCone.unopOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone f g)
:
c.unop.op ≅ c
If c is a pullback cone in Cᵒᵖ, then c.unop.op is isomorphic to c.
Equations
- c.unopOp = CategoryTheory.Limits.PullbackCone.ext (CategoryTheory.Iso.refl c.unop.op.pt) ⋯ ⋯
Instances For
def
CategoryTheory.Limits.PushoutCocone.opUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.op.unop ≅ c
If c is a pushout cocone, then c.op.unop is isomorphic to c.
Equations
- c.opUnop = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl c.op.unop.pt) ⋯ ⋯
Instances For
def
CategoryTheory.Limits.PushoutCocone.unopOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone f g)
:
c.unop.op ≅ c
If c is a pushout cocone in Cᵒᵖ, then c.unop.op is isomorphic to c.
Equations
- c.unopOp = CategoryTheory.Limits.PushoutCocone.ext (CategoryTheory.Iso.refl c.unop.op.pt) ⋯ ⋯
Instances For
noncomputable def
CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone 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
- One or more equations did not get rendered due to their size.
Instances For
noncomputable def
CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : PushoutCocone 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
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone 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.
Equations
- c.isLimitEquivIsColimitOp = (CategoryTheory.Limits.IsLimit.equivIsoLimit c.opUnop).symm.trans c.op.isColimitEquivIsLimitUnop.symm
Instances For
def
CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : PullbackCone 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.
Equations
- c.isLimitEquivIsColimitUnop = (CategoryTheory.Limits.IsLimit.equivIsoLimit c.unopOp).symm.trans c.unop.isColimitEquivIsLimitOp.symm
Instances For
noncomputable def
CategoryTheory.Limits.pullbackIsoUnopPushout
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[h : HasPullback f g]
[HasPushout f.op g.op]
:
pullback f g ≅ Opposite.unop (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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
:
CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (pullback.fst f g) = (pushout.inl f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
{Z✝ : C}
(h : X ⟶ Z✝)
:
CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (CategoryStruct.comp (pullback.fst f g) h) = CategoryStruct.comp (pushout.inl f.op g.op).unop h
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
:
CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (pullback.snd f g) = (pushout.inr f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
{Z✝ : C}
(h : Y ⟶ Z✝)
:
CategoryStruct.comp (pullbackIsoUnopPushout f g).inv (CategoryStruct.comp (pullback.snd f g) h) = CategoryStruct.comp (pushout.inr f.op g.op).unop h
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
:
CategoryStruct.comp (pushout.inl f.op g.op) (pullbackIsoUnopPushout f g).hom.op = (pullback.fst f g).op
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
{Z✝ : Cᵒᵖ}
(h : Opposite.op (pullback f g) ⟶ Z✝)
:
CategoryStruct.comp (pushout.inl f.op g.op) (CategoryStruct.comp (pullbackIsoUnopPushout f g).hom.op h) = CategoryStruct.comp (pullback.fst f g).op h
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
:
CategoryStruct.comp (pushout.inr f.op g.op) (pullbackIsoUnopPushout f g).hom.op = (pullback.snd f g).op
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[HasPullback f g]
[HasPushout f.op g.op]
{Z✝ : Cᵒᵖ}
(h : Opposite.op (pullback f g) ⟶ Z✝)
:
CategoryStruct.comp (pushout.inr f.op g.op) (CategoryStruct.comp (pullbackIsoUnopPushout f g).hom.op h) = CategoryStruct.comp (pullback.snd f g).op h
noncomputable def
CategoryTheory.Limits.pushoutIsoUnopPullback
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[h : HasPushout f g]
[HasPullback f.op g.op]
:
pushout f g ≅ Opposite.unop (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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[HasPushout f g]
[HasPullback f.op g.op]
:
CategoryStruct.comp (pushout.inl f g) (pushoutIsoUnopPullback f g).hom = (pullback.fst f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[HasPushout f g]
[HasPullback f.op g.op]
{Z✝ : C}
(h : Opposite.unop (pullback f.op g.op) ⟶ Z✝)
:
CategoryStruct.comp (pushout.inl f g) (CategoryStruct.comp (pushoutIsoUnopPullback f g).hom h) = CategoryStruct.comp (pullback.fst f.op g.op).unop h
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[HasPushout f g]
[HasPullback f.op g.op]
:
CategoryStruct.comp (pushout.inr f g) (pushoutIsoUnopPullback f g).hom = (pullback.snd f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[HasPushout f g]
[HasPullback f.op g.op]
{Z✝ : C}
(h : Opposite.unop (pullback f.op g.op) ⟶ Z✝)
:
CategoryStruct.comp (pushout.inr f g) (CategoryStruct.comp (pushoutIsoUnopPullback f g).hom h) = CategoryStruct.comp (pullback.snd f.op g.op).unop h
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[HasPushout f g]
[HasPullback f.op g.op]
:
CategoryStruct.comp (pushoutIsoUnopPullback f g).inv.op (pullback.fst f.op g.op) = (pushout.inl f g).op
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd
{C : Type u₁}
[Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[HasPushout f g]
[HasPullback f.op g.op]
:
CategoryStruct.comp (pushoutIsoUnopPullback f g).inv.op (pullback.snd f.op g.op) = (pushout.inr f g).op
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{X Y Q : C}
(p : Y ⟶ Q)
{f : X ⟶ Y}
(w : CategoryStruct.comp f p = 0)
(h : IsColimit (CokernelCofork.ofπ p w))
:
IsLimit (KernelFork.ofι p.op ⋯)
A colimit cokernel cofork gives a limit kernel fork in the opposite category
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{X Y Q : Cᵒᵖ}
(p : Y ⟶ Q)
{f : X ⟶ Y}
(w : CategoryStruct.comp f p = 0)
(h : IsColimit (CokernelCofork.ofπ p w))
:
IsLimit (KernelFork.ofι p.unop ⋯)
A colimit cokernel cofork in the opposite category gives a limit kernel fork in the original category
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.ofιOp
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{K X Y : C}
(i : K ⟶ X)
{f : X ⟶ Y}
(w : CategoryStruct.comp i f = 0)
(h : IsLimit (KernelFork.ofι i w))
:
IsColimit (CokernelCofork.ofπ i.op ⋯)
A limit kernel fork gives a colimit cokernel cofork in the opposite category
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop
{C : Type u₁}
[Category.{v₁, u₁} C]
[HasZeroMorphisms C]
{K X Y : Cᵒᵖ}
(i : K ⟶ X)
{f : X ⟶ Y}
(w : CategoryStruct.comp i f = 0)
(h : IsLimit (KernelFork.ofι i w))
:
IsColimit (CokernelCofork.ofπ i.unop ⋯)
A limit kernel fork in the opposite category gives a colimit cokernel cofork in the original category
Equations
- One or more equations did not get rendered due to their size.