toPlus_mk — Mathlib

English

The mk construction realizes elements of J.plusObj P applied to op X as has-type objects produced by the colimit injection.

Русский

Конструкция mk реализует элементы J.plusObj P, применяемые к op X, как элементы типа, полученные инъекцией колимита.

LaTeX

$$$\text{Plus.mk} : Meq P S \to (J.plusObj P).obj (op X)$$$

Lean4

theorem toPlus_mk {X : C} {P : Cᵒᵖ ⥤ D} (S : J.Cover X) (x : ToType (P.obj (op X))) :
    (J.toPlus P).app _ x = mk (Meq.mk S x) := by
  dsimp [mk, toPlus]
  let e : S ⟶ ⊤ := homOfLE (OrderTop.le_top _)
  rw [← colimit.w _ e.op]
  delta Cover.toMultiequalizer
  rw [ConcreteCategory.comp_apply, ConcreteCategory.comp_apply]
  apply congr_arg
  dsimp [diagram]
  apply Concrete.multiequalizer_ext (C := D)
  intro i
  simp only [← ConcreteCategory.comp_apply, Category.assoc, Multiequalizer.lift_ι, Meq.equiv_symm_eq_apply]
  rfl

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