Theorems · Definition · algebraic geometry

AlgebraicGeometry.AffineSpace.mapSpecMap

{n : Type u} →
  {R S : CommRingCat} →
    (φ : R ⟶ S) →
      CategoryTheory.Arrow.mk (AlgebraicGeometry.AffineSpace.map n (AlgebraicGeometry.Spec.map φ)) ≅
        CategoryTheory.Arrow.mk
          (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))

The map between affine spaces over affine bases is isomorphic to the natural map between polynomial rings.

Defined in

Mathlib.AlgebraicGeometry.AffineSpace

Cited by

0 results in Mathlib

Foundations

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