isPushoutAddCommGrpFreeSheaf — Mathlib

English

For a Mayer-Vietoris square S and a functor P, S.SheafCondition P is equivalent to S.SheafCondition (P ⋙ coyoneda.obj X) for all X in Aᵒᵖ.

Русский

Для квадрата Майера–Виетоpиса S и каскадного P условиеSheafCondition эквивалентно для каждого X: S.SheafCondition (P ⋙ coyoneda.obj X).

LaTeX

$$$S.SheafCondition\ P \iff \forall X: A^{op},\ S.SheafCondition\big( P \circ \mathrm{coyoneda.obj}\ X \big)$$$

Lean4

theorem isPushoutAddCommGrpFreeSheaf [HasWeakSheafify J AddCommGrpCat.{v}] :
    (S.map (yoneda ⋙ (Functor.whiskeringRight _ _ _).obj AddCommGrpCat.free ⋙ presheafToSheaf J _)).IsPushout :=
  (S.isPushout.map (Sheaf.composeAndSheafify J AddCommGrpCat.free)).of_iso
    ((Square.mapFunctor.mapIso (presheafToSheafCompComposeAndSheafifyIso J AddCommGrpCat.free)).app (S.map yoneda))

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