Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop

∀ {n : Type u} (R : CommRingCat),
  AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.AffineSpace.SpecIso n R).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).hom
      (CommRingCat.ofHom
        (MvPolynomial.eval₂Hom
          (CommRingCat.Hom.hom
            (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
              (AlgebraicGeometry.Scheme.Hom.appTop
                (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R))))
          (AlgebraicGeometry.AffineSpace.coord (AlgebraicGeometry.Spec R))))

Defined in

Mathlib.AlgebraicGeometry.AffineSpace

Cited by

0 results in Mathlib

Foundations

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