Γevaluation_naturality — Mathlib

English

The naturality of the Γ-evaluation with respect to f, ensuring commutativity between Γ-evaluation, residue field maps, and the morphism f.

Русский

Естественность Γ-оценки по отношению к f, обеспечивающая коммутативность между Γ-оценкой, резидуума-гомоморфизмами и гомоморфизмом f.

LaTeX

$$$ Y.\\Gamma\\mathrm{evaluation} (f.base x) \\circ \\mathrm{residueFieldMap} f x = f.c.app (op \\top) \\circ X.\\Gamma\\mathrm{evaluation} x $$$

Lean4

@[reassoc]
theorem Γevaluation_naturality (x : X) :
    Y.Γevaluation (f.base x) ≫ residueFieldMap f x = f.c.app (op ⊤) ≫ X.Γevaluation x :=
  evaluation_naturality f ⟨x, by simp only [Opens.map_top]; trivial⟩

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