isoSpec_Spec_hom — Mathlib

English

The hom component of the isoSpec of R equals the map on Spec induced by ΓSpecIso.

Русский

Гом-компонент isoSpec равен отображению на Spec, индуцируемому ΓSpecIso.

LaTeX

$$$(\\Spec R).isoSpec.hom = \\mathrm{Spec.map}( (\\mathrm{Scheme.}\\mathrm{ΓSpecIso} R) ).hom$$$

Lean4

@[simp]
theorem isoSpec_Spec_hom (R : CommRingCat.{u}) : (Spec R).isoSpec.hom = Spec.map (Scheme.ΓSpecIso R).hom :=
  (SpecMap_ΓSpecIso_hom R).symm

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