instSmallArrowOfLocallySmall — Mathlib

English

If C is small and locally small, then Arrow(C) is small.

Русский

Если C малая и локально-малая, то Arrow(C) малая.

LaTeX

$$$\text{Small}(\text{Arrow}(C))$$$

Lean4

instance [Small.{w} C] [LocallySmall.{w} C] : Small.{w} (Arrow C) :=
  by
  let φ (f : Arrow C) : Σ (s t : C), s ⟶ t := ⟨_, _, f.hom⟩
  refine small_of_injective (f := φ) ?_
  rintro ⟨s, t, f⟩ ⟨s', t', f'⟩ h
  obtain rfl : s = s' := congr_arg Sigma.fst h
  simp only [Functor.id_obj, Sigma.mk.injEq, heq_eq_eq, true_and, φ] at h
  obtain rfl : t = t' := h.1
  obtain rfl : f = f' := by simpa using h
  rfl

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