Skip to content

[Merged by Bors] - chore(CategoryTheory/Limits): functoriality of coconeLeftOpOfCone and co #36918

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
chrisflav wants to merge 1 commit into from
+70 −0
Closed

[Merged by Bors] - chore(CategoryTheory/Limits): functoriality of coconeLeftOpOfCone and co #36918

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
70 changes: 70 additions & 0 deletions Mathlib/CategoryTheory/Limits/Cones.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -975,6 +975,16 @@ def coconeEquivalenceOpConeOp : Cocone F ≌ (Cone F.op)ᵒᵖ where

attribute [simps] coconeEquivalenceOpConeOp

/-- Cones on `F : J ⥤ C` are equivalent to cocones on `F.op : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def coneOpEquiv {F : J ⥤ C} : (Cone F)ᵒᵖ ≌ Cocone F.op where
Copy link
Copy Markdown
Contributor

@JovanGerb JovanGerb Mar 23, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hey, I noticed that coneOpEquiv is essentially the same as (the dual of) coconeEquivalenceOpConeOp. Do we really need both? And can the names be made more similar?

Copy link
Copy Markdown
Member Author

@chrisflav chrisflav Mar 24, 2026

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes we need both because F.op.op is sadly not def-eq to F :) I agree that the names should be more similar and the statements aligned (adapting the style of coneOpEquiv).

functor.obj c := c.unop.op
functor.map f := { hom := f.unop.hom.op, w j := congr($(f.unop.w j.unop).op) }
inverse.obj c := .op <| c.unop
inverse.map f := ⟨{ hom := f.hom.unop, w j := congr($(f.w (.op j)).unop) }⟩
unitIso := Iso.refl _
counitIso := Iso.refl _

end

section
Expand Down Expand Up @@ -1005,6 +1015,26 @@ def coneLeftOpOfCocone (c : Cocone F) : Cone F.leftOp where
pt := unop c.pt
π := NatTrans.leftOp c.ι

/-- Cones on `F : J ⥤ Cᵒᵖ` are equivalent to cocones on `F.leftOp : Jᵒᵖ ⥤ C`. -/
@[simps]
def coconeLeftOpOfConeEquiv {F : J ⥤ Cᵒᵖ} : (Cone F)ᵒᵖ ≌ Cocone F.leftOp where
functor.obj c := coconeLeftOpOfCone c.unop
functor.map f := { hom := f.unop.hom.unop, w j := congr($(f.unop.w j.unop).unop) }
inverse.obj c := .op <| coneOfCoconeLeftOp c
inverse.map f := ⟨{ hom := f.hom.op, w j := congr($(f.w (.op j)).op) }⟩
unitIso := Iso.refl _
counitIso := Iso.refl _

/-- Cocones on `F : J ⥤ Cᵒᵖ` are equivalent to cones on `F.leftOp : Jᵒᵖ ⥤ C`. -/
@[simps]
def coneLeftOpOfCoconeEquiv {F : J ⥤ Cᵒᵖ} : (Cocone F)ᵒᵖ ≌ Cone F.leftOp where
functor.obj c := coneLeftOpOfCocone c.unop
functor.map f := { hom := f.unop.hom.unop, w j := congr($(f.unop.w j.unop).unop) }
inverse.obj c := .op <| coconeOfConeLeftOp c
inverse.map f := ⟨{ hom := f.hom.op, w j := congr($(f.w (.op j)).op) }⟩
unitIso := Iso.refl _
counitIso := Iso.refl _

end

section
Expand Down Expand Up @@ -1035,6 +1065,26 @@ def coneRightOpOfCocone (c : Cocone F) : Cone F.rightOp where
pt := op c.pt
π := NatTrans.rightOp c.ι

/-- Cones on `F : Jᵒᵖ ⥤ C` are equivalent to cocones on `F.rightOp : J ⥤ Cᵒᵖ`. -/
@[simps]
def coconeRightOpOfConeEquiv {F : Jᵒᵖ ⥤ C} : (Cone F)ᵒᵖ ≌ Cocone F.rightOp where
functor.obj c := coconeRightOpOfCone c.unop
functor.map f := { hom := f.unop.hom.op, w j := congr($(f.unop.w (.op j)).op) }
inverse.obj c := .op <| coneOfCoconeRightOp c
inverse.map f := ⟨{ hom := f.hom.unop, w j := congr($(f.w j.unop).unop) }⟩
unitIso := Iso.refl _
counitIso := Iso.refl _

/-- Cocones on `F : Jᵒᵖ ⥤ C` are equivalent to cones on `F.rightOp : J ⥤ Cᵒᵖ`. -/
@[simps]
def coneRightOpOfCoconeEquiv {F : Jᵒᵖ ⥤ C} : (Cocone F)ᵒᵖ ≌ Cone F.rightOp where
functor.obj c := coneRightOpOfCocone c.unop
functor.map f := { hom := f.unop.hom.op, w j := congr($(f.unop.w (.op j)).op) }
inverse.obj c := .op <| coconeOfConeRightOp c
inverse.map f := ⟨{ hom := f.hom.unop, w j := congr($(f.w j.unop).unop) }⟩
unitIso := Iso.refl _
counitIso := Iso.refl _

end

section
Expand Down Expand Up @@ -1065,6 +1115,26 @@ def coneUnopOfCocone (c : Cocone F) : Cone F.unop where
pt := unop c.pt
π := NatTrans.unop c.ι

/-- Cones on `F : Jᵒᵖ ⥤ Cᵒᵖ` are equivalent to cocones on `F.unop : J ⥤ C`. -/
@[simps]
def coconeUnopOfConeEquiv {F : Jᵒᵖ ⥤ Cᵒᵖ} : (Cone F)ᵒᵖ ≌ Cocone F.unop where
functor.obj c := coconeUnopOfCone c.unop
functor.map f := { hom := f.unop.hom.unop, w j := congr($(f.unop.w (.op j)).unop) }
inverse.obj c := .op <| coneOfCoconeUnop c
inverse.map f := ⟨{ hom := f.hom.op, w j := congr($(f.w j.unop).op) }⟩
unitIso := Iso.refl _
counitIso := Iso.refl _

/-- Cocones on `F : Jᵒᵖ ⥤ Cᵒᵖ` are equivalent to cones on `F.unop : J ⥤ C`. -/
@[simps]
def coneUnopOfCoconeEquiv {F : Jᵒᵖ ⥤ Cᵒᵖ} : (Cocone F)ᵒᵖ ≌ Cone F.unop where
functor.obj c := coneUnopOfCocone c.unop
functor.map f := { hom := f.unop.hom.unop, w j := congr($(f.unop.w (.op j)).unop) }
inverse.obj c := .op <| coconeOfConeUnop c
inverse.map f := ⟨{ hom := f.hom.op, w j := congr($(f.w j.unop).op) }⟩
unitIso := Iso.refl _
counitIso := Iso.refl _

end

end CategoryTheory.Limits
Expand Down
Loading