English
If left index L and right index R are finite and decidable, then WalkingMultispan J forms a finite category.
Русский
При конечных и разрешимых равенствах левого и правого индексов, WalkingMultispan J образует конечную категорию.
LaTeX
$$$\operatorname{FinCat}(\mathrm{WalkingMultispan}(J))$ under $[\text{DecidableEq } J.L]$ and $[\text{DecidableEq } J.R]$$$
Lean4
instance [DecidableEq J.L] [DecidableEq J.R] : FinCategory (WalkingMultispan J) where
fintypeHom
| .left a, .left b => ⟨if e : a = b then {eqToHom (e ▸ rfl)} else ∅, by rintro ⟨⟩; simp⟩
| .left a, .right b =>
⟨⟨(if e : J.fst a = b then {Hom.fst a ≫ eqToHom (e ▸ rfl)} else 0) +
(if e : J.snd a = b then {Hom.snd a ≫ eqToHom (e ▸ rfl)} else 0),
by
split_ifs with h₁ h₂
· simp only [Multiset.singleton_add, Multiset.nodup_cons, Multiset.mem_singleton, Multiset.nodup_singleton,
and_true]
let f : ((left a : WalkingMultispan J) ⟶ right b) → Prop
| .fst a => True
| .snd a => False
apply ne_of_apply_ne f
conv_lhs => tactic => subst h₁; simp only [eqToHom_refl, f]
conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, f]
simp
all_goals simp⟩,
by rintro ⟨⟩ <;> simp⟩
| .right a, .left b => ⟨∅, by rintro ⟨⟩⟩
| .right a, .right b => ⟨if e : a = b then {eqToHom (e ▸ rfl)} else ∅, by rintro ⟨⟩; simp⟩
