Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom

∀ (n : Type u) (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S],
  (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S).toSpecΓ
      (AlgebraicGeometry.Spec.map
        (CommRingCat.ofHom
          (MvPolynomial.eval₂Hom
            (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace n S ↘ S)))
            (AlgebraicGeometry.AffineSpace.coord S))))

Defined in

Mathlib.AlgebraicGeometry.AffineSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

AlgebraicGeometry.IsAffine