ΓRes_map — Mathlib

English

The ΓRes components are natural in the presheaf variable; i.e., (Γ J A).map f ≫ ΓRes G U = ΓRes F U ≫ f.val.app U.

Русский

Компоненты ΓRes естественны по отношению к morphisms: (Γ J A).map f ≫ ΓRes G U = ΓRes F U ≫ f.val.app U.

LaTeX

$$$(\Gamma J A).map f \;\gg\; \GammaRes G U = \GammaRes F U \;\gg\; f.\mathrm{val}.\mathrm{app} U$$$

Lean4

@[reassoc (attr := simp)]
theorem ΓRes_map [HasGlobalSectionsFunctor J A] (F : Sheaf J A) {V U : Cᵒᵖ} (f : U ⟶ V) :
    F.ΓRes U ≫ F.val.map f = F.ΓRes V :=
  F.coneΓ.w f

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