sheafifyMap_id — Mathlib

English

Same compatibility statement as above for the same objects, expressing the coherence of the plus-Comp isomorphism.

Русский

Та же совместимость между теми же объектами, выражающая когерентность изоморфизма плюс-Comp.

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

@[simp]
theorem sheafifyMap_id (P : Cᵒᵖ ⥤ D) : J.sheafifyMap (𝟙 P) = 𝟙 (J.sheafify P) :=
  by
  dsimp [sheafifyMap, sheafify]
  simp

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