Limits in C give colimits in Cᵒᵖ. #
We also give special cases for (co)products, (co)equalizers, and pullbacks / pushouts.
@[deprecated CategoryTheory.Limits.IsColimit.op]
def
CategoryTheory.Limits.isLimitCoconeOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{t : CategoryTheory.Limits.Cocone F}
(P : CategoryTheory.Limits.IsColimit t)
:
Alias of CategoryTheory.Limits.IsColimit.op.
If t : Cocone F is a colimit cocone, then t.op : Cone F.op is a limit cone.
Instances For
@[deprecated CategoryTheory.Limits.IsLimit.op]
def
CategoryTheory.Limits.isColimitConeOp
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{t : CategoryTheory.Limits.Cone F}
(P : CategoryTheory.Limits.IsLimit t)
:
Alias of CategoryTheory.Limits.IsLimit.op.
If t : Cone F is a limit cone, then t.op : Cocone F.op is a colimit cocone.
Instances For
@[deprecated CategoryTheory.Limits.IsColimit.unop]
def
CategoryTheory.Limits.isLimitCoconeUnop
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{t : CategoryTheory.Limits.Cocone F.op}
(P : CategoryTheory.Limits.IsColimit t)
:
Alias of CategoryTheory.Limits.IsColimit.unop.
If t : Cocone F.op is a colimit cocone, then t.unop : Cone F is a limit cone.
Instances For
@[deprecated CategoryTheory.Limits.IsLimit.unop]
def
CategoryTheory.Limits.isColimitConeUnop
{J : Type u₁}
[CategoryTheory.Category.{v₁, u₁} J]
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{F : CategoryTheory.Functor J C}
{t : CategoryTheory.Limits.Cone F.op}
(P : CategoryTheory.Limits.IsLimit t)
:
Alias of CategoryTheory.Limits.IsLimit.unop.
If t : Cone F.op is a limit cone, then t.unop : Cocone F is a colimit cocone.
Instances For
def
CategoryTheory.Limits.isLimitConeLeftOpOfCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsColimit c)
(s : CategoryTheory.Limits.Cone F.leftOp)
:
(CategoryTheory.Limits.isLimitConeLeftOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
def
CategoryTheory.Limits.isColimitCoconeLeftOpOfCone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
(s : CategoryTheory.Limits.Cocone F.leftOp)
:
(CategoryTheory.Limits.isColimitCoconeLeftOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
def
CategoryTheory.Limits.isLimitConeRightOpOfCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsColimit c)
(s : CategoryTheory.Limits.Cone F.rightOp)
:
(CategoryTheory.Limits.isLimitConeRightOpOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
def
CategoryTheory.Limits.isColimitCoconeRightOpOfCone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
(s : CategoryTheory.Limits.Cocone F.rightOp)
:
(CategoryTheory.Limits.isColimitCoconeRightOpOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
def
CategoryTheory.Limits.isLimitConeUnopOfCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsColimit c)
(s : CategoryTheory.Limits.Cone F.unop)
:
(CategoryTheory.Limits.isLimitConeUnopOfCocone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
def
CategoryTheory.Limits.isColimitCoconeUnopOfCone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
(s : CategoryTheory.Limits.Cocone F.unop)
:
(CategoryTheory.Limits.isColimitCoconeUnopOfCone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
def
CategoryTheory.Limits.isLimitConeOfCoconeLeftOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.leftOp}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.leftOp}
(hc : CategoryTheory.Limits.IsColimit c)
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.isLimitConeOfCoconeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
def
CategoryTheory.Limits.isColimitCoconeOfConeLeftOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.leftOp}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.leftOp}
(hc : CategoryTheory.Limits.IsLimit c)
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.isColimitCoconeOfConeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
def
CategoryTheory.Limits.isLimitConeOfCoconeRightOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F.rightOp}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F.rightOp}
(hc : CategoryTheory.Limits.IsColimit c)
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.isLimitConeOfCoconeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
def
CategoryTheory.Limits.isColimitCoconeOfConeRightOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F.rightOp}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F.rightOp}
(hc : CategoryTheory.Limits.IsLimit c)
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.isColimitCoconeOfConeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
def
CategoryTheory.Limits.isLimitConeOfCoconeUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.unop}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.unop}
(hc : CategoryTheory.Limits.IsColimit c)
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.isLimitConeOfCoconeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
def
CategoryTheory.Limits.isColimitCoconeOfConeUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.unop}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.unop}
(hc : CategoryTheory.Limits.IsLimit c)
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.isColimitCoconeOfConeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
def
CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneLeftOpOfCocone c))
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.isColimitOfConeLeftOpOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneLeftOpOfCocone s)).op
def
CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeLeftOpOfCone c))
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.isLimitOfCoconeLeftOpOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeLeftOpOfCone s)).op
def
CategoryTheory.Limits.isColimitOfConeRightOpOfCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneRightOpOfCocone c))
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.isColimitOfConeRightOpOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneRightOpOfCocone s)).unop
def
CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeRightOpOfCone 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeRightOpOfCone c))
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.isLimitOfCoconeRightOpOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeRightOpOfCone s)).unop
def
CategoryTheory.Limits.isColimitOfConeUnopOfCocone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneUnopOfCocone c))
(s : CategoryTheory.Limits.Cocone F)
:
(CategoryTheory.Limits.isColimitOfConeUnopOfCocone F hc).desc s = (hc.lift (CategoryTheory.Limits.coneUnopOfCocone s)).op
def
CategoryTheory.Limits.isLimitOfCoconeUnopOfCone
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeUnopOfCone c))
(s : CategoryTheory.Limits.Cone F)
:
(CategoryTheory.Limits.isLimitOfCoconeUnopOfCone F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeUnopOfCone s)).op
def
CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.leftOp}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.leftOp}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeLeftOp c))
(s : CategoryTheory.Limits.Cocone F.leftOp)
:
(CategoryTheory.Limits.isColimitOfConeOfCoconeLeftOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeLeftOp s)).unop
def
CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.leftOp}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeLeftOp 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.leftOp}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeLeftOp c))
(s : CategoryTheory.Limits.Cone F.leftOp)
:
(CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeLeftOp s)).unop
def
CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F.rightOp}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cocone F.rightOp}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeRightOp c))
(s : CategoryTheory.Limits.Cocone F.rightOp)
:
(CategoryTheory.Limits.isColimitOfConeOfCoconeRightOp F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeRightOp s)).op
def
CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F.rightOp}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
{c : CategoryTheory.Limits.Cone F.rightOp}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeRightOp c))
(s : CategoryTheory.Limits.Cone F.rightOp)
:
(CategoryTheory.Limits.isLimitOfCoconeOfConeRightOp F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeRightOp s)).op
def
CategoryTheory.Limits.isColimitOfConeOfCoconeUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.unop}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cocone F.unop}
(hc : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.coneOfCoconeUnop c))
(s : CategoryTheory.Limits.Cocone F.unop)
:
(CategoryTheory.Limits.isColimitOfConeOfCoconeUnop F hc).desc s = (hc.lift (CategoryTheory.Limits.coneOfCoconeUnop s)).unop
def
CategoryTheory.Limits.isLimitOfCoconeOfConeUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.unop}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeUnop 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.unop}
(hc : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeUnop c))
(s : CategoryTheory.Limits.Cone F.unop)
:
(CategoryTheory.Limits.isLimitOfCoconeOfConeUnop F hc).lift s = (hc.desc (CategoryTheory.Limits.coconeOfConeUnop s)).unop
@[deprecated CategoryTheory.Limits.isColimitCoconeOfConeUnop]
def
CategoryTheory.Limits.isColimitConeOfCoconeUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
{c : CategoryTheory.Limits.Cone F.unop}
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F.leftOp]
:
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F.op]
:
theorem
CategoryTheory.Limits.hasLimit_of_hasColimit_rightOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasColimit F.rightOp]
:
theorem
CategoryTheory.Limits.hasLimit_of_hasColimit_unop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F.unop]
:
instance
CategoryTheory.Limits.hasLimit_op_of_hasColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasLimit_leftOp_of_hasColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
:
CategoryTheory.Limits.HasLimit F.leftOp
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasLimit_rightOp_of_hasColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasColimit F]
:
CategoryTheory.Limits.HasLimit F.rightOp
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasLimit_unop_of_hasColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.limitOpIsoOpColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : F.op.obj j ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F]
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F]
(j : J)
{Z : Cᵒᵖ}
(h : Opposite.op (F.obj j) ⟶ Z)
:
def
CategoryTheory.Limits.limitLeftOpIsoUnopColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasColimit 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitLeftOpIsoUnopColimit F).inv
(CategoryTheory.Limits.limit.π F.leftOp j) = (CategoryTheory.Limits.colimit.ι F (Opposite.unop j)).unop
@[simp]
theorem
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_inv_comp_π_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
{Z : C}
(h : F.leftOp.obj j ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.limitLeftOpIsoUnopColimit_hom_comp_ι_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : J)
{Z : C}
(h : Opposite.unop (F.obj j) ⟶ Z)
:
def
CategoryTheory.Limits.limitRightOpIsoOpColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasColimit F]
:
CategoryTheory.Limits.limit F.rightOp ≅ Opposite.op (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasColimit F]
(j : J)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).inv
(CategoryTheory.Limits.limit.π F.rightOp j) = (CategoryTheory.Limits.colimit.ι F (Opposite.op j)).op
@[simp]
theorem
CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasColimit F]
(j : J)
{Z : Cᵒᵖ}
(h : F.rightOp.obj j ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : Opposite.op (F.obj j) ⟶ Z)
:
def
CategoryTheory.Limits.limitUnopIsoUnopColimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasColimit 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.limitUnopIsoUnopColimit_inv_comp_π_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : J)
{Z : C}
(h : F.unop.obj j ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Limits.limitUnopIsoUnopColimit_hom_comp_ι_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasColimit F]
(j : Jᵒᵖ)
{Z : C}
(h : Opposite.unop (F.obj j) ⟶ Z)
:
theorem
CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
[CategoryTheory.Limits.HasColimitsOfShape Jᵒᵖ C]
:
If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
instance
CategoryTheory.Limits.hasLimits_op_of_hasColimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasColimits C]
:
If C has colimits, we can construct limits for Cᵒᵖ.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit F.op]
:
theorem
CategoryTheory.Limits.hasColimit_of_hasLimit_rightOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasLimit F.rightOp]
:
theorem
CategoryTheory.Limits.hasColimit_of_hasLimit_unop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F.unop]
:
instance
CategoryTheory.Limits.hasColimit_op_of_hasLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit F]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasColimit_leftOp_of_hasLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
:
CategoryTheory.Limits.HasColimit F.leftOp
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasColimit_rightOp_of_hasLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasLimit F]
:
CategoryTheory.Limits.HasColimit F.rightOp
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasColimit_unop_of_hasLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.colimitOpIsoOpLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitOpIsoOpLimit_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : Opposite.op (CategoryTheory.Limits.limit F) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit F]
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit F]
(j : J)
{Z : Cᵒᵖ}
(h : CategoryTheory.Limits.colimit F.op ⟶ Z)
:
def
CategoryTheory.Limits.colimitLeftOpIsoUnopLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasLimit 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.leftOp j)
(CategoryTheory.Limits.colimitLeftOpIsoUnopLimit F).hom = (CategoryTheory.Limits.limit.π F (Opposite.unop j)).unop
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
{Z : C}
(h : Opposite.unop (CategoryTheory.Limits.limit F) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitLeftOpIsoUnopLimit_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor J Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : J)
{Z : C}
(h : CategoryTheory.Limits.colimit F.leftOp ⟶ Z)
:
def
CategoryTheory.Limits.colimitRightOpIsoUnopLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasLimit F]
:
CategoryTheory.Limits.colimit F.rightOp ≅ Opposite.op (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasLimit F]
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitRightOpIsoUnopLimit_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasLimit F]
(j : J)
{Z : Cᵒᵖ}
(h : Opposite.op (CategoryTheory.Limits.limit F) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitRightOpIsoUnopLimit_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ C)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
{Z : Cᵒᵖ}
(h : CategoryTheory.Limits.colimit F.rightOp ⟶ Z)
:
def
CategoryTheory.Limits.colimitUnopIsoOpLimit
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasLimit 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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : J)
:
@[simp]
theorem
CategoryTheory.Limits.ι_comp_colimitUnopIsoOpLimit_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : J)
{Z : C}
(h : Opposite.unop (CategoryTheory.Limits.limit F) ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
:
@[simp]
theorem
CategoryTheory.Limits.π_comp_colimitUnopIsoOpLimit_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
(F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ)
[CategoryTheory.Limits.HasLimit F]
(j : Jᵒᵖ)
{Z : C}
(h : CategoryTheory.Limits.colimit F.unop ⟶ Z)
:
instance
CategoryTheory.Limits.hasColimitsOfShape_op_of_hasLimitsOfShape
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{J : Type u₂}
[CategoryTheory.Category.{v₂, u₂} J]
[CategoryTheory.Limits.HasLimitsOfShape Jᵒᵖ C]
:
If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasColimits_op_of_hasLimits
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasLimits C]
:
If C has limits, we can construct colimits for Cᵒᵖ.
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasCoproductsOfShape_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : Type v₂)
[CategoryTheory.Limits.HasProductsOfShape X C]
:
If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.hasCoproductsOfShape_of_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : Type v₂)
[CategoryTheory.Limits.HasProductsOfShape X Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasProductsOfShape_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : Type v₂)
[CategoryTheory.Limits.HasCoproductsOfShape X C]
:
If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Limits.hasProductsOfShape_of_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(X : Type v₂)
[CategoryTheory.Limits.HasCoproductsOfShape X Cᵒᵖ]
:
instance
CategoryTheory.Limits.hasProducts_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasCoproducts C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasCoproducts_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasProducts C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasFiniteCoproducts_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasFiniteProducts C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasFiniteProducts_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasFiniteCoproducts C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.instHasLimitOppositeDiscreteOpFunctor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasCoproduct Z]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.instHasLimitDiscreteOppositeCompInverseOppositeOpFunctor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasCoproduct Z]
:
CategoryTheory.Limits.HasLimit
((CategoryTheory.Discrete.opposite α).inverse.comp (CategoryTheory.Discrete.functor Z).op)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.instHasProductOppositeOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasCoproduct Z]
:
CategoryTheory.Limits.HasProduct fun (x : α) => Opposite.op (Z x)
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Cofan.op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
(c : CategoryTheory.Limits.Cofan Z)
:
CategoryTheory.Limits.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
def
CategoryTheory.Limits.Cofan.IsColimit.op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : CategoryTheory.Limits.Cofan Z}
(hc : CategoryTheory.Limits.IsColimit c)
:
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : CategoryTheory.Limits.Cofan Z}
{f : CategoryTheory.Limits.Fan fun (x : α) => Opposite.op (Z x)}
(hc : CategoryTheory.Limits.IsColimit c)
(hf : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : CategoryTheory.Limits.Cofan Z}
{f : CategoryTheory.Limits.Fan fun (x : α) => Opposite.op (Z x)}
(hc : CategoryTheory.Limits.IsColimit c)
(hf : CategoryTheory.Limits.IsLimit f)
(b : α)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).inv (c.inj b).op = f.proj b
theorem
CategoryTheory.Limits.opCoproductIsoProduct'_comp_self
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c c' : CategoryTheory.Limits.Cofan Z}
{f : CategoryTheory.Limits.Fan fun (x : α) => Opposite.op (Z x)}
(hc : CategoryTheory.Limits.IsColimit c)
(hc' : CategoryTheory.Limits.IsColimit c')
(hf : CategoryTheory.Limits.IsLimit f)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom
(CategoryTheory.Limits.opCoproductIsoProduct' hc' hf).inv = (hc.coconePointUniqueUpToIso hc').op.inv
theorem
CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[CategoryTheory.Limits.HasCoproduct Z]
(b : α)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opCoproductIsoProduct Z).inv
(CategoryTheory.Limits.Sigma.ι Z b).op = CategoryTheory.Limits.Pi.π (fun (x : α) => Opposite.op (Z x)) b
theorem
CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{c : CategoryTheory.Limits.Cofan Z}
{f : CategoryTheory.Limits.Fan fun (x : α) => Opposite.op (Z x)}
(hc : CategoryTheory.Limits.IsColimit c)
(hf : CategoryTheory.Limits.IsLimit f)
(c' : CategoryTheory.Limits.Cofan Z)
:
CategoryTheory.CategoryStruct.comp (hc.desc c').op (CategoryTheory.Limits.opCoproductIsoProduct' hc hf).hom = hf.lift c'.op
theorem
CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasCoproduct Z]
{X : C}
(π : (a : α) → Z a ⟶ X)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc π).op
(CategoryTheory.Limits.opCoproductIsoProduct Z).hom = CategoryTheory.Limits.Pi.lift fun (a : α) => (π a).op
instance
CategoryTheory.Limits.instHasColimitOppositeDiscreteOpFunctor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasProduct Z]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasProduct Z]
:
CategoryTheory.Limits.HasColimit
((CategoryTheory.Discrete.opposite α).inverse.comp (CategoryTheory.Discrete.functor Z).op)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.instHasCoproductOppositeOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasProduct Z]
:
CategoryTheory.Limits.HasCoproduct fun (x : α) => Opposite.op (Z x)
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.Fan.op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
(f : CategoryTheory.Limits.Fan Z)
:
CategoryTheory.Limits.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
def
CategoryTheory.Limits.Fan.IsLimit.op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : CategoryTheory.Limits.Fan Z}
(hf : CategoryTheory.Limits.IsLimit f)
:
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : CategoryTheory.Limits.Fan Z}
{c : CategoryTheory.Limits.Cofan fun (x : α) => Opposite.op (Z x)}
(hf : CategoryTheory.Limits.IsLimit f)
(hc : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : CategoryTheory.Limits.Fan Z}
{c : CategoryTheory.Limits.Cofan fun (x : α) => Opposite.op (Z x)}
(hf : CategoryTheory.Limits.IsLimit f)
(hc : CategoryTheory.Limits.IsColimit c)
(b : α)
:
CategoryTheory.CategoryStruct.comp (f.proj b).op (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom = c.inj b
theorem
CategoryTheory.Limits.opProductIsoCoproduct'_comp_self
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f f' : CategoryTheory.Limits.Fan Z}
{c : CategoryTheory.Limits.Cofan fun (x : α) => Opposite.op (Z x)}
(hf : CategoryTheory.Limits.IsLimit f)
(hf' : CategoryTheory.Limits.IsLimit f')
(hc : CategoryTheory.Limits.IsColimit c)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).hom
(CategoryTheory.Limits.opProductIsoCoproduct' hf' hc).inv = (hf.conePointUniqueUpToIso hf').op.inv
theorem
CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
(Z : α → C)
[CategoryTheory.Limits.HasProduct Z]
(b : α)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π Z b).op
(CategoryTheory.Limits.opProductIsoCoproduct Z).hom = CategoryTheory.Limits.Sigma.ι (fun (x : α) => Opposite.op (Z x)) b
theorem
CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
{f : CategoryTheory.Limits.Fan Z}
{c : CategoryTheory.Limits.Cofan fun (x : α) => Opposite.op (Z x)}
(hf : CategoryTheory.Limits.IsLimit f)
(hc : CategoryTheory.Limits.IsColimit c)
(f' : CategoryTheory.Limits.Fan Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct' hf hc).inv (hf.lift f').op = hc.desc f'.op
theorem
CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{α : Type u_1}
{Z : α → C}
[CategoryTheory.Limits.HasProduct Z]
{X : C}
(π : (a : α) → X ⟶ Z a)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProductIsoCoproduct Z).inv
(CategoryTheory.Limits.Pi.lift π).op = CategoryTheory.Limits.Sigma.desc fun (a : α) => (π a).op
instance
CategoryTheory.Limits.instHasBinaryCoproductOppositeOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.opProdIsoCoprod
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
(A B : C)
[CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op (CategoryTheory.Limits.opProdIsoCoprod A B).hom = CategoryTheory.Limits.coprod.inl
@[simp]
theorem
CategoryTheory.Limits.fst_opProdIsoCoprod_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op A ⨿ Opposite.op B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h
@[simp]
theorem
CategoryTheory.Limits.snd_opProdIsoCoprod_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd.op (CategoryTheory.Limits.opProdIsoCoprod A B).hom = CategoryTheory.Limits.coprod.inr
@[simp]
theorem
CategoryTheory.Limits.snd_opProdIsoCoprod_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op A ⨿ Opposite.op B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd.op
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr h
@[simp]
theorem
CategoryTheory.Limits.inl_opProdIsoCoprod_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl (CategoryTheory.Limits.opProdIsoCoprod A B).inv = CategoryTheory.Limits.prod.fst.op
@[simp]
theorem
CategoryTheory.Limits.inl_opProdIsoCoprod_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op (A ⨯ B) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst.op h
@[simp]
theorem
CategoryTheory.Limits.inr_opProdIsoCoprod_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr (CategoryTheory.Limits.opProdIsoCoprod A B).inv = CategoryTheory.Limits.prod.snd.op
@[simp]
theorem
CategoryTheory.Limits.inr_opProdIsoCoprod_inv_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : Cᵒᵖ}
(h : Opposite.op (A ⨯ B) ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd.op h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_fst
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.coprod.inl.unop
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_fst_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : C}
(h : A ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl.unop h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_snd
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.coprod.inr.unop
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_hom_snd_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : C}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr.unop h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
CategoryTheory.Limits.coprod.inl.unop = CategoryTheory.Limits.prod.fst
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inl_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : C}
(h : A ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl.unop h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inr
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
CategoryTheory.Limits.coprod.inr.unop = CategoryTheory.Limits.prod.snd
@[simp]
theorem
CategoryTheory.Limits.opProdIsoCoprod_inv_inr_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{A B : C}
[CategoryTheory.Limits.HasBinaryProduct A B]
{Z : C}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr.unop h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h
instance
CategoryTheory.Limits.hasEqualizers_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasCoequalizers C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasCoequalizers_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasEqualizers C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasFiniteColimits_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasFiniteLimits C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasFiniteLimits_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasFiniteColimits C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPullbacks_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPushouts C]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.Limits.hasPushouts_opposite
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasPullbacks C]
:
Equations
- ⋯ = ⋯
def
CategoryTheory.Limits.spanOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
CategoryTheory.Limits.span f.op g.op ≅ CategoryTheory.Limits.walkingCospanOpEquiv.inverse.comp (CategoryTheory.Limits.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_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingSpan)
:
(CategoryTheory.Limits.spanOp f g).inv.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X))
(CategoryTheory.Iso.refl (Opposite.op Y)) val)
X✝).inv
@[simp]
theorem
CategoryTheory.Limits.spanOp_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingSpan)
:
(CategoryTheory.Limits.spanOp f g).hom.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X))
(CategoryTheory.Iso.refl (Opposite.op Y)) val)
X✝).hom
def
CategoryTheory.Limits.opCospan
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
:
(CategoryTheory.Limits.cospan f g).op ≅ CategoryTheory.Limits.walkingCospanOpEquiv.functor.comp (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingCospanᵒᵖ)
:
(CategoryTheory.Limits.opCospan f g).inv.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X))
(CategoryTheory.Iso.refl (Opposite.op Y)) val)
(Opposite.unop X✝)).hom
@[simp]
theorem
CategoryTheory.Limits.opCospan_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingCospanᵒᵖ)
:
(CategoryTheory.Limits.opCospan f g).hom.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op Z))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X))
(CategoryTheory.Iso.refl (Opposite.op Y)) val)
(Opposite.unop X✝)).inv
def
CategoryTheory.Limits.cospanOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
CategoryTheory.Limits.cospan f.op g.op ≅ CategoryTheory.Limits.walkingSpanOpEquiv.inverse.comp (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingCospan)
:
(CategoryTheory.Limits.cospanOp f g).inv.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y))
(CategoryTheory.Iso.refl (Opposite.op Z)) val)
X✝).inv
@[simp]
theorem
CategoryTheory.Limits.cospanOp_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingCospan)
:
(CategoryTheory.Limits.cospanOp f g).hom.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y))
(CategoryTheory.Iso.refl (Opposite.op Z)) val)
X✝).hom
def
CategoryTheory.Limits.opSpan
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
:
(CategoryTheory.Limits.span f g).op ≅ CategoryTheory.Limits.walkingSpanOpEquiv.functor.comp (CategoryTheory.Limits.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_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingSpanᵒᵖ)
:
(CategoryTheory.Limits.opSpan f g).inv.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y))
(CategoryTheory.Iso.refl (Opposite.op Z)) val)
(Opposite.unop X✝)).hom
@[simp]
theorem
CategoryTheory.Limits.opSpan_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Y)
(g : X ⟶ Z)
(X✝ : CategoryTheory.Limits.WalkingSpanᵒᵖ)
:
(CategoryTheory.Limits.opSpan f g).hom.app X✝ = (Option.rec (CategoryTheory.Iso.refl (Opposite.op X))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y))
(CategoryTheory.Iso.refl (Opposite.op Z)) val)
(Opposite.unop X✝)).inv
def
CategoryTheory.Limits.PushoutCocone.unop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
CategoryTheory.Limits.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_pt
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
c.unop.pt = Opposite.unop c.pt
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.unop_π_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
(X✝ : CategoryTheory.Limits.WalkingCospan)
:
c.unop.π.app X✝ = CategoryTheory.CategoryStruct.comp (c.ι.app X✝).unop
(Option.rec (CategoryTheory.Iso.refl X)
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl Y) (CategoryTheory.Iso.refl Z) val)
X✝).inv.unop
theorem
CategoryTheory.Limits.PushoutCocone.unop_fst
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
c.unop.fst = c.inl.unop
theorem
CategoryTheory.Limits.PushoutCocone.unop_snd
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
c.unop.snd = c.inr.unop
def
CategoryTheory.Limits.PushoutCocone.op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
CategoryTheory.Limits.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_π_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
(X✝ : CategoryTheory.Limits.WalkingCospan)
:
c.op.π.app X✝ = CategoryTheory.CategoryStruct.comp (c.ι.app X✝).op
(Option.rec (CategoryTheory.Iso.refl (Opposite.op X))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op Y))
(CategoryTheory.Iso.refl (Opposite.op Z)) val)
X✝).inv
@[simp]
theorem
CategoryTheory.Limits.PushoutCocone.op_pt
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
c.op.pt = Opposite.op c.pt
theorem
CategoryTheory.Limits.PushoutCocone.op_fst
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
c.op.fst = c.inl.op
theorem
CategoryTheory.Limits.PushoutCocone.op_snd
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.PushoutCocone f g)
:
c.op.snd = c.inr.op
def
CategoryTheory.Limits.PullbackCone.unop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
CategoryTheory.Limits.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_pt
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
c.unop.pt = Opposite.unop c.pt
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.unop_ι_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
(X✝ : CategoryTheory.Limits.WalkingSpan)
:
c.unop.ι.app X✝ = CategoryTheory.CategoryStruct.comp
(Option.rec (CategoryTheory.Iso.refl Z)
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl X) (CategoryTheory.Iso.refl Y) val)
X✝).hom.unop
(c.π.app X✝).unop
theorem
CategoryTheory.Limits.PullbackCone.unop_inl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
c.unop.inl = c.fst.unop
theorem
CategoryTheory.Limits.PullbackCone.unop_inr
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
c.unop.inr = c.snd.unop
def
CategoryTheory.Limits.PullbackCone.op
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
CategoryTheory.Limits.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_ι_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
(X✝ : CategoryTheory.Limits.WalkingSpan)
:
c.op.ι.app X✝ = CategoryTheory.CategoryStruct.comp
(Option.rec (CategoryTheory.Iso.refl (Opposite.op Z))
(fun (val : CategoryTheory.Limits.WalkingPair) =>
CategoryTheory.Limits.WalkingPair.rec (CategoryTheory.Iso.refl (Opposite.op X))
(CategoryTheory.Iso.refl (Opposite.op Y)) val)
X✝).hom
(c.π.app X✝).op
@[simp]
theorem
CategoryTheory.Limits.PullbackCone.op_pt
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
c.op.pt = Opposite.op c.pt
theorem
CategoryTheory.Limits.PullbackCone.op_inl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
c.op.inl = c.fst.op
theorem
CategoryTheory.Limits.PullbackCone.op_inr
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.PullbackCone f g)
:
c.op.inr = c.snd.op
def
CategoryTheory.Limits.PullbackCone.opUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.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
def
CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.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
def
CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Y}
{g : X ⟶ Z}
(c : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : Cᵒᵖ}
{f : X ⟶ Z}
{g : Y ⟶ Z}
(c : CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[h : CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
:
CategoryTheory.Limits.pullback f g ≅ Opposite.unop (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv
(CategoryTheory.Limits.pullback.fst f g) = (CategoryTheory.Limits.pushout.inl f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
{Z✝ : C}
(h : X ⟶ Z✝)
:
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv
(CategoryTheory.Limits.pullback.snd f g) = (CategoryTheory.Limits.pushout.inr f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
{Z✝ : C}
(h : Y ⟶ Z✝)
:
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f.op g.op)
(CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op = (CategoryTheory.Limits.pullback.fst f g).op
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
{Z✝ : Cᵒᵖ}
(h : Opposite.op (CategoryTheory.Limits.pullback f g) ⟶ Z✝)
:
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f.op g.op)
(CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op = (CategoryTheory.Limits.pullback.snd f g).op
@[simp]
theorem
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
[CategoryTheory.Limits.HasPullback f g]
[CategoryTheory.Limits.HasPushout f.op g.op]
{Z✝ : Cᵒᵖ}
(h : Opposite.op (CategoryTheory.Limits.pullback f g) ⟶ Z✝)
:
noncomputable def
CategoryTheory.Limits.pushoutIsoUnopPullback
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[h : CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPullback f.op g.op]
:
CategoryTheory.Limits.pushout f g ≅ Opposite.unop (CategoryTheory.Limits.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPullback f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl f g)
(CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom = (CategoryTheory.Limits.pullback.fst f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPullback f.op g.op]
{Z✝ : C}
(h : Opposite.unop (CategoryTheory.Limits.pullback f.op g.op) ⟶ Z✝)
:
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPullback f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f g)
(CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom = (CategoryTheory.Limits.pullback.snd f.op g.op).unop
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom_assoc
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPullback f.op g.op]
{Z✝ : C}
(h : Opposite.unop (CategoryTheory.Limits.pullback f.op g.op) ⟶ Z✝)
:
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPullback f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op
(CategoryTheory.Limits.pullback.fst f.op g.op) = (CategoryTheory.Limits.pushout.inl f g).op
@[simp]
theorem
CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{X Y Z : C}
(f : X ⟶ Z)
(g : X ⟶ Y)
[CategoryTheory.Limits.HasPushout f g]
[CategoryTheory.Limits.HasPullback f.op g.op]
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op
(CategoryTheory.Limits.pullback.snd f.op g.op) = (CategoryTheory.Limits.pushout.inr f g).op
def
CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Q : C}
(p : Y ⟶ Q)
{f : X ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp f p = 0)
(h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p w))
:
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{X Y Q : Cᵒᵖ}
(p : Y ⟶ Q)
{f : X ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp f p = 0)
(h : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ p w))
:
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K X Y : C}
(i : K ⟶ X)
{f : X ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp i f = 0)
(h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w))
:
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
[CategoryTheory.Limits.HasZeroMorphisms C]
{K X Y : Cᵒᵖ}
(i : K ⟶ X)
{f : X ⟶ Y}
(w : CategoryTheory.CategoryStruct.comp i f = 0)
(h : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι i w))
:
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.