isSheafFor_singleton_iff_of_hasPullback

English

Special case: if f has a pullback, then the singleton-sieve condition is equivalent to the corresponding fork being a limit built from pullback maps.

Русский

Особый случай: если у f есть pullback, то условие singleton-sieve эквивалентно тому, что соответствующая вилка является пределом, построенным из pullback-карт.

LaTeX

$$$Presieve.IsSheafFor F (.singleton f) \iff Nonempty(IsLimit(Fork.ofι f.op (pullback.fst f f).op (pullback.snd f f).op))$$$

Lean4

/-- Special case of `isSheafFor_singleton_iff` with `c = pullback.cone f f`. -/
theorem isSheafFor_singleton_iff_of_hasPullback {F : Cᵒᵖ ⥤ Type*} {X Y : C} {f : X ⟶ Y} [HasPullback f f] :
    Presieve.IsSheafFor F (.singleton f) ↔
      Nonempty
        (IsLimit
          (Fork.ofι (F.map f.op) (f := F.map (pullback.fst f f).op) (g := F.map (pullback.snd f f).op)
            (by simp [← Functor.map_comp, ← op_comp, pullback.condition]))) :=
  isSheafFor_singleton_iff (pullback.cone f f) (pullback.isLimit f f)

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