instIsSmallGeneratingMonomorphismsOfSmallSubobject

English

Given a generator G, the family of generating monomorphisms has existence of pushouts to enlarge subobjects.

Русский

Для генератора G существуют pushout-образования, позволяющие расширять подобъекты.

LaTeX

$$$\exists X', i, p', \text{pushouts } i\,\cdot\, p' = p$$$

Lean4

instance (G : C) [Small.{w} (Subobject G)] : MorphismProperty.IsSmall.{w} (generatingMonomorphisms G) :=
  by
  dsimp [generatingMonomorphisms]
  infer_instance

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