Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc

∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S] {Z : AlgebraicGeometry.Scheme}
  (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).inv
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S ↘ S) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C))
      (CategoryTheory.CategoryStruct.comp S.isoSpec.inv h)

Defined in

Mathlib.AlgebraicGeometry.AffineSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsAffine