From 4d9990b3925435087a7e0530a4a1e84d7746c3e4 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <jakob@von-raumer.de>
Date: Fri, 25 Oct 2024 22:10:03 +0000
Subject: [PATCH] feat(CategoryTheory/Limits/Final): Add pointfree version of
 `Final.colimitIso` (#17902)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Co-authored-by: Joël Riou <joel.riou@universite-paris-saclay.fr>
---
 Mathlib/CategoryTheory/Limits/Final.lean | 59 +++++++++---------------
 1 file changed, 23 insertions(+), 36 deletions(-)

diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean
index 8dea5b13733db..6390aaa372617 100644
--- a/Mathlib/CategoryTheory/Limits/Final.lean
+++ b/Mathlib/CategoryTheory/Limits/Final.lean
@@ -319,9 +319,21 @@ variable (G)
 
 https://stacks.math.columbia.edu/tag/04E7
 -/
+@[simps! (config := .lemmasOnly)]
 def colimitIso [HasColimit G] : colimit (F ⋙ G) ≅ colimit G :=
   asIso (colimit.pre G F)
 
+/-- A pointfree version of `colimitIso`, stating that whiskering by `F` followed by taking the
+colimit is isomorpic to taking the colimit on the codomain of `F`. -/
+def colimIso [HasColimitsOfShape D E] [HasColimitsOfShape C E] :
+    (whiskeringLeft _ _ _).obj F ⋙ colim ≅ colim (J := D) (C := E) :=
+  NatIso.ofComponents (fun G => colimitIso F G) fun f => by
+    simp only [comp_obj, whiskeringLeft_obj_obj, colim_obj, comp_map, whiskeringLeft_obj_map,
+      colim_map, colimitIso_hom]
+    ext
+    simp only [comp_obj, ι_colimMap_assoc, whiskerLeft_app, colimit.ι_pre, colimit.ι_pre_assoc,
+      ι_colimMap]
+
 end
 
 /-- Given a colimit cocone over `F ⋙ G` we can construct a colimit cocone over `G`. -/
@@ -342,24 +354,6 @@ include F in
 theorem hasColimitsOfShape_of_final [HasColimitsOfShape C E] : HasColimitsOfShape D E where
   has_colimit := fun _ => hasColimit_of_comp F
 
-section
-
--- Porting note: this instance does not seem to be found automatically
---attribute [local instance] hasColimit_of_comp
-
-/-- When `F` is final, and `F ⋙ G` has a colimit, then `G` has a colimit also and
-`colimit (F ⋙ G) ≅ colimit G`
-
-https://stacks.math.columbia.edu/tag/04E7
--/
-def colimitIso' [HasColimit (F ⋙ G)] :
-    haveI : HasColimit G := hasColimit_of_comp F
-    colimit (F ⋙ G) ≅ colimit G :=
-  haveI : HasColimit G := hasColimit_of_comp F
-  asIso (colimit.pre G F)
-
-end
-
 end Final
 
 end ArbitraryUniverse
@@ -602,9 +596,20 @@ variable (G)
 
 https://stacks.math.columbia.edu/tag/04E7
 -/
+@[simps! (config := .lemmasOnly)]
 def limitIso [HasLimit G] : limit (F ⋙ G) ≅ limit G :=
   (asIso (limit.pre G F)).symm
 
+/-- A pointfree version of `limitIso`, stating that whiskering by `F` followed by taking the
+limit is isomorpic to taking the limit on the codomain of `F`. -/
+def limIso [HasLimitsOfShape D E] [HasLimitsOfShape C E] :
+    (whiskeringLeft _ _ _).obj F ⋙ lim ≅ lim (J := D) (C := E) :=
+  Iso.symm <| NatIso.ofComponents (fun G => (limitIso F G).symm) fun f => by
+    simp only [comp_obj, whiskeringLeft_obj_obj, lim_obj, comp_map, whiskeringLeft_obj_map, lim_map,
+      Iso.symm_hom, limitIso_inv]
+    ext
+    simp
+
 end
 
 /-- Given a limit cone over `F ⋙ G` we can construct a limit cone over `G`. -/
@@ -625,24 +630,6 @@ include F in
 theorem hasLimitsOfShape_of_initial [HasLimitsOfShape C E] : HasLimitsOfShape D E where
   has_limit := fun _ => hasLimit_of_comp F
 
-section
-
--- Porting note: this instance does not seem to be found automatically
--- attribute [local instance] hasLimit_of_comp
-
-/-- When `F` is initial, and `F ⋙ G` has a limit, then `G` has a limit also and
-`limit (F ⋙ G) ≅ limit G`
-
-https://stacks.math.columbia.edu/tag/04E7
--/
-def limitIso' [HasLimit (F ⋙ G)] :
-    haveI : HasLimit G := hasLimit_of_comp F
-    limit (F ⋙ G) ≅ limit G :=
-  haveI : HasLimit G := hasLimit_of_comp F
-  (asIso (limit.pre G F)).symm
-
-end
-
 end Initial
 
 section