toPresheaf_map_sheafificationAdjunction_unit_app

English

The map obtained by applying the symm of the sheafification homEquiv to a morphism g is equal to the corresponding image under the adjunction's homEquiv, composed with the toPresheaf map.

Русский

Отображение, полученное применением симм гомэквивалентности шейификации, равно образу через гомэквивалентность адъункции в сочетании с отображением toPresheaf.

LaTeX

$$$ (\mathrm{SheafOfModules.toSheaf R}).map ((sheafificationHomEquiv α).symm g) = ((sheafificationAdjunction J AddCommGrpCat).homEquiv P.presheaf ((SheafOfModules.toSheaf R).obj F)).symm ((toPresheaf R_0).map g) $$$

Lean4

@[simp]
theorem toPresheaf_map_sheafificationAdjunction_unit_app (M₀ : PresheafOfModules.{v} R₀) :
    (toPresheaf _).map ((sheafificationAdjunction α).unit.app M₀) = CategoryTheory.toSheafify J M₀.presheaf :=
  rfl

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