isSmall_ofHoms — Mathlib

English

Let W be a morphism property on a category C. For a small index type ι and a family of morphisms f_i : A_i → B_i (i ∈ ι), the induced morphism built from these arrows, denoted by ofHoms f, is small.

Русский

Пусть W — свойство морфизмов в категории C. Для малого типа индексов ι и семейства стрел f_i : A_i → B_i, образующийся из этих стрел морфизм ofHoms f является малым.

LaTeX

$$$\operatorname{IsSmall}(\operatorname{ofHoms} f)$$$

Lean4

instance isSmall_ofHoms {ι : Type t} [Small.{w} ι] {A B : ι → C} (f : ∀ i, A i ⟶ B i) : IsSmall.{w} (ofHoms f) :=
  by
  let φ (i : ι) : (ofHoms f).toSet := ⟨Arrow.mk (f i), ⟨i⟩⟩
  have hφ : Function.Surjective φ := by
    rintro ⟨⟨_, _, f⟩, ⟨i⟩⟩
    exact ⟨i, rfl⟩
  exact ⟨small_of_surjective hφ⟩

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