ι_plusCompIso_hom — Mathlib

English

A compatibility relation for the iota component of the plus-Comp isomorphism: a specified equality of composed maps involving colimits and diagram is satisfied.

Русский

Совместимость компоненты iota в изоморфизме плюс-объекта: выполняется определённое равенство композиций связанных с колимитами и диаграммой.

LaTeX

$$$F.map(\\mathrm{colimit.ι}(W)) \\circ (J.plusCompIso F P).hom_X = (J.diagramCompIso F P X.unop).hom_W \\circ \\mathrm{colimit.ι}(W)$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_plusCompIso_hom (X) (W) :
    F.map (colimit.ι _ W) ≫ (J.plusCompIso F P).hom.app X = (J.diagramCompIso F P X.unop).hom.app W ≫ colimit.ι _ W :=
  by
  delta diagramCompIso plusCompIso
  simp only [Iso.trans_hom, NatIso.ofComponents_hom_app, ← Category.assoc]
  erw [(isColimitOfPreserves F (colimit.isColimit (J.diagram P (unop X)))).fac]
  simp

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