Skip to content

Commit

Permalink
chore: remove duplicates of IsLimit.op and variants (#11683)
Browse files Browse the repository at this point in the history
  • Loading branch information
@TwoFX
TwoFX committed Mar 26, 2024
1 parent 3fea5dc commit d587641
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 56 deletions.
71 changes: 19 additions & 52 deletions Mathlib/CategoryTheory/Limits/Opposites.lean
View file
Expand Up @@ -34,27 +34,16 @@ namespace CategoryTheory.Limits
variable {C : Type u₁} [Category.{v₁} C]
variable {J : Type u₂} [Category.{v₂} J]

/-- Turn a colimit for `F : J ⥤ C` into a limit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def isLimitCoconeOp (F : J ⥤ C) {c : Cocone F} (hc : IsColimit c) : IsLimit c.op
where
lift s := (hc.desc s.unop).op
fac s j := Quiver.Hom.unop_inj (by simp)
uniq s m w := by
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
simpa only [Quiver.Hom.unop_op, IsColimit.fac] using w (op j)
#align category_theory.limits.is_limit_cocone_op CategoryTheory.Limits.isLimitCoconeOp
#align category_theory.limits.is_limit_cocone_op CategoryTheory.Limits.IsColimit.op
#align category_theory.limits.is_colimit_cone_op CategoryTheory.Limits.IsLimit.op
#align category_theory.limits.is_limit_cocone_unop CategoryTheory.Limits.IsColimit.unop
#align category_theory.limits.is_colimit_cone_unop CategoryTheory.Limits.IsLimit.unop

/-- Turn a limit for `F : J ⥤ C` into a colimit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ`. -/
@[simps]
def isColimitConeOp (F : J ⥤ C) {c : Cone F} (hc : IsLimit c) : IsColimit c.op
where
desc s := (hc.lift s.unop).op
fac s j := Quiver.Hom.unop_inj (by simp)
uniq s m w := by
refine' Quiver.Hom.unop_inj (hc.hom_ext fun j => Quiver.Hom.op_inj _)
simpa only [Quiver.Hom.unop_op, IsLimit.fac] using w (op j)
#align category_theory.limits.is_colimit_cone_op CategoryTheory.Limits.isColimitConeOp
-- 2024-03-26
@[deprecated] alias isLimitCoconeOp := IsColimit.op
@[deprecated] alias isColimitConeOp := IsLimit.op
@[deprecated] alias isLimitCoconeUnop := IsColimit.unop
@[deprecated] alias isColimitConeUnop := IsLimit.unop

/-- Turn a colimit for `F : J ⥤ Cᵒᵖ` into a limit for `F.leftOp : Jᵒᵖ ⥤ C`. -/
@[simps]
Expand Down Expand Up @@ -134,28 +123,6 @@ def isColimitCoconeUnopOfCone (F : Jᵒᵖ ⥤ Cᵒᵖ) {c : Cone F} (hc : IsLim
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using w (unop j)
#align category_theory.limits.is_colimit_cocone_unop_of_cone CategoryTheory.Limits.isColimitCoconeUnopOfCone

/-- Turn a colimit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ` into a limit for `F : J ⥤ C`. -/
@[simps]
def isLimitCoconeUnop (F : J ⥤ C) {c : Cocone F.op} (hc : IsColimit c) : IsLimit c.unop
where
lift s := (hc.desc s.op).unop
fac s j := Quiver.Hom.op_inj (by simp)
uniq s m w := by
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
simpa only [Quiver.Hom.op_unop, IsColimit.fac] using w (unop j)
#align category_theory.limits.is_limit_cocone_unop CategoryTheory.Limits.isLimitCoconeUnop

/-- Turn a limit for `F.op : Jᵒᵖ ⥤ Cᵒᵖ` into a colimit for `F : J ⥤ C`. -/
@[simps]
def isColimitConeUnop (F : J ⥤ C) {c : Cone F.op} (hc : IsLimit c) : IsColimit c.unop
where
desc s := (hc.lift s.op).unop
fac s j := Quiver.Hom.op_inj (by simp)
uniq s m w := by
refine' Quiver.Hom.op_inj (hc.hom_ext fun j => Quiver.Hom.unop_inj _)
simpa only [Quiver.Hom.op_unop, IsLimit.fac] using w (unop j)
#align category_theory.limits.is_colimit_cone_unop CategoryTheory.Limits.isColimitConeUnop

/-- Turn a colimit for `F.leftOp : Jᵒᵖ ⥤ C` into a limit for `F : J ⥤ Cᵒᵖ`. -/
@[simps]
def isLimitConeOfCoconeLeftOp (F : J ⥤ Cᵒᵖ) {c : Cocone F.leftOp} (hc : IsColimit c) :
Expand Down Expand Up @@ -245,12 +212,12 @@ theorem hasLimit_of_hasColimit_leftOp (F : J ⥤ Cᵒᵖ) [HasColimit F.leftOp]
theorem hasLimit_of_hasColimit_op (F : J ⥤ C) [HasColimit F.op] : HasLimit F :=
HasLimit.mk
{ cone := (colimit.cocone F.op).unop
isLimit := isLimitCoconeUnop _ (colimit.isColimit _) }
isLimit := (colimit.isColimit _).unop }

theorem hasLimit_op_of_hasColimit (F : J ⥤ C) [HasColimit F] : HasLimit F.op :=
HasLimit.mk
{ cone := (colimit.cocone F).op
isLimit := isLimitCoconeOp _ (colimit.isColimit _) }
isLimit := (colimit.isColimit _).op }
#align category_theory.limits.has_limit_of_has_colimit_op CategoryTheory.Limits.hasLimit_of_hasColimit_op

/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
Expand Down Expand Up @@ -298,13 +265,13 @@ theorem hasColimit_of_hasLimit_leftOp (F : J ⥤ Cᵒᵖ) [HasLimit F.leftOp] :
theorem hasColimit_of_hasLimit_op (F : J ⥤ C) [HasLimit F.op] : HasColimit F :=
HasColimit.mk
{ cocone := (limit.cone F.op).unop
isColimit := isColimitConeUnop _ (limit.isLimit _) }
isColimit := (limit.isLimit _).unop }
#align category_theory.limits.has_colimit_of_has_limit_op CategoryTheory.Limits.hasColimit_of_hasLimit_op

theorem hasColimit_op_of_hasLimit (F : J ⥤ C) [HasLimit F] : HasColimit F.op :=
HasColimit.mk
{ cocone := (limit.cone F).op
isColimit := isColimitConeOp _ (limit.isLimit _) }
isColimit := (limit.isLimit _).op }

/-- If `C` has colimits of shape `Jᵒᵖ`, we can construct limits in `Cᵒᵖ` of shape `J`.
-/
Expand Down Expand Up @@ -732,11 +699,11 @@ def isColimitEquivIsLimitOp {X Y Z : C} {f : X ⟶ Y} {g : X ⟶ Z} (c : Pushout
apply equivOfSubsingletonOfSubsingleton
· intro h
exact (IsLimit.postcomposeHomEquiv _ _).invFun
((IsLimit.whiskerEquivalenceEquiv walkingSpanOpEquiv.symm).toFun (isLimitCoconeOp _ h))
((IsLimit.whiskerEquivalenceEquiv walkingSpanOpEquiv.symm).toFun h.op)
· intro h
exact (IsColimit.equivIsoColimit c.opUnop).toFun
(isColimitConeUnop _ ((IsLimit.postcomposeHomEquiv _ _).invFun
((IsLimit.whiskerEquivalenceEquiv _).toFun h)))
(((IsLimit.postcomposeHomEquiv _ _).invFun
((IsLimit.whiskerEquivalenceEquiv _).toFun h)).unop)
#align category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_op CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp

/-- A pushout cone is a colimit cocone in `Cᵒᵖ` if and only if the corresponding pullback cone
Expand All @@ -745,12 +712,12 @@ def isColimitEquivIsLimitUnop {X Y Z : Cᵒᵖ} {f : X ⟶ Y} {g : X ⟶ Z} (c :
IsColimit c ≃ IsLimit c.unop := by
apply equivOfSubsingletonOfSubsingleton
· intro h
exact isLimitCoconeUnop _ ((IsColimit.precomposeHomEquiv _ _).invFun
((IsColimit.whiskerEquivalenceEquiv _).toFun h))
exact ((IsColimit.precomposeHomEquiv _ _).invFun
((IsColimit.whiskerEquivalenceEquiv _).toFun h)).unop
· intro h
exact (IsColimit.equivIsoColimit c.unopOp).toFun
((IsColimit.precomposeHomEquiv _ _).invFun
((IsColimit.whiskerEquivalenceEquiv walkingCospanOpEquiv.symm).toFun (isColimitConeOp _ h)))
((IsColimit.whiskerEquivalenceEquiv walkingCospanOpEquiv.symm).toFun h.op))
#align category_theory.limits.pushout_cocone.is_colimit_equiv_is_limit_unop CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop

end PushoutCocone
Expand Down
8 changes: 4 additions & 4 deletions Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
View file
Expand Up @@ -56,15 +56,15 @@ def preservesLimitLeftOp (K : J ⥤ Cᵒᵖ) (F : C ⥤ Dᵒᵖ) [PreservesColim
def preservesLimitRightOp (K : J ⥤ C) (F : Cᵒᵖ ⥤ D) [PreservesColimit K.op F] :
PreservesLimit K F.rightOp where
preserves {_} hc :=
isLimitConeRightOpOfCocone _ (isColimitOfPreserves F (isColimitConeOp _ hc))
isLimitConeRightOpOfCocone _ (isColimitOfPreserves F hc.op)
#align category_theory.limits.preserves_limit_right_op CategoryTheory.Limits.preservesLimitRightOp

/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves colimits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` preserves
limits of `K : J ⥤ C`. -/
def preservesLimitUnop (K : J ⥤ C) (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesColimit K.op F] :
PreservesLimit K F.unop where
preserves {_} hc :=
isLimitConeUnopOfCocone _ (isColimitOfPreserves F (isColimitConeOp _ hc))
isLimitConeUnopOfCocone _ (isColimitOfPreserves F hc.op)
#align category_theory.limits.preserves_limit_unop CategoryTheory.Limits.preservesLimitUnop

/-- If `F : C ⥤ D` preserves limits of `K.left_op : Jᵒᵖ ⥤ C`, then `F.op : Cᵒᵖ ⥤ Dᵒᵖ` preserves
Expand All @@ -88,15 +88,15 @@ def preservesColimitLeftOp (K : J ⥤ Cᵒᵖ) (F : C ⥤ Dᵒᵖ) [PreservesLim
def preservesColimitRightOp (K : J ⥤ C) (F : Cᵒᵖ ⥤ D) [PreservesLimit K.op F] :
PreservesColimit K F.rightOp where
preserves {_} hc :=
isColimitCoconeRightOpOfCone _ (isLimitOfPreserves F (isLimitCoconeOp _ hc))
isColimitCoconeRightOpOfCone _ (isLimitOfPreserves F hc.op)
#align category_theory.limits.preserves_colimit_right_op CategoryTheory.Limits.preservesColimitRightOp

/-- If `F : Cᵒᵖ ⥤ Dᵒᵖ` preserves limits of `K.op : Jᵒᵖ ⥤ Cᵒᵖ`, then `F.unop : C ⥤ D` preserves
colimits of `K : J ⥤ C`. -/
def preservesColimitUnop (K : J ⥤ C) (F : Cᵒᵖ ⥤ Dᵒᵖ) [PreservesLimit K.op F] :
PreservesColimit K F.unop where
preserves {_} hc :=
isColimitCoconeUnopOfCone _ (isLimitOfPreserves F (isLimitCoconeOp _ hc))
isColimitCoconeUnopOfCone _ (isLimitOfPreserves F hc.op)
#align category_theory.limits.preserves_colimit_unop CategoryTheory.Limits.preservesColimitUnop

section
Expand Down

0 comments on commit d587641

Please sign in to comment.