isoSpec_hom_naturality — Mathlib

English

For any morphism f: X → Y between affine schemes, the natural square involving isoSpec is commutative with Spec.map on topological maps.

Русский

Для любых Морфизмов f: X → Y между аффинными схемами диаграмма естественности isoSpec сохраняет commute через Spec.map на верхнем уровне.

LaTeX

$$$X.isoSpec.hom \\;\\circ\\; \\mathrm{Spec.map}(f_{\\mathrm{top}}) = f \\;\\circ\\; Y.isoSpec.hom$$$

Lean4

@[reassoc]
theorem isoSpec_hom_naturality {X Y : Scheme} [IsAffine X] [IsAffine Y] (f : X ⟶ Y) :
    X.isoSpec.hom ≫ Spec.map (f.appTop) = f ≫ Y.isoSpec.hom := by
  simp only [isoSpec, asIso_hom, Scheme.toSpecΓ_naturality]

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