small_proj_preimage_of_locallySmall

English

If 𝒢 ⊆ C is small and D is locally small, then the preimage under the projection proj S T of 𝒢 is small as a family of objects over 𝒢.

Русский

Пусть 𝒢 ⊆ C имеет множество малых, и D локально-мал, тогда прообраз под проекцией proj S T от 𝒢 маловыпуклый как семейство объектов.

LaTeX

$$$$\text{Small}((\mathrm{proj}\ S\ T).\mathrm{obj}^{-1}(\mathcal{G})).$$$$

Lean4

instance small_proj_preimage_of_locallySmall {𝒢 : Set C} [Small.{v₁} 𝒢] [LocallySmall.{v₁} D] :
    Small.{v₁} ((proj S T).obj ⁻¹' 𝒢) :=
  by
  suffices (proj S T).obj ⁻¹' 𝒢 = Set.range fun f : Σ G : 𝒢, S ⟶ T.obj G => mk f.2
    by
    rw [this]
    infer_instance
  exact Set.ext fun X => ⟨fun h => ⟨⟨⟨_, h⟩, X.hom⟩, (eq_mk _).symm⟩, by cat_disch⟩

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