English
For f: R → S, the naturality square for toSpecΓ and Γ.map commutes: f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op.
Русский
Для гомоморфизма f: R → S диаграмма естественности между toSpecΓ и Γ.map сходится: f ∘ toSpecΓ(S) = toSpecΓ(R) ∘ Γ.map(Spec.toLocallyRingedSpace.map f^{op})^{op}.
LaTeX
$$$f \;\gg\; \mathrm{toSpec}\Gamma(S) = \mathrm{toSpec}\Gamma(R) \;\gg\; \Gamma.map\bigl( \mathrm{Spec.toLocallyRingedSpace.map}(f^{op}) \bigr)^{op}$$$
Lean4
@[reassoc]
theorem Spec_Γ_naturality {R S : CommRingCat.{u}} (f : R ⟶ S) :
f ≫ toSpecΓ S = toSpecΓ R ≫ Γ.map (Spec.toLocallyRingedSpace.map f.op).op := by
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11041): `ext` failed to pick up one of the three lemmas
ext : 2
refine Subtype.ext <| funext fun x' => ?_; symm
apply Localization.localRingHom_to_map
