ΓHomEquiv_naturality_right — Mathlib

English

Right naturality: ΓHomEquiv(f ≫ g.val) = ΓHomEquiv(f) ≫ (Γ J A).map g.

Русский

Право-натуральность: ΓHomEquiv(f ≫ g.val) = ΓHomEquiv(f) ≫ (Γ J A).map g.

LaTeX

$$$\GammaHomEquiv(f \;\gg\; g.\mathrm{val}) = \GammaHomEquiv(f) \;\gg\; (\Gamma J A).map g$$$

Lean4

/-- Naturality lemma for `ΓHomEquiv` analogous to `Adjunction.homEquiv_naturality_right`. -/
theorem ΓHomEquiv_naturality_right [HasGlobalSectionsFunctor J A] {X : A} {F F' : Sheaf J A}
    (f : (Functor.const _).obj X ⟶ F.val) (g : F ⟶ F') : ΓHomEquiv (f ≫ g.val) = ΓHomEquiv f ≫ (Γ J A).map g :=
  (congrArg _ ((sheafificationAdjunction J A).homEquiv_naturality_right_symm _ _)).trans
    ((constantSheafΓAdj J A).homEquiv_naturality_right _ _)

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