sheafCondition_iff_comp_coyoneda — Mathlib

English

A direct reformulation of the previous Coyoneda criterion for Sheaf condition in a Mayer-Vietoris square.

Русский

Прямое переразложение предыдущего критерия Coyoneda для условия Sheaf в квадрате Майера–Виетоpиса.

LaTeX

$$$S.SheafCondition\ P \iff \forall X: Coyoneda, S.SheafCondition( P \circ X)$$$

Lean4

theorem sheafCondition_iff_comp_coyoneda {A : Type u'} [Category.{v'} A] (P : Cᵒᵖ ⥤ A) :
    S.SheafCondition P ↔ ∀ (X : Aᵒᵖ), S.SheafCondition (P ⋙ coyoneda.obj X) :=
  Square.isPullback_iff_map_coyoneda_isPullback (S.op.map P)

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