isSheafFor_iff_yonedaSheafCondition

English

The sheaf condition for P with respect to a presieve S is equivalent to the Yoneda-based sheaf condition for P and S.

Русский

Условие sheaf для P относительно предрассыпь S эквивалентно Yoneda-условию для P и S.

LaTeX

$$IsSheafFor P S.arrows ↔ YonedaSheafCondition P S$$

Lean4

/-- The yoneda version of the sheaf condition is equivalent to the sheaf condition.

C2.1.4 of [Elephant].
-/
theorem isSheafFor_iff_yonedaSheafCondition {P : Cᵒᵖ ⥤ Type v₁} :
    IsSheafFor P (S : Presieve X) ↔ YonedaSheafCondition P S :=
  by
  rw [IsSheafFor, YonedaSheafCondition]
  simp_rw [extension_iff_amalgamation]
  rw [Equiv.forall_congr_left natTransEquivCompatibleFamily]
  rw [Subtype.forall]
  exact forall₂_congr fun x hx ↦ by simp [Equiv.existsUnique_congr_right]

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