p_comm

Mathlib.AlgebraicGeometry.Pullbacks

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Pullback.p_comm

English

Projections p1 and p2 commute with the pullback projections; the composed map p1 ≫ f equals p2 ≫ g.

Русский

Проекции p1 и p2 коммутируют с проекциям обратной диаграммы: p1 ≫ f = p2 ≫ g.

LaTeX

$$$ p_1 𝒰 f g \\;\\gg\\; f = p_2 𝒰 f g \\;\\gg\\; g$$

Lean4

theorem p_comm : p1 𝒰 f g ≫ f = p2 𝒰 f g ≫ g :=
  by
  apply Multicoequalizer.hom_ext
  simp [p1, p2, pullback.condition]

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

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

Разделы

Аффилиация

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