map_inv — Mathlib

English

As above, the induced map on spectra is an isomorphism when f is an isomorphism of rings.

Русский

Как и выше, индуцированное отображение на спектрах является изоморфизмом, если f — изоморфизм колец.

LaTeX

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

Lean4

@[simp]
theorem map_inv {R S : CommRingCat} (f : R ⟶ S) [IsIso f] : Spec.map (inv f) = inv (Spec.map f) :=
  by
  change Scheme.Spec.map (inv f).op = inv (Scheme.Spec.map f.op)
  rw [op_inv, ← Scheme.Spec.map_inv]

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