ΓSpecIso_inv_naturality — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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