yonedaGluedToSheaf_app_comp — Mathlib

English

Naturality of the glued-to-sheaf construction: composing with γ and α yields the action of F on γ with the glued component.

Русский

Натуральность конструкции glued-to-sheaf: композирование с γ и α даёт действие F на γ с взведённой компонентой.

LaTeX

$$$(\\yonedaGluedToSheaf hf).val.app (op V) (\\gamma \\gg \\alpha) = F.val.map \\gamma^{op} ((\\yonedaGluedToSheaf hf).val.app (op U) \\alpha)$$$

Lean4

@[simp]
theorem yonedaGluedToSheaf_app_comp {V U : Scheme.{u}} (γ : V ⟶ U) (α : U ⟶ (glueData hf).glued) :
    (yonedaGluedToSheaf hf).val.app (op V) (γ ≫ α) = F.val.map γ.op ((yonedaGluedToSheaf hf).val.app (op U) α) :=
  congr_fun ((yonedaGluedToSheaf hf).val.naturality γ.op) α

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