finBiconeHom — Mathlib

English

For a finite J, the set of morphisms j ⟶ k in the bicone has a finite cardinality, given by a case analysis on j and k and the two possible directions left or right.

Русский

Для конечного J множество морфизмов в биоконе j ⟶ k конечно; разбор происходит по случаям левый/правый направления.

LaTeX

$$$[FinCategory J] \\Rightarrow \\text{Fintype}((\\text{Bicone } J).\\text{Hom}(j,k))$$$

Lean4

instance finBiconeHom [FinCategory J] (j k : Bicone J) : Fintype (j ⟶ k) :=
  by
  cases j <;> cases k
  ·
    exact
      { elems := { BiconeHom.left_id }
        complete := fun f => by cases f; simp }
  ·
    exact
      { elems := ∅
        complete := fun f => by cases f }
  ·
    exact
      { elems := {BiconeHom.left _}
        complete := fun f => by cases f; simp }
  ·
    exact
      { elems := ∅
        complete := fun f => by cases f }
  ·
    exact
      { elems := { BiconeHom.right_id }
        complete := fun f => by cases f; simp }
  ·
    exact
      { elems := {BiconeHom.right _}
        complete := fun f => by cases f; simp }
  ·
    exact
      { elems := ∅
        complete := fun f => by cases f }
  ·
    exact
      { elems := ∅
        complete := fun f => by cases f }
  ·
    exact
      { elems := Finset.image BiconeHom.diagram Fintype.elems
        complete := fun f => by
          rcases f with (_ | _ | _ | _ | f)
          simp only [Finset.mem_image]
          use f
          simpa using Fintype.complete _ }

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