ΓObjEquivHom_naturality_symm — Mathlib

English

Symmetric naturality form for ΓObjEquivHom with respect to left; the symmetric formula holds.

Русский

Симметричная форма натуральности для ΓObjEquivHom по левой координате; выполняется симметричная формула.

LaTeX

$$$(\GammaObjEquivHom J G X).\mathrm{symm} (x \circ f) = (\mathrm{Functor.const} _).map f \circ (\GammaObjEquivHom J F X).\mathrm{symm} x$$$

Lean4

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

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