ΓObjEquivHom_naturality — Mathlib

English

Naturality of the equivalence ΓObjEquivHom with respect to morphisms f: F → G in the Sheaf category.

Русский

Натуральность эквивалентности ΓObjEquivHom по отношению к морфизмам f: F → G в категории шейфов.

LaTeX

$$$(\GammaObjEquivHom J G X) \circ (\Gamma J _).map f = (\Gamma J _).map f \circ (\GammaObjEquivHom J F X)$$$

Lean4

theorem ΓObjEquivHom_naturality [HasWeakSheafify J (Type w)] [HasGlobalSectionsFunctor J (Type w)] (X : Type w)
    [Unique X] {F G : Sheaf J (Type w)} (f : F ⟶ G) (x : (Γ J _).obj F) :
    (ΓObjEquivHom J G X) ((Γ J _).map f x) = (ΓObjEquivHom J F X) x ≫ f :=
  (constantSheafΓAdj J _).homEquiv_naturality_right_symm _ _

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