From ec5d1d8e277005586c3ca983680ead5416c79888 Mon Sep 17 00:00:00 2001
From: Markus Himmel <markus@himmel-villmar.de>
Date: Tue, 21 Jan 2025 21:03:22 +0000
Subject: [PATCH] feat(CategoryTheory): Functor.prod and Functor.prod' are
 final (#20841)

Co-authored-by: Markus Himmel <markus@lean-fro.org>
---
 Mathlib/CategoryTheory/Filtered/Final.lean | 18 +++++++++++++-----
 Mathlib/CategoryTheory/Limits/Final.lean   | 13 +++++++++++++
 Mathlib/CategoryTheory/Limits/Sifted.lean  | 12 +++++++++++-
 3 files changed, 37 insertions(+), 6 deletions(-)

diff --git a/Mathlib/CategoryTheory/Filtered/Final.lean b/Mathlib/CategoryTheory/Filtered/Final.lean
index 69bd8fd66b993..24e561db7288e 100644
--- a/Mathlib/CategoryTheory/Filtered/Final.lean
+++ b/Mathlib/CategoryTheory/Filtered/Final.lean
@@ -5,7 +5,7 @@ Authors: Markus Himmel
 -/
 import Mathlib.CategoryTheory.Filtered.Connected
 import Mathlib.CategoryTheory.Limits.TypesFiltered
-import Mathlib.CategoryTheory.Limits.Final
+import Mathlib.CategoryTheory.Limits.Sifted
 
 /-!
 # Final functors with filtered (co)domain
@@ -298,26 +298,34 @@ theorem Functor.initial_iff_isCofiltered_costructuredArrow [IsCofilteredOrEmpty
 
 /-- If `C` is filtered, then the structured arrow category on the diagonal functor `C ⥤ C × C`
 is filtered as well. -/
-instance [IsFiltered C] (X : C × C) : IsFiltered (StructuredArrow X (diag C)) := by
+instance [IsFilteredOrEmpty C] (X : C × C) : IsFiltered (StructuredArrow X (diag C)) := by
   haveI : ∀ Y, IsFiltered (StructuredArrow Y (Under.forget X.1)) := by
     rw [← final_iff_isFiltered_structuredArrow (Under.forget X.1)]
     infer_instance
   apply IsFiltered.of_equivalence (StructuredArrow.ofDiagEquivalence X).symm
 
 /-- The diagonal functor on any filtered category is final. -/
-instance Functor.final_diag_of_isFiltered [IsFiltered C] : Final (Functor.diag C) :=
+instance Functor.final_diag_of_isFiltered [IsFilteredOrEmpty C] : Final (Functor.diag C) :=
   final_of_isFiltered_structuredArrow _
 
+-- Adding this instance causes performance problems elsewhere, even with low priority
+theorem IsFilteredOrEmpty.isSiftedOrEmpty [IsFilteredOrEmpty C] : IsSiftedOrEmpty C :=
+  Functor.final_diag_of_isFiltered
+
+-- Adding this instance causes performance problems elsewhere, even with low priority
+attribute [local instance] IsFiltered.nonempty in
+theorem IsFiltered.isSifted [IsFiltered C] : IsSifted C where
+
 /-- If `C` is cofiltered, then the costructured arrow category on the diagonal functor `C ⥤ C × C`
 is cofiltered as well. -/
-instance [IsCofiltered C] (X : C × C) : IsCofiltered (CostructuredArrow (diag C) X) := by
+instance [IsCofilteredOrEmpty C] (X : C × C) : IsCofiltered (CostructuredArrow (diag C) X) := by
   haveI : ∀ Y, IsCofiltered (CostructuredArrow (Over.forget X.1) Y) := by
     rw [← initial_iff_isCofiltered_costructuredArrow (Over.forget X.1)]
     infer_instance
   apply IsCofiltered.of_equivalence (CostructuredArrow.ofDiagEquivalence X).symm
 
 /-- The diagonal functor on any cofiltered category is initial. -/
-instance Functor.initial_diag_of_isFiltered [IsCofiltered C] : Initial (Functor.diag C) :=
+instance Functor.initial_diag_of_isFiltered [IsCofilteredOrEmpty C] : Initial (Functor.diag C) :=
   initial_of_isCofiltered_costructuredArrow _
 
 /-- If `C` is filtered, then every functor `F : C ⥤ Discrete PUnit` is final. -/
diff --git a/Mathlib/CategoryTheory/Limits/Final.lean b/Mathlib/CategoryTheory/Limits/Final.lean
index 5124dc554a97f..f019212af5a48 100644
--- a/Mathlib/CategoryTheory/Limits/Final.lean
+++ b/Mathlib/CategoryTheory/Limits/Final.lean
@@ -1027,4 +1027,17 @@ instance Grothendieck.final_pre [hG : Final G] : (Grothendieck.pre F G).Final :=
 
 end Grothendieck
 
+section Prod
+
+variable {C : Type u₁} [Category.{v₁} C]
+variable {D : Type u₂} [Category.{v₂} D]
+variable {C' : Type u₃} [Category.{v₃} C']
+variable {D' : Type u₄} [Category.{v₄} D']
+variable (F : C ⥤ D) (G : C' ⥤ D')
+
+instance [F.Final] [G.Final] : (F.prod G).Final where
+  out := fun ⟨d, d'⟩ => isConnected_of_equivalent (StructuredArrow.prodEquivalence d d' F G).symm
+
+end Prod
+
 end CategoryTheory
diff --git a/Mathlib/CategoryTheory/Limits/Sifted.lean b/Mathlib/CategoryTheory/Limits/Sifted.lean
index 8f5721d4f8dae..7baf9a4e2a34b 100644
--- a/Mathlib/CategoryTheory/Limits/Sifted.lean
+++ b/Mathlib/CategoryTheory/Limits/Sifted.lean
@@ -20,7 +20,7 @@ preserves finite products.
 - [*Algebraic Theories*, Chapter 2.][Adamek_Rosicky_Vitale_2010]
 -/
 
-universe w v v₁ u u₁
+universe w v v₁ v₂ u u₁ u₂
 
 namespace CategoryTheory
 
@@ -101,4 +101,14 @@ end IsSifted
 
 end
 
+section
+
+variable {C : Type u} [Category.{v} C] [IsSiftedOrEmpty C] {D : Type u₁} [Category.{v₁} D]
+  {D' : Type u₂} [Category.{v₂} D'] (F : C ⥤ D) (G : C ⥤ D')
+
+instance [F.Final] [G.Final] : (F.prod' G).Final :=
+  show (diag C ⋙ F.prod G).Final from final_comp _ _
+
+end
+
 end CategoryTheory