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]