Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineSpace.map_SpecMap

∀ {n : Type u} {R S : CommRingCat} (φ : R ⟶ S),
  AlgebraicGeometry.AffineSpace.map n (AlgebraicGeometry.Spec.map φ) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n S).hom
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (MvPolynomial.map (CommRingCat.Hom.hom φ))))
        (AlgebraicGeometry.AffineSpace.SpecIso n R).inv)

Defined in

Mathlib.AlgebraicGeometry.AffineSpace

Cited by

0 results in Mathlib

Foundations

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