mk'

Mathlib.CategoryTheory.Sites.MayerVietorisSquare

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk'

Lean4

/-- Constructor for Mayer-Vietoris squares taking as an input
a square `sq` such that `sq.f₁₃` is a mono and that for every
sheaf of types `F`, the square `sq.op.map F.val` is a pullback square. -/
@[simps toSquare]
noncomputable def mk' (sq : Square C) [Mono sq.f₁₃] (H : ∀ (F : Sheaf J (Type v)), (sq.op.map F.val).IsPullback) :
    J.MayerVietorisSquare where
  toSquare := sq
  isPushout := by
    rw [Square.isPushout_iff_op_map_yoneda_isPullback]
    intro F
    exact (F.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff sq).2 (H F)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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