feat(CategoryTheory/Limits): precomposition with final functors and ColimitType (#30779)

We obtain a dual result to #30403 for the interaction between final functors and colimits of functors to types. This is phrased using the universe generic `Functor.ColimitType`. (We also improve the proof of #30403)

Author: joelriou

Mathlib/CategoryTheory/IsConnected.lean

@@ -145,6 +145,19 @@ theorem constant_of_preserves_morphisms [IsPreconnected J] {α : Type u₂} (F :
         map := fun f => eqToHom (by ext; exact h _ _ f) }
       j j'
 
+/-- If `J` is connected, then given any function `F` such that the presence of a
+morphism `j₁ ⟶ j₂` implies `F j₁ = F j₂`, there exists `a` such that `F j = a`
+holds for any `j`. See `constant_of_preserves_morphisms` for a different
+formulation of the fact that `F` is constant.
+This can be thought of as a local-to-global property.
+
+The converse is shown in `IsConnected.of_constant_of_preserves_morphisms`
+-/
+theorem constant_of_preserves_morphisms' [IsConnected J] {α : Type u₂} (F : J → α)
+    (h : ∀ (j₁ j₂ : J) (_ : j₁ ⟶ j₂), F j₁ = F j₂) :
+    ∃ (a : α), ∀ (j : J), F j = a :=
+  ⟨F (Classical.arbitrary _), fun _ ↦ constant_of_preserves_morphisms _ h _ _⟩
+
 /-- `J` is connected if: given any function `F : J → α` which is constant for any
 `j₁, j₂` for which there is a morphism `j₁ ⟶ j₂`, then `F` is constant.
 This can be thought of as a local-to-global property.

Mathlib/CategoryTheory/Limits/Final/Type.lean

@@ -16,6 +16,10 @@ As `Functor.sections` identify to limits of functors to types
 be deduced from general results about limits and
 initial functors, but we provide a more down to earth proof.
 
+We also obtain the dual result that if `F` is final,
+then `F.colimitTypePrecomp : (F ⋙ P).ColimitType → P.ColimitType`
+is a bijection.
+
 -/
 
 universe w v₁ v₂ u₁ u₂
@@ -44,22 +48,57 @@ lemma bijective_sectionsPrecomp (F : C ⥤ D) (P : D ⥤ Type w) [F.Initial] :
     have h₂ := s₂.property X.hom
     dsimp at this h₁ h₂
     rw [← h₁, this, h₂]
-  · let X (Y : D) : CostructuredArrow F Y := Classical.arbitrary _
-    let val (Y : D) : P.obj Y := P.map (X Y).hom (t.val (X Y).left)
-    have h (Y : D) (Z : CostructuredArrow F Y) :
-        val Y = P.map Z.hom (t.val Z.left) :=
-      constant_of_preserves_morphisms (α := P.obj Y)
-        (fun (Z : CostructuredArrow F Y) ↦ P.map Z.hom (t.val Z.left)) (by
+  · have h (Y : D) := constant_of_preserves_morphisms'
+      (fun (Z : CostructuredArrow F Y) ↦ P.map Z.hom (t.val Z.left)) (by
           intro Z₁ Z₂ φ
           dsimp
           rw [← t.property φ.left]
           dsimp
-          rw [← FunctorToTypes.map_comp_apply, CostructuredArrow.w]) _ _
+          rw [← FunctorToTypes.map_comp_apply, CostructuredArrow.w])
+    choose val hval using h
     refine ⟨⟨val, fun {Y₁ Y₂} f ↦ ?_⟩, ?_⟩
-    · rw [h Y₁ (X Y₁), h Y₂ ((CostructuredArrow.map f).obj (X Y₁))]
-      simp
+    · let X : CostructuredArrow F Y₁ := Classical.arbitrary _
+      simp [← hval Y₁ X, ← hval Y₂ ((CostructuredArrow.map f).obj X)]
     · ext X : 2
-      simpa using h (F.obj X) (CostructuredArrow.mk (𝟙 _))
+      simpa using (hval (F.obj X) (CostructuredArrow.mk (𝟙 _))).symm
+
+/-- Given `P : D ⥤ Type w` and `F : C ⥤ D`, this is the obvious map
+`(F ⋙ P).ColimitType → P.ColimitType`. -/
+def colimitTypePrecomp (F : C ⥤ D) (P : D ⥤ Type w) :
+    (F ⋙ P).ColimitType → P.ColimitType :=
+  (F ⋙ P).descColimitType (P.coconeTypes.precomp F)
+
+@[simp]
+lemma colimitTypePrecomp_ιColimitType (F : C ⥤ D) {P : D ⥤ Type w}
+    (i : C) (x : P.obj (F.obj i)) :
+    colimitTypePrecomp F P ((F ⋙ P).ιColimitType i x) = P.ιColimitType (F.obj i) x :=
+  rfl
+
+lemma bijective_colimitTypePrecomp (F : C ⥤ D) (P : D ⥤ Type w) [F.Final] :
+    Function.Bijective (F.colimitTypePrecomp (P := P)) := by
+  refine ⟨?_, fun x ↦ ?_⟩
+  · have h (Y : D) := constant_of_preserves_morphisms'
+      (fun (Z : StructuredArrow Y F) ↦ (F ⋙ P).ιColimitType Z.right ∘ P.map Z.hom) (by
+        intro Z₁ Z₂ f
+        ext x
+        dsimp
+        rw [← (F ⋙ P).ιColimitType_map f.right, comp_map,
+          ← FunctorToTypes.map_comp_apply, StructuredArrow.w f])
+    choose φ hφ using h
+    let c : P.CoconeTypes :=
+      { pt := (F ⋙ P).ColimitType
+        ι Y := φ Y
+        ι_naturality {Y₁ Y₂} f := by
+          ext
+          have X : StructuredArrow Y₂ F := Classical.arbitrary _
+          rw [← hφ Y₂ X, ← hφ Y₁ ((StructuredArrow.map f).obj X)]
+          simp }
+    refine Function.RightInverse.injective (g := (P.descColimitType c)) (fun x ↦ ?_)
+    obtain ⟨X, x, rfl⟩ := (F ⋙ P).ιColimitType_jointly_surjective x
+    simp [c, ← hφ (F.obj X) (StructuredArrow.mk (𝟙 _))]
+  · obtain ⟨X, x, rfl⟩ := P.ιColimitType_jointly_surjective x
+    let Y : StructuredArrow X F := Classical.arbitrary _
+    exact ⟨(F ⋙ P).ιColimitType Y.right (P.map Y.hom x), by simp⟩
 
 end Functor
 

Mathlib/CategoryTheory/Limits/Types/ColimitType.lean

@@ -84,6 +84,14 @@ def precompose (c : CoconeTypes.{w₁} F) {G : J ⥤ Type w₀'} (app : ∀ j, G
   ι_naturality f := by
     rw [Function.comp_assoc, naturality, ← Function.comp_assoc, ι_naturality]
 
+/-- Given `F : J ⥤ w₀`, `c : F.CoconeTypes` and `G : J' ⥤ J`, this is
+the induced cocone in `(G ⋙ F).CoconeTypes`. -/
+@[simps]
+def precomp (c : CoconeTypes.{w₁} F) {J' : Type*} [Category J'] (G : J' ⥤ J) :
+    CoconeTypes.{w₁} (G ⋙ F) where
+  pt := c.pt
+  ι _ := c.ι _
+
 end CoconeTypes
 
 /-- Given `F : J ⥤ Type w₀`, this is the relation `Σ j, F.obj j` which