Theorems · Theorem · algebraic geometry

AlgebraicGeometry.AffineSpace.SpecIso_inv_over

∀ {n : Type u} (R : CommRingCat),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n R).inv
      (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)

Defined in: Mathlib.AlgebraicGeometry.AffineSpace
Cited by: 4 results in Mathlib
Foundations: Depth 177 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites39

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Quiver.Homstatement and proof · cited by 32,603
CategoryTheory.CategoryStruct.compstatement and proof · cited by 17,999
Top.topproof · cited by 9,680
CategoryTheory.Functor.mapproof · cited by 8,698
CategoryTheory.Iso.invstatement and proof · cited by 6,514
CategoryTheory.Category.assocproof · cited by 6,433
Finsuppstatement · cited by 5,255
AlgebraicGeometry.Schemestatement · cited by 2,540
CommRingCatstatement and proof · cited by 2,333
MvPolynomialstatement and proof · cited by 2,140
AlgebraicGeometry.SheafedSpace.toPresheafedSpaceproof · cited by 1,988
AlgebraicGeometry.LocallyRingedSpace.toSheafedSpaceproof · cited by 1,892

Cited by4

Results whose statement or proof uses this declaration.

AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assocproof · cited by 1
AlgebraicGeometry.AffineSpace.isOpenMap_overproof · cited by 0
AlgebraicGeometry.AffineSpace.map_SpecMapproof · cited by 0
AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmptyproof · cited by 0