fromSpec_top — Mathlib

English

For a scheme X that is affine, the fromSpec morphism for the entire space coincides with the inverse of the universal affine isomorphism X.isoSpec.inv.

Русский

Для аффинной схемы X отображение fromSpec для всей области совпадает с обратной стороной общего аффинного изоморфизма X.isoSpec.inv.

LaTeX

$$fromSpec_top [IsAffine X] : (isAffineOpen_top X).fromSpec = X.isoSpec.inv$$

Lean4

theorem fromSpec_top [IsAffine X] : (isAffineOpen_top X).fromSpec = X.isoSpec.inv := by
  rw [fromSpec, isoSpec_inv, Category.assoc, ← @Scheme.isoSpec_inv_naturality, ← Spec.map_comp_assoc,
    Scheme.Opens.ι_appTop, ← X.presheaf.map_comp, ← op_comp, eqToHom_comp_homOfLE, ← eqToHom_eq_homOfLE rfl,
    eqToHom_refl, op_id, X.presheaf.map_id, Spec.map_id, Category.id_comp]

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