ΓHomEquiv_naturality_right_symm — Mathlib

English

Naturality of the inverse of ΓHomEquiv: for any f and g, ΓHomEquiv.symm (f ≫ Γ.map g) = ΓHomEquiv.symm f ≫ g.

Русский

Натуральность обратной к ΓHomEquiv: для любых отображений f и g выполняется равенство ΓHomEquiv.symm (f ≫ Γ.map g) = ΓHomEquiv.symm f ≫ g.

LaTeX

$$$\\Gamma\\mathrm{HomEquiv}^{-1}\\bigl(f \\circ (\\Gamma J A).map g\\bigr) = \\Gamma\\mathrm{HomEquiv}^{-1} f \\circ g$$$

Lean4

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

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