ΓHomEquiv_naturality_left_symm — Mathlib

English

Symmetric naturality form of ΓHomEquiv with respect to left; the reversed equation holds.

Русский

Симметричная форма натуральности ΓHomEquiv слева; обратное равенство выполняется.

LaTeX

$$$\GammaHomEquiv^{-1}(f \circ g) = (Functor.const _).map f \circ \GammaHomEquiv^{-1}(g)$$$

Lean4

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

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