feat(CategoryTheory): FinCategory instance on Pairwise (leanprover-community#33537)

Author: erdOne

Mathlib/CategoryTheory/Category/Pairwise.lean

@@ -7,7 +7,9 @@ module
 
 public import Mathlib.CategoryTheory.Category.Preorder
 public import Mathlib.CategoryTheory.Limits.IsLimit
+public import Mathlib.CategoryTheory.FinCategory.Basic
 public import Mathlib.Order.CompleteLattice.Basic
+public import Mathlib.Tactic.DeriveFintype
 
 /-!
 # The category of "pairwise intersections".
@@ -43,6 +45,7 @@ We use this as the objects of a category to describe the sheaf condition.
 inductive Pairwise (ι : Type v)
   | single : ι → Pairwise ι
   | pair : ι → ι → Pairwise ι
+  deriving Fintype, DecidableEq
 
 variable {ι : Type v}
 
@@ -59,6 +62,10 @@ inductive Hom : Pairwise ι → Pairwise ι → Type v
   | id_pair : ∀ i j, Hom (pair i j) (pair i j)
   | left : ∀ i j, Hom (pair i j) (single i)
   | right : ∀ i j, Hom (pair i j) (single j)
+  deriving DecidableEq
+
+-- False positive?
+attribute [nolint unusedArguments] instDecidableEqHom.decEq
 
 open Hom
 
@@ -95,6 +102,20 @@ instance : Category (Pairwise ι) where
 
 end
 
+instance {i j : Pairwise ι} [DecidableEq ι] : DecidableEq (i ⟶ j) :=
+  inferInstanceAs (DecidableEq (Pairwise.Hom i j))
+
+instance [Fintype ι] [DecidableEq ι] : FinCategory (Pairwise ι) where
+  fintypeHom
+  | .single i, .single j => ⟨if h : i = j then {eqToHom (h ▸ rfl)} else ∅, by rintro ⟨⟩; cat_disch⟩
+  | .single i, .pair j k => ⟨∅, by rintro ⟨⟩⟩
+  | .pair i j, .single k =>
+    ⟨(if h : i = k then {Hom.left i j ≫ eqToHom (h ▸ rfl)} else ∅) ∪
+      (if h : j = k then {Hom.right i j ≫ eqToHom (h ▸ rfl)} else ∅),
+        by rintro ⟨⟩ <;> cat_disch⟩
+  | .pair i j, .pair k l =>
+    ⟨if h : i = k ∧ j = l then {eqToHom (h.1 ▸ h.2 ▸ rfl)} else ∅, by rintro ⟨⟩; cat_disch⟩
+
 variable {α : Type u} (U : ι → α)
 
 section