Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop

∀ {n : Type u} (S : AlgebraicGeometry.Scheme) [inst : AlgebraicGeometry.IsAffine S],
  AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.isoOfIsAffine n S).hom =
    CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑(S.presheaf.obj (Opposite.op ⊤))))).hom
      (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 177 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AlgebraicGeometry.IsAffine