map_f₂₄_op_glue

Mathlib.CategoryTheory.Sites.MayerVietorisSquare

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.map_f₂₄_op_glue

English

If h.glue u v huv is chosen, then P.map S.f₂₄.op (h.glue u v huv) = u.

Русский

При выборе glue, выполняется тождество через отображение P.map f24.op: P.map f24.op (glue) = u.

LaTeX

$$P.map S.f₂₄.op (h.glue u v huv) = u$$

Lean4

@[simp]
theorem map_f₂₄_op_glue : P.map S.f₂₄.op (h.glue u v huv) = u :=
  PullbackCone.IsLimit.equivPullbackObj_symm_apply_fst h.isLimit _

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

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

Разделы

Аффилиация

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