ΓHomEquiv_naturality_left — Mathlib

English

Naturality of ΓHomEquiv with respect to left composition: ΓHomEquiv((Functor.const _).map f ≫ g) = f ≫ ΓHomEquiv(g).

Русский

Натуральность ΓHomEquiv слева: ΓHomEquiv((Functor.const _).map f ≫ g) = f ≫ ΓHomEquiv(g).

LaTeX

$$$\GammaHomEquiv((\mathrm{Functor}.{\ca}}\text{const} \,).\mathrm{map} f \circ g) = f \circ \GammaHomEquiv(g)$$$

Lean4

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

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