ΓSpecIso_naturality — Mathlib

English

Natural compatibility of ΓSpecIso with Spec.map on appTop.

Русский

Естественная совместимость ΓSpecIso с отображением Spec.map на appTop.

LaTeX

$$$ (\mathrm{Spec.map} f).\mathrm{appTop} ≫ (\GammaSpecIso S).\mathrm{hom} = (\GammaSpecIso R).\mathrm{hom} ≫ f. $$$

Lean4

@[reassoc (attr := simp)]
theorem ΓSpecIso_naturality {R S : CommRingCat.{u}} (f : R ⟶ S) :
    (Spec.map f).appTop ≫ (ΓSpecIso S).hom = (ΓSpecIso R).hom ≫ f :=
  SpecΓIdentity.hom.naturality f

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