plusMap — Mathlib

English

The definition of plusObj collects the universal construction across the indexing of covers.

Русский

Определение plusObj собирает универсальную конструкцию по индексам покрытий.

LaTeX

$$$\\mathrm{plusObj}\;P = \\mathrm{colim}\\, (J.\\mathrm{diagram}\\ P\\ X.unop)$$$

Lean4

/-- An auxiliary definition used in `plus` below. -/
def plusMap {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) : J.plusObj P ⟶ J.plusObj Q
    where
  app X := colimMap (J.diagramNatTrans η X.unop)
  naturality := by
    intro X Y f
    dsimp [plusObj]
    ext
    simp only [diagramPullback_app, ι_colimMap, colimit.ι_pre_assoc, colimit.ι_pre, ι_colimMap_assoc, Category.assoc]
    simp_rw [← Category.assoc]
    congr 1
    exact Multiequalizer.hom_ext _ _ _ (fun I => by simp)

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