fintypeHom — Mathlib

English

For WidePullbackShape, the Hom-sets are finite in the finite index case.

Русский

Для WidePullbackShape множество гомоморфизмов конечного индекса конечно.

LaTeX

$$$\text{Hom}(j, j') \text{ finite for finite indices}$$$

Lean4

instance fintypeHom (j j' : WidePullbackShape J) : Fintype (j ⟶ j')
    where
  elems := by
    obtain - | j' := j'
    · obtain - | j := j
      · exact {Hom.id none}
      · exact {Hom.term j}
    · by_cases h : some j' = j
      · rw [h]
        exact {Hom.id j}
      · exact ∅
  complete := by
    rintro (_ | _)
    · cases j <;> simp
    · simp

Похожие утверждения