feat: turn a cocone into a functor to costructured arrows (#6369)

After making this PR I noticed that this already existed in `Functor/Flat.lean`, so I unified the two developments.

Mathlib/CategoryTheory/Functor/Flat.lean

@@ -3,6 +3,7 @@ Copyright (c) 2021 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
+import Mathlib.CategoryTheory.Limits.ConeCategory
 import Mathlib.CategoryTheory.Limits.FilteredColimitCommutesFiniteLimit
 import Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory
 import Mathlib.CategoryTheory.Limits.Bicones
@@ -51,43 +52,6 @@ open Opposite
 
 namespace CategoryTheory
 
-namespace StructuredArrowCone
-
-open StructuredArrow
-
-variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₁} D]
-
-variable {J : Type w} [SmallCategory J]
-
-variable {K : J ⥤ C} (F : C ⥤ D) (c : Cone K)
-
-/-- Given a cone `c : cone K` and a map `f : X ⟶ c.X`, we can construct a cone of structured
-arrows over `X` with `f` as the cone point. This is the underlying diagram.
--/
-@[simps]
-def toDiagram : J ⥤ StructuredArrow c.pt K where
-  obj j := StructuredArrow.mk (c.π.app j)
-  map g := StructuredArrow.homMk g
-#align category_theory.structured_arrow_cone.to_diagram CategoryTheory.StructuredArrowCone.toDiagram
-
-/-- Given a diagram of `structured_arrow X F`s, we may obtain a cone with cone point `X`. -/
-@[simps!]
-def diagramToCone {X : D} (G : J ⥤ StructuredArrow X F) : Cone (G ⋙ proj X F ⋙ F) where
-  π := { app := fun j => (G.obj j).hom }
-#align category_theory.structured_arrow_cone.diagram_to_cone CategoryTheory.StructuredArrowCone.diagramToCone
-
-/-- Given a cone `c : cone K` and a map `f : X ⟶ F.obj c.X`, we can construct a cone of structured
-arrows over `X` with `f` as the cone point.
--/
-@[simps]
-def toCone {X : D} (f : X ⟶ F.obj c.pt) :
-    Cone (toDiagram (F.mapCone c) ⋙ map f ⋙ pre _ K F) where
-  pt := mk f
-  π := { app := fun j => homMk (c.π.app j) rfl }
-#align category_theory.structured_arrow_cone.to_cone CategoryTheory.StructuredArrowCone.toCone
-
-end StructuredArrowCone
-
 section RepresentablyFlat
 
 variable {C : Type u₁} [Category.{v₁} C] {D : Type u₂} [Category.{v₂} D]
@@ -197,8 +161,6 @@ namespace PreservesFiniteLimitsOfFlat
 
 open StructuredArrow
 
-open StructuredArrowCone
-
 variable {J : Type v₁} [SmallCategory J] [FinCategory J] {K : J ⥤ C}
 
 variable (F : C ⥤ D) [RepresentablyFlat F] {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
@@ -208,12 +170,13 @@ Given a limit cone `c : cone K` and a cone `s : cone (K ⋙ F)` with `F` represe
 `s` can factor through `F.map_cone c`.
 -/
 noncomputable def lift : s.pt ⟶ F.obj c.pt :=
-  let s' := IsCofiltered.cone (toDiagram s ⋙ StructuredArrow.pre _ K F)
+  let s' := IsCofiltered.cone (s.toStructuredArrow ⋙ StructuredArrow.pre _ K F)
   s'.pt.hom ≫
     (F.map <|
       hc.lift <|
         (Cones.postcompose
-              ({ app := fun X => 𝟙 _ } : (toDiagram s ⋙ pre s.pt K F) ⋙ proj s.pt F ⟶ K)).obj <|
+              ({ app := fun X => 𝟙 _ } :
+                (s.toStructuredArrow ⋙ pre s.pt K F) ⋙ proj s.pt F ⟶ K)).obj <|
           (StructuredArrow.proj s.pt F).mapCone s')
 #align category_theory.preserves_finite_limits_of_flat.lift CategoryTheory.PreservesFiniteLimitsOfFlat.lift
 
@@ -227,7 +190,7 @@ theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
     (f₁ f₂ : s.pt ⟶ F.obj c.pt) (h₁ : ∀ j : J, f₁ ≫ (F.mapCone c).π.app j = s.π.app j)
     (h₂ : ∀ j : J, f₂ ≫ (F.mapCone c).π.app j = s.π.app j) : f₁ = f₂ := by
   -- We can make two cones over the diagram of `s` via `f₁` and `f₂`.
-  let α₁ : toDiagram (F.mapCone c) ⋙ map f₁ ⟶ toDiagram s :=
+  let α₁ : (F.mapCone c).toStructuredArrow ⋙ map f₁ ⟶ s.toStructuredArrow :=
     { app := fun X => eqToHom (by simp [← h₁])
       naturality := fun j₁ j₂ φ => by
         ext
@@ -236,24 +199,25 @@ theorem uniq {K : J ⥤ C} {c : Cone K} (hc : IsLimit c) (s : Cone (K ⋙ F))
         -- Asked here https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20not.20using.20a.20simp.20lemma/near/353943416
         -- I'm now doing `simp, rw [Comma.eqToHom_right, Comma.eqToHom_right], simp` but
         -- I squeezed the first `simp`.
-        simp only [Functor.mapCone_pt, Functor.comp_obj, toDiagram_obj,
-          Functor.mapCone_π_app, map_mk, mk_right, Functor.comp_map, toDiagram_map, comp_right,
-          map_map_right, homMk_right]
+        simp only [Functor.mapCone_pt, Functor.comp_obj, Cone.toStructuredArrow_obj,
+          Functor.mapCone_π_app, map_mk, mk_right, Functor.comp_map, Cone.toStructuredArrow_map,
+          comp_right, map_map_right, homMk_right]
         rw [Comma.eqToHom_right, Comma.eqToHom_right] -- this is a `simp` lemma
         simp }
-  let α₂ : toDiagram (F.mapCone c) ⋙ map f₂ ⟶ toDiagram s :=
+  let α₂ : (F.mapCone c).toStructuredArrow ⋙ map f₂ ⟶ s.toStructuredArrow :=
     { app := fun X => eqToHom (by simp [← h₂])
       naturality := fun _ _ _ => by
         ext
         -- porting note: see comments above. `simp` should close this goal (and did in Lean 3)
-        simp only [Functor.mapCone_pt, Functor.comp_obj, toDiagram_obj, Functor.mapCone_π_app,
-          map_mk, mk_right, Functor.comp_map, toDiagram_map, comp_right, map_map_right, homMk_right]
+        simp only [Functor.mapCone_pt, Functor.comp_obj, Cone.toStructuredArrow_obj,
+          Functor.mapCone_π_app, map_mk, mk_right, Functor.comp_map, Cone.toStructuredArrow_map,
+          comp_right, map_map_right, homMk_right]
         rw [Comma.eqToHom_right, Comma.eqToHom_right] -- this is a `simp` lemma
         simp }
-  let c₁ : Cone (toDiagram s ⋙ pre s.pt K F) :=
-    (Cones.postcompose (whiskerRight α₁ (pre s.pt K F) : _)).obj (toCone F c f₁)
-  let c₂ : Cone (toDiagram s ⋙ pre s.pt K F) :=
-    (Cones.postcompose (whiskerRight α₂ (pre s.pt K F) : _)).obj (toCone F c f₂)
+  let c₁ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
+    (Cones.postcompose (whiskerRight α₁ (pre s.pt K F) : _)).obj (c.toStructuredArrowCone F f₁)
+  let c₂ : Cone (s.toStructuredArrow ⋙ pre s.pt K F) :=
+    (Cones.postcompose (whiskerRight α₂ (pre s.pt K F) : _)).obj (c.toStructuredArrowCone F f₂)
   -- The two cones can then be combined and we may obtain a cone over the two cones since
   -- `StructuredArrow s.pt F` is cofiltered.
   let c₀ := IsCofiltered.cone (biconeMk _ c₁ c₂)

Mathlib/CategoryTheory/Limits/ConeCategory.lean

@@ -5,8 +5,8 @@ Authors: Andrew Yang
 -/
 import Mathlib.CategoryTheory.Adjunction.Comma
 import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
-import Mathlib.CategoryTheory.StructuredArrow
 import Mathlib.CategoryTheory.Limits.Shapes.Equivalence
+import Mathlib.CategoryTheory.Over
 
 #align_import category_theory.limits.cone_category from "leanprover-community/mathlib"@"18302a460eb6a071cf0bfe11a4df025c8f8af244"
 
@@ -35,6 +35,55 @@ variable {J : Type u₁} [Category.{v₁} J] {K : Type u₂} [Category.{v₂} K]
 
 variable {C : Type u₃} [Category.{v₃} C] {D : Type u₄} [Category.{v₄} D]
 
+/-- Given a cone `c` over `F`, we can interpret the legs of `c` as structured arrows
+    `c.pt ⟶ F.obj -`. -/
+@[simps]
+def Cone.toStructuredArrow {F : J ⥤ C} (c : Cone F) : J ⥤ StructuredArrow c.pt F where
+  obj j := StructuredArrow.mk (c.π.app j)
+  map f := StructuredArrow.homMk f
+
+/-- Interpreting the legs of a cone as a structured arrow and then forgetting the arrow again does
+    nothing. -/
+@[simps!]
+def Cone.toStructuredArrowCompProj {F : J ⥤ C} (c : Cone F) :
+    c.toStructuredArrow ⋙ StructuredArrow.proj _ _ ≅ 𝟭 J :=
+  Iso.refl _
+
+@[simp]
+lemma Cone.toStructuredArrow_comp_proj {F : J ⥤ C} (c : Cone F) :
+    c.toStructuredArrow ⋙ StructuredArrow.proj _ _ = 𝟭 J :=
+  rfl
+
+/-- Interpreting the legs of a cone as a structured arrow, interpreting this arrow as an arrow over
+    the cone point, and finally forgetting the arrow is the same as just applying the functor the
+    cone was over. -/
+@[simps!]
+def Cone.toStructuredArrowCompToUnderCompForget {F : J ⥤ C} (c : Cone F) :
+    c.toStructuredArrow ⋙ StructuredArrow.toUnder _ _ ⋙ Under.forget _ ≅ F :=
+  Iso.refl _
+
+@[simp]
+lemma Cone.toStructuredArrow_comp_toUnder_comp_forget {F : J ⥤ C} (c : Cone F) :
+    c.toStructuredArrow ⋙ StructuredArrow.toUnder _ _ ⋙ Under.forget _ = F :=
+  rfl
+
+/-- Given a diagram of `StructuredArrow X F`s, we may obtain a cone with cone point `X`. -/
+@[simps!]
+def Cone.fromStructuredArrow (F : C ⥤ D) {X : D} (G : J ⥤ StructuredArrow X F) :
+    Cone (G ⋙ StructuredArrow.proj X F ⋙ F) where
+  π := { app := fun j => (G.obj j).hom }
+#align category_theory.structured_arrow_cone.diagram_to_cone CategoryTheory.Limits.Cone.fromStructuredArrow
+
+/-- Given a cone `c : Cone K` and a map `f : X ⟶ F.obj c.X`, we can construct a cone of structured
+arrows over `X` with `f` as the cone point.
+-/
+@[simps]
+def Cone.toStructuredArrowCone {K : J ⥤ C} (c : Cone K) (F : C ⥤ D) {X : D} (f : X ⟶ F.obj c.pt) :
+    Cone ((F.mapCone c).toStructuredArrow ⋙ StructuredArrow.map f ⋙ StructuredArrow.pre _ K F) where
+  pt := StructuredArrow.mk f
+  π := { app := fun j => StructuredArrow.homMk (c.π.app j) rfl }
+#align category_theory.structured_arrow_cone.to_cone CategoryTheory.Limits.Cone.toStructuredArrowCone
+
 /-- Construct an object of the category `(Δ ↓ F)` from a cone on `F`. This is part of an
     equivalence, see `Cone.equivCostructuredArrow`. -/
 @[simps]
@@ -124,6 +173,53 @@ def IsLimit.ofReflectsConeTerminal {F : J ⥤ C} {F' : K ⥤ D} (G : Cone F ⥤
   (Cone.isLimitEquivIsTerminal _).symm <| (Cone.isLimitEquivIsTerminal _ hc).isTerminalOfObj _ _
 #align category_theory.limits.is_limit.of_reflects_cone_terminal CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal
 
+/-- Given a cocone `c` over `F`, we can interpret the legs of `c` as costructured arrows
+    `F.obj - ⟶ c.pt`. -/
+@[simps]
+def Cocone.toCostructuredArrow {F : J ⥤ C} (c : Cocone F) : J ⥤ CostructuredArrow F c.pt where
+  obj j := CostructuredArrow.mk (c.ι.app j)
+  map f := CostructuredArrow.homMk f
+
+/-- Interpreting the legs of a cocone as a costructured arrow and then forgetting the arrow again
+    does nothing. -/
+@[simps!]
+def Cocone.toCostructuredArrowCompProj {F : J ⥤ C} (c : Cocone F) :
+    c.toCostructuredArrow ⋙ CostructuredArrow.proj _ _ ≅ 𝟭 J :=
+  Iso.refl _
+
+@[simp]
+lemma Cocone.toCostructuredArrow_comp_proj {F : J ⥤ C} (c : Cocone F) :
+    c.toCostructuredArrow ⋙ CostructuredArrow.proj _ _ = 𝟭 J :=
+  rfl
+
+/-- Interpreting the legs of a cocone as a costructured arrow, interpreting this arrow as an arrow
+    over the cocone point, and finally forgetting the arrow is the same as just applying the
+    functor the cocone was over. -/
+@[simps!]
+def Cocone.toCostructuredArrowCompToOverCompForget {F : J ⥤ C} (c : Cocone F) :
+    c.toCostructuredArrow ⋙ CostructuredArrow.toOver _ _ ⋙ Over.forget _ ≅ F :=
+  Iso.refl _
+
+@[simp]
+lemma Cocone.toCostructuredArrow_comp_toOver_comp_forget {F : J ⥤ C} (c : Cocone F) :
+    c.toCostructuredArrow ⋙ CostructuredArrow.toOver _ _ ⋙ Over.forget _ = F :=
+  rfl
+
+/-- Given a diagram `CostructuredArrow F X`s, we may obtain a cocone with cone point `X`. -/
+@[simps!]
+def Cocone.fromCostructuredArrow (F : C ⥤ D) {X : D} (G : J ⥤ CostructuredArrow F X) :
+    Cocone (G ⋙ CostructuredArrow.proj F X ⋙ F) where
+  ι := { app := fun j => (G.obj j).hom }
+
+/-- Given a cocone `c : Cocone K` and a map `f : F.obj c.X ⟶ X`, we can construct a cocone of
+    costructured arrows over `X` with `f` as the cone point. -/
+@[simps]
+def Cocone.toCostructuredArrowCocone {K : J ⥤ C} (c : Cocone K) (F : C ⥤ D) {X : D}
+    (f : F.obj c.pt ⟶ X) : Cocone ((F.mapCocone c).toCostructuredArrow ⋙
+      CostructuredArrow.map f ⋙ CostructuredArrow.pre _ _ _) where
+  pt := CostructuredArrow.mk f
+  ι := { app := fun j => CostructuredArrow.homMk (c.ι.app j) rfl }
+
 /-- Construct an object of the category `(F ↓ Δ)` from a cocone on `F`. This is part of an
     equivalence, see `Cocone.equivStructuredArrow`. -/
 @[simps]

Mathlib/CategoryTheory/Sites/CoverPreserving.lean

@@ -133,7 +133,7 @@ theorem compatiblePreservingOfFlat {C : Type u₁} [Category.{v₁} C] {D : Type
     over it since `StructuredArrow W u` is cofiltered.
     Then, it suffices to prove that it is compatible when restricted onto `u(c'.X.right)`.
     -/
-  let c' := IsCofiltered.cone (StructuredArrowCone.toDiagram c ⋙ StructuredArrow.pre _ _ _)
+  let c' := IsCofiltered.cone (c.toStructuredArrow ⋙ StructuredArrow.pre _ _ _)
   have eq₁ : f₁ = (c'.pt.hom ≫ G.map (c'.π.app left).right) ≫ eqToHom (by simp) := by
     erw [← (c'.π.app left).w]
     dsimp