map_fromSpec — Mathlib

English

For affine opens U ⊆ X and V ⊆ X with hU, hV affine, the Spec map intertwines the fromSpec morphisms along f: U ⟶ V; i.e., Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec.

Русский

Для аффинных открытых подмножеств U ⊆ X и V ⊆ X и соответствующих hU, hV, отображение Spec связывает fromSpec через f: U ⟶ V; то есть Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec.

LaTeX

$$Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec$$

Lean4

@[reassoc (attr := simp)]
theorem map_fromSpec {V : X.Opens} (hV : IsAffineOpen V) (f : op U ⟶ op V) :
    Spec.map (X.presheaf.map f) ≫ hU.fromSpec = hV.fromSpec :=
  by
  have : IsAffine U := hU
  haveI : IsAffine _ := hV
  conv_rhs =>
    rw [fromSpec, ← X.homOfLE_ι (V := U) f.unop.le, isoSpec_inv, Category.assoc, ← Scheme.isoSpec_inv_naturality_assoc,
      ← Spec.map_comp_assoc, Scheme.homOfLE_appTop, ← Functor.map_comp]
  rw [fromSpec, isoSpec_inv, Category.assoc, ← Spec.map_comp_assoc, ← Functor.map_comp]
  rfl

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