sheafCondition_iff_bijective_toPullbackObj

English

For a Mayer–Vietoris square S and a presheaf P, the sheaf condition S.SheafCondition P is equivalent to the bijectivity of the map S.toPullbackObj P.

Русский

Для квадрата Mayer–Vietoris S и прешерифа P условие sheaf равносильно биективности отображения S.toPullbackObj P.

LaTeX

$$$S\text{.SheafCondition }P \iff \mathrm{Bijective}\bigl(S\text{.toPullbackObj }Pigr)$$

Lean4

theorem sheafCondition_iff_bijective_toPullbackObj (P : Cᵒᵖ ⥤ Type v') :
    S.SheafCondition P ↔ Function.Bijective (S.toPullbackObj P) :=
  by
  have := (S.toSquare.op.map P).pullbackCone.isLimitEquivBijective
  exact ⟨fun h ↦ this h.isLimit, fun h ↦ Square.IsPullback.mk _ (this.symm h)⟩

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