sheafify — Mathlib

English

Composition compatibility for yonedaULiftEquiv: yonedaULiftEquiv (α ≫ β) equals β.app _ (yonedaULiftEquiv α).

Русский

Совместимость композиции для yonedaULiftEquiv: yonedaULiftEquiv (α ≫ β) = β.app _ (yonedaULiftEquiv α).

LaTeX

$$$J.yonedaULiftEquiv (\alpha ≫ \beta) = \beta.\val.app\ _ (J.yonedaULiftEquiv\alpha)$$$

Lean4

/-- The sheafification of a subpresheaf as a subpresheaf.
Note that this is a sheaf only when the whole presheaf is a sheaf. -/
def sheafify : Subpresheaf F where
  obj U := {s | G.sieveOfSection s ∈ J (unop U)}
  map := by
    rintro U V i s hs
    refine J.superset_covering ?_ (J.pullback_stable i.unop hs)
    intro _ _ h
    dsimp at h ⊢
    rwa [← FunctorToTypes.map_comp_apply]

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