isSheafFor_arrows_iff_pullbacks — Mathlib

English

For presieve of arrows with HasPairwisePullbacks, IsSheafFor is equivalent to a unique glue t with pullback compatibility.

Русский

Для presieve стрелок с HasPairwisePullbacks IsSheafFor эквивалентно существованию уникального клея t, удовлетворяющего Pullback совместимости.

LaTeX

$$$(ofArrows X π).IsSheafFor P ↔ (∀ x, Arrows.PullbackCompatible P π x → ∃! t, ∀ i, P.map (π_i).op t = x_i)$$$

Lean4

theorem isSheafFor_arrows_iff_pullbacks :
    (ofArrows X π).IsSheafFor P ↔
      (∀ (x : (i : I) → P.obj (op (X i))), Arrows.PullbackCompatible P π x → ∃! t, ∀ i, P.map (π i).op t = x i) :=
  by simp_rw [← Arrows.pullbackCompatible_iff, isSheafFor_arrows_iff]

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