ΓNatIsoSectionsFunctor — Mathlib

English

Internal proof component for the Coyoneda-style representation of Γ.

Русский

Внутренняя часть доказательства представления Γ через Coyoneda.

LaTeX

$$$$\text{Proof component for the Coyoneda representation of }\Gamma.$$$$

Lean4

/-- For sheaves of types, the global sections functor is isomorphic to the sections functor
on presheaves. -/
noncomputable def ΓNatIsoSectionsFunctor : Γ J (Type max u v) ≅ sheafToPresheaf J _ ⋙ Functor.sectionsFunctor _ :=
  NatIso.ofComponents (fun F ↦ (ΓObjEquivSections J F).toIso) fun f ↦
    by
    ext x
    exact ΓObjEquivSections_naturality J f x

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