feat(CategoryTheory): Finality of functors from filtered categories into PUnit (#15641)

javra · javra · commit 815eabcd67f2 · 2024-08-12T10:09:28.000Z
diff --git a/Mathlib/CategoryTheory/Filtered/Final.lean b/Mathlib/CategoryTheory/Filtered/Final.lean
@@ -230,4 +230,24 @@ theorem Functor.initial_iff_isCofiltered_costructuredArrow [IsCofilteredOrEmpty
 
 end LocallySmall
 
+/-- If `C` is filtered, then every functor `F : C ⥤ Discrete PUnit` is final. -/
+theorem Functor.final_of_isFiltered_of_pUnit {C : Type u₁} [Category.{v₁} C]
+    [IsFiltered C] (F : C ⥤ Discrete PUnit) :
+    Final F := by
+  refine final_of_exists_of_isFiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
+  · use Classical.choice IsFiltered.nonempty
+    exact ⟨Discrete.eqToHom (by simp)⟩
+  · use c; use 𝟙 c
+    apply Subsingleton.elim
+
+/-- If `C` is cofiltered, then every functor `F : C ⥤ Discrete PUnit` is initial. -/
+theorem Functor.initial_of_isCofiltered_pUnit {C : Type u₁} [Category.{v₁} C]
+    [IsCofiltered C] (F : C ⥤ Discrete PUnit) :
+    Initial F := by
+  refine initial_of_exists_of_isCofiltered F (fun _ => ?_) (fun {_} {c} _ _ => ?_)
+  · use Classical.choice IsCofiltered.nonempty
+    exact ⟨Discrete.eqToHom (by simp)⟩
+  · use c; use 𝟙 c
+    apply Subsingleton.elim
+
 end CategoryTheory
