instIsIsoSchemeMapOfCommRingCat — Mathlib

English

If f: R → S is an isomorphism of commutative rings, then the induced morphism Spec.map f is an isomorphism of schemes.

Русский

Если f: R → S — изоморфизм колец, то индуцированное отображение Spec.map f — изоморфизм схем.

LaTeX

$$$\\mathrm{IsIso}(\\mathrm{Spec.map}\\, f)$$$

Lean4

instance {R S : CommRingCat} (f : R ⟶ S) [IsIso f] : IsIso (Spec.map f) :=
  inferInstanceAs (IsIso <| Scheme.Spec.map f.op)

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