Theorems · Definition · algebraic geometry

AlgebraicGeometry.SpecMapRestrictBasicOpenIso

{R S : CommRingCat} →
  (f : R ⟶ S) →
    (r : ↑R) →
      CategoryTheory.Arrow.mk (AlgebraicGeometry.Spec.map f ∣_ PrimeSpectrum.basicOpen r) ≅
        CategoryTheory.Arrow.mk
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Localization.awayMap (CommRingCat.Hom.hom f) r)))

The restriction of Spec.map f to a basic open D(r) is isomorphic to Spec.map of the localization of f away from r.

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

Depth 147 from the axioms · uses propext, Classical.choice, Quot.sound