opEpi_id

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

URI: https://scilib.ai/kg/mathlib#SheafOfModules.GeneratingSections.opEpi_id

English

The identity σ.ofEpi 𝟙 M equals σ itself for any σ in M.GeneratingSections.

Русский

Для любого σ ∈ M.GeneratingSections верно σ.ofEpi 𝟙 M = σ.

LaTeX

$$$\sigma.{\text{ofEpi}}(\mathrm{id}_M) = \sigma$$$

Lean4

theorem opEpi_id (σ : M.GeneratingSections) : σ.ofEpi (𝟙 M) = σ :=
  rfl

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

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

Разделы

Аффилиация

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