ΓNatIsoCoyoneda — Mathlib

English

Repeat of the symmetric naturality for ΓObjEquivHom with morphisms in the opposite direction.

Русский

Повтор симметричной натуральности для ΓObjEquivHom по направлениям гомоморфизмов.

LaTeX

$$$(\GammaObjEquivHom J G X).symm (x \circ f) = (\mathrm{Functor.const} _).map f \circ (\GammaObjEquivHom J F X).symm x$$$

Lean4

/-- For sheaves of types, the global sections functor is isomorphic to the covariant hom
functor of the terminal sheaf. -/
noncomputable def ΓNatIsoCoyoneda (X : Type max u v) [Unique X] :
    Γ J (Type max u v) ≅ coyoneda.obj (op ((constantSheaf J _).obj X)) :=
  NatIso.ofComponents (fun F ↦ (F.ΓObjEquivHom J X).toIso) fun f ↦
    by
    ext x
    exact ΓObjEquivHom_naturality J X f x

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