ϕ — Mathlib · SciLib

English

The locally small full subcategory of Ind-objects is well-behaved (exists hom-sets).

Русский

Локально малая полноть подкатегории Ind-объектов корректна (множества гомоморфизмов существуют).

LaTeX

$$$\mathrm{LocallySmall}\big(\mathrm{ObjectProperty.FullSubcategory}(\mathrm{IsIndObject}(C))\big)$$$

Lean4

/-- Implementation; see `nonempty_indParallelPairPresentation`. -/
def ϕ : F₁ f g P₁ P₂ ⟶ F₂ f g P₁ P₂ where
  app h := h.hom.1.left
  naturality _ _
    h := by
    have := h.w
    simp only [Functor.prod'_obj, Functor.comp_obj, prod_Hom, Functor.prod'_map, Functor.comp_map, prod_comp,
      Prod.mk.injEq, CostructuredArrow.hom_eq_iff, CostructuredArrow.map_obj_left,
      IndObjectPresentation.toCostructuredArrow_obj_left, CostructuredArrow.comp_left, CostructuredArrow.map_map_left,
      IndObjectPresentation.toCostructuredArrow_map_left] at this
    exact this.1

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