toSheafify_app_apply

Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafify

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.toSheafify_app_apply

English

At each X, the application of toSheafify to an element x agrees with φ acting on x.

Русский

В каждом X применение toSheafify к элементу x совпадает с действием φ на x.

LaTeX

$$$((toSheafify(\alpha, \varphi)).\mathrm{app} X).hom(x) = \varphi_{X}(x).$$$

Lean4

theorem toSheafify_app_apply (X : Cᵒᵖ) (x : M₀.obj X) : ((toSheafify α φ).app X).hom x = φ.app X x :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru