English
Under decidable equality on the left and right index sets, the walking multicospan forms a finite category; in particular, the Hom-sets are finite.
Русский
При разрешимой по множеству равенств слева и справа равенства, ходовая multicospan образует конечную категорию; в частности, множество мороморфизмов между любыми двумя объектами конечно.
LaTeX
$$$\text{FinCat}(\mathrm{WalkingMulticospan}(J))$ при условии $[\text{DecidableEq } J.L]$, $[\text{DecidableEq } J.R]$$$
Lean4
instance [DecidableEq J.L] [DecidableEq J.R] : FinCategory (WalkingMulticospan 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 b = a then {eqToHom (e ▸ rfl) ≫ Hom.fst b} else 0) +
(if e : J.snd b = a then {eqToHom (e ▸ rfl) ≫ Hom.snd b} 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 : WalkingMulticospan 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, Category.id_comp, f]
conv_rhs => tactic => subst h₂; simp only [eqToHom_refl, Category.id_comp, 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⟩
