opEpi_comp

Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators

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

English

For σ in M.GeneratingSections and p: M ⟶ N, q: N ⟶ P, if p and q are epis, then σ.ofEpi (p ≫ q) = (σ.ofEpi p).ofEpi q.

Русский

Для σ и эпиморфизмов p, q выполняется σ.ofEpi(p ≫ q) = (σ.ofEpi p).ofEpi q.

LaTeX

$$$\sigma.ofEpi(p \circ q) = (\sigma.ofEpi(p)).ofEpi(q)$$$

Lean4

theorem opEpi_comp (σ : M.GeneratingSections) (p : M ⟶ N) (q : N ⟶ P) [Epi p] [Epi q] :
    σ.ofEpi (p ≫ q) = (σ.ofEpi p).ofEpi q :=
  rfl

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

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

Разделы

Аффилиация

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