AffineSpace

📁 Source: Mathlib/AlgebraicGeometry/AffineSpace.lean

Statistics

Metric	Count
Definitions AffineSpace, SpecIso, coord, functor, homOfVector, homOverEquiv, isoOfIsAffine, map, mapSpecMap, over, reindex, toSpecMvPoly, toSpecMvPolyIntEquiv, «term𝔸(_;_)»»)	14
Theorems SpecIso_hom_appTop, SpecIso_inv_appTop_coord, SpecIso_inv_over, SpecIso_inv_over_assoc, comp_homOfVector, comp_homOfVector_assoc, functor_map_app, functor_obj_map, functor_obj_obj, homOfVector_appTop_coord, homOfVector_over, homOfVector_over_assoc, homOfVector_toSpecMvPoly, homOfVector_toSpecMvPoly_assoc, homOverEquiv_apply, homOverEquiv_symm_apply_coe, hom_ext, hom_ext_iff, instIsAffine, instIsAffineHomOverSchemeInferInstanceOverClass, instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty, instIsOverHomOfVectorOverSchemeInferInstanceOverClass, instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite, instSurjectiveOverSchemeInferInstanceOverClass, isIntegralHom_over_iff_isEmpty, isOpenMap_over, isPullback_map, isoOfIsAffine_hom, isoOfIsAffine_hom_appTop, isoOfIsAffine_inv, isoOfIsAffine_inv_appTop_coord, isoOfIsAffine_inv_over, isoOfIsAffine_inv_over_assoc, map_SpecMap, map_Spec_map, map_appTop_coord, map_comp, map_comp_assoc, map_id, map_over, map_over_assoc, map_reindex, map_reindex_assoc, map_toSpecMvPoly, map_toSpecMvPoly_assoc, not_isIntegralHom, of_mvPolynomial_int_ext, over_over, reindex_appTop_coord, reindex_comp, reindex_comp_assoc, reindex_id, reindex_over, reindex_over_assoc, spec_le_iff, toSpecMvPolyIntEquiv_apply, toSpecMvPolyIntEquiv_comp, toSpecMvPolyIntEquiv_symm_apply	58
Total	72

AlgebraicGeometry

Definitions

Name	Category	Theorems
AffineSpace 📖	CompOp	51 math math: AffineSpace.not_isIntegralHom, AffineSpace.map_Spec_map, AffineSpace.map_toSpecMvPoly_assoc, AffineSpace.map_reindex, AffineSpace.isoOfIsAffine_inv, AffineSpace.SpecIso_hom_appTop, AffineSpace.map_over_assoc, AffineSpace.homOverEquiv_symm_apply_coe, AffineSpace.isoOfIsAffine_inv_appTop_coord, AffineSpace.isoOfIsAffine_inv_over_assoc, AffineSpace.map_comp, AffineSpace.reindex_over, AffineSpace.map_over, AffineSpace.SpecIso_inv_appTop_coord, AffineSpace.instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite, AffineSpace.map_reindex_assoc, AffineSpace.instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty, AffineSpace.homOfVector_toSpecMvPoly_assoc, AffineSpace.comp_homOfVector, AffineSpace.isOpenMap_over, AffineSpace.hom_ext_iff, AffineSpace.map_toSpecMvPoly, AffineSpace.isPullback_map, AffineSpace.homOfVector_over_assoc, AffineSpace.reindex_comp, AffineSpace.map_SpecMap, AffineSpace.SpecIso_inv_over_assoc, AffineSpace.instIsAffineHomOverSchemeInferInstanceOverClass, AffineSpace.reindex_comp_assoc, AffineSpace.instIsOverHomOfVectorOverSchemeInferInstanceOverClass, AffineSpace.functor_obj_obj, AffineSpace.map_id, AffineSpace.isIntegralHom_over_iff_isEmpty, AffineSpace.functor_map_app, AffineSpace.instIsAffine, AffineSpace.map_comp_assoc, AffineSpace.homOfVector_over, AffineSpace.reindex_over_assoc, AffineSpace.isoOfIsAffine_hom_appTop, AffineSpace.isoOfIsAffine_hom, AffineSpace.reindex_appTop_coord, AffineSpace.homOverEquiv_apply, AffineSpace.over_over, AffineSpace.homOfVector_toSpecMvPoly, AffineSpace.SpecIso_inv_over, AffineSpace.isoOfIsAffine_inv_over, AffineSpace.instSurjectiveOverSchemeInferInstanceOverClass, AffineSpace.comp_homOfVector_assoc, AffineSpace.map_appTop_coord, AffineSpace.reindex_id, AffineSpace.homOfVector_appTop_coord
«term𝔸(_;_)» 📖» "API Documentation")	CompOp	—

AlgebraicGeometry.AffineSpace

Definitions

Name	Category	Theorems
SpecIso 📖	CompOp	6 math math: map_Spec_map, SpecIso_hom_appTop, SpecIso_inv_appTop_coord, map_SpecMap, SpecIso_inv_over_assoc, SpecIso_inv_over
coord 📖	CompOp	10 math math: SpecIso_hom_appTop, isoOfIsAffine_inv_appTop_coord, SpecIso_inv_appTop_coord, hom_ext_iff, isoOfIsAffine_hom_appTop, isoOfIsAffine_hom, reindex_appTop_coord, homOverEquiv_apply, map_appTop_coord, homOfVector_appTop_coord
functor 📖	CompOp	3 math math: functor_obj_map, functor_obj_obj, functor_map_app
homOfVector 📖	CompOp	10 math math: isoOfIsAffine_inv, homOverEquiv_symm_apply_coe, homOfVector_toSpecMvPoly_assoc, comp_homOfVector, homOfVector_over_assoc, instIsOverHomOfVectorOverSchemeInferInstanceOverClass, homOfVector_over, homOfVector_toSpecMvPoly, comp_homOfVector_assoc, homOfVector_appTop_coord
homOverEquiv 📖	CompOp	2 math math: homOverEquiv_symm_apply_coe, homOverEquiv_apply
isoOfIsAffine 📖	CompOp	6 math math: isoOfIsAffine_inv, isoOfIsAffine_inv_appTop_coord, isoOfIsAffine_inv_over_assoc, isoOfIsAffine_hom_appTop, isoOfIsAffine_hom, isoOfIsAffine_inv_over
map 📖	CompOp	15 math math: map_Spec_map, map_toSpecMvPoly_assoc, map_reindex, map_over_assoc, map_comp, map_over, functor_obj_map, map_reindex_assoc, map_toSpecMvPoly, isPullback_map, map_SpecMap, map_id, functor_map_app, map_comp_assoc, map_appTop_coord
mapSpecMap 📖	CompOp	—
over 📖	CompOp	26 math math: not_isIntegralHom, SpecIso_hom_appTop, map_over_assoc, homOverEquiv_symm_apply_coe, isoOfIsAffine_inv_over_assoc, reindex_over, map_over, instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite, instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty, isOpenMap_over, hom_ext_iff, isPullback_map, homOfVector_over_assoc, SpecIso_inv_over_assoc, instIsAffineHomOverSchemeInferInstanceOverClass, instIsOverHomOfVectorOverSchemeInferInstanceOverClass, isIntegralHom_over_iff_isEmpty, homOfVector_over, reindex_over_assoc, isoOfIsAffine_hom_appTop, isoOfIsAffine_hom, homOverEquiv_apply, over_over, SpecIso_inv_over, isoOfIsAffine_inv_over, instSurjectiveOverSchemeInferInstanceOverClass
reindex 📖	CompOp	9 math math: map_reindex, reindex_over, map_reindex_assoc, reindex_comp, reindex_comp_assoc, functor_map_app, reindex_over_assoc, reindex_appTop_coord, reindex_id
toSpecMvPoly 📖	CompOp	4 math math: map_toSpecMvPoly_assoc, homOfVector_toSpecMvPoly_assoc, map_toSpecMvPoly, homOfVector_toSpecMvPoly
toSpecMvPolyIntEquiv 📖	CompOp	5 math math: toSpecMvPolyIntEquiv_symm_apply, homOfVector_toSpecMvPoly_assoc, toSpecMvPolyIntEquiv_apply, toSpecMvPolyIntEquiv_comp, homOfVector_toSpecMvPoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
SpecIso_hom_appTop 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.appTop AlgebraicGeometry.AffineSpace AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CategoryTheory.Iso.hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory SpecIso CategoryTheory.CategoryStruct.comp CommRingCat CategoryTheory.Category.toCategoryStruct CommRingCat.instCategory CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.Scheme.ΓSpecIso CommRingCat.ofHom MvPolynomial.eval₂Hom CommRingCat.Hom.hom CategoryTheory.Iso.inv CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over coord	—	CommRingCat.hom_ext RingHom.ext AlgebraicGeometry.isAffine_Spec isoOfIsAffine_hom_appTop AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc MvPolynomial.eval₂_map
SpecIso_inv_appTop_coord 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.AffineSpace AlgebraicGeometry.Spec TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop CategoryTheory.Iso.inv AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory SpecIso coord AlgebraicGeometry.Scheme.ΓSpecIso MvPolynomial.X	—	AlgebraicGeometry.isAffine_Spec CommRingCat.comp_apply isoOfIsAffine_inv_appTop_coord AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality MvPolynomial.map_X
SpecIso_inv_over 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AlgebraicGeometry.AffineSpace CategoryTheory.Iso.inv SpecIso CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over AlgebraicGeometry.Spec.map CommRingCat.ofHom MvPolynomial.C	—	AlgebraicGeometry.isAffine_Spec CategoryTheory.Category.assoc isoOfIsAffine_inv_over AlgebraicGeometry.Scheme.isoSpec_Spec_inv CategoryTheory.Iso.inv_comp_eq CommRingCat.hom_ext RingHom.ext MvPolynomial.map_C
SpecIso_inv_over_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AlgebraicGeometry.AffineSpace CategoryTheory.Iso.inv SpecIso CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over AlgebraicGeometry.Spec.map CommRingCat.ofHom MvPolynomial.C	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' SpecIso_inv_over
comp_homOfVector 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace homOfVector CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop	—	hom_ext CategoryTheory.Category.assoc homOfVector_over homOfVector_appTop_coord
comp_homOfVector_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace homOfVector CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing CategoryTheory.ConcreteCategory.hom RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_homOfVector
functor_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace Opposite.unop map CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category functor reindex Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
functor_obj_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category functor map Opposite.unop	—	—
functor_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor CategoryTheory.Functor.category functor AlgebraicGeometry.AffineSpace Opposite.unop	—	—
homOfVector_appTop_coord 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.AffineSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop homOfVector coord	—	coord.eq_1 toSpecMvPolyIntEquiv_comp homOfVector_toSpecMvPoly Equiv.apply_symm_apply
homOfVector_over 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace homOfVector CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.instHasTerminalScheme
homOfVector_over_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace homOfVector CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfVector_over
homOfVector_toSpecMvPoly 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid homOfVector toSpecMvPoly DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSpecMvPolyIntEquiv	—	CategoryTheory.Limits.pullback.lift_snd AlgebraicGeometry.instHasTerminalScheme
homOfVector_toSpecMvPoly_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace homOfVector AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid toSpecMvPoly DFunLike.coe Equiv Quiver.Hom CategoryTheory.CategoryStruct.toQuiver EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSpecMvPolyIntEquiv	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' homOfVector_toSpecMvPoly
homOverEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace AlgebraicGeometry.Scheme.Hom.IsOver CategoryTheory.CanonicallyOverClass.toOverClass over EquivLike.toFunLike Equiv.instEquivLike homOverEquiv CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop coord	—	—
homOverEquiv_symm_apply_coe 📖	mathematical	—	Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace AlgebraicGeometry.Scheme.Hom.IsOver CategoryTheory.CanonicallyOverClass.toOverClass over DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm homOverEquiv homOfVector CategoryTheory.over CategoryTheory.OverClass	—	—
hom_ext 📖	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop coord	—	—	CategoryTheory.Limits.pullback.hom_ext AlgebraicGeometry.instHasTerminalScheme Equiv.injective toSpecMvPolyIntEquiv_comp
hom_ext_iff 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop coord	—	hom_ext
instIsAffine 📖	mathematical	—	AlgebraicGeometry.IsAffine AlgebraicGeometry.AffineSpace	—	AlgebraicGeometry.IsAffine.of_isIso CategoryTheory.Iso.isIso_hom AlgebraicGeometry.isAffine_Spec
instIsAffineHomOverSchemeInferInstanceOverClass 📖	mathematical	—	AlgebraicGeometry.IsAffineHom AlgebraicGeometry.AffineSpace CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.instHasTerminalScheme CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange AlgebraicGeometry.isAffineHom_isStableUnderBaseChange AlgebraicGeometry.isAffineHom_of_isAffine AlgebraicGeometry.isAffine_Spec AlgebraicGeometry.instIsAffineTerminalScheme
instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty 📖	mathematical	—	CategoryTheory.IsIso AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.instHasTerminalScheme CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange CategoryTheory.MorphismProperty.IsStableUnderBaseChange.isomorphisms CategoryTheory.Limits.terminal.comp_from CategoryTheory.MorphismProperty.IsStableUnderComposition.comp_mem CategoryTheory.MorphismProperty.HasTwoOutOfThreeProperty.toIsStableUnderComposition CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyIsomorphisms AlgebraicGeometry.HasAffineProperty.iff_of_isAffine AlgebraicGeometry.instHasAffinePropertyIsomorphismsSchemeAndIsAffineIsIsoCommRingCatAppTop AlgebraicGeometry.isAffine_Spec CategoryTheory.MorphismProperty.isomorphisms.eq_1 CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms CategoryTheory.ConcreteCategory.isIso_iff_bijective CommRingCat.forgetReflectIsos MvPolynomial.C_injective MvPolynomial.C_surjective CategoryTheory.Limits.isIso_of_isTerminal
instIsOverHomOfVectorOverSchemeInferInstanceOverClass 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.IsOver AlgebraicGeometry.AffineSpace homOfVector CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.comp_over homOfVector_over
instLocallyOfFinitePresentationOverSchemeInferInstanceOverClassOfFinite 📖	mathematical	—	AlgebraicGeometry.LocallyOfFinitePresentation AlgebraicGeometry.AffineSpace CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.instHasTerminalScheme CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange AlgebraicGeometry.locallyOfFinitePresentation_isStableUnderBaseChange CategoryTheory.Limits.isIso_of_isTerminal CategoryTheory.Limits.terminal.comp_from CategoryTheory.MorphismProperty.cancel_right_of_respectsIso CategoryTheory.MorphismProperty.IsLocalAtSource.toRespects AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtSource AlgebraicGeometry.instHasRingHomPropertyLocallyOfFinitePresentationFinitePresentation AlgebraicGeometry.HasRingHomProperty.Spec_iff RingHom.FinitePresentation.eq_1 Algebra.algebra_ext Algebra.FinitePresentation.mvPolynomial Algebra.FinitePresentation.self
instSurjectiveOverSchemeInferInstanceOverClass 📖	mathematical	—	AlgebraicGeometry.Surjective AlgebraicGeometry.AffineSpace CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.MorphismProperty.pullback_fst AlgebraicGeometry.instHasTerminalScheme CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange AlgebraicGeometry.Surjective.instIsStableUnderBaseChangeScheme CategoryTheory.Limits.isIso_of_isTerminal CategoryTheory.Limits.terminal.comp_from CategoryTheory.MorphismProperty.cancel_right_of_respectsIso AlgebraicGeometry.instRespectsIsoSchemeSurjective MvPolynomial.comap_C_surjective
isIntegralHom_over_iff_isEmpty 📖	mathematical	—	AlgebraicGeometry.IsIntegralHom AlgebraicGeometry.AffineSpace CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over IsEmpty TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace	—	isEmpty_or_nonempty subsingleton_or_nontrivial not_isEmpty_of_nonempty RingHom.toMorphismProperty_respectsIso_iff RingHom.isIntegral_respectsIso CategoryTheory.MorphismProperty.arrow_mk_iso_iff AlgebraicGeometry.HasAffineProperty.iff_of_isAffine AlgebraicGeometry.IsIntegralHom.hasAffineProperty AlgebraicGeometry.isAffine_Spec SpecIso_inv_over CategoryTheory.MorphismProperty.cancel_left_of_respectsIso CategoryTheory.MorphismProperty.IsLocalAtTarget.toRespects AlgebraicGeometry.Scheme.instHasPullbacksPrecoverageOfHasPullbacks AlgebraicGeometry.Scheme.instHasPullbacksIsOpenImmersion AlgebraicGeometry.HasAffineProperty.instIsZariskiLocalAtTarget CategoryTheory.Iso.isIso_inv Polynomial.algHom_eval₂_algebraMap MvPolynomial.rename_X EquivLike.toEmbeddingLike MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass map_eq_zero_iff AlgHom.algHomClass MvPolynomial.rename_injective AlgHom.comp_apply AlgebraicGeometry.Scheme.instJointlySurjectivePrecoverage AlgebraicGeometry.Scheme.Cover.covers CategoryTheory.MorphismProperty.IsStableUnderBaseChange.of_isPullback AlgebraicGeometry.IsIntegralHom.instIsStableUnderBaseChangeScheme isPullback_map AlgebraicGeometry.Scheme.local_affine AlgebraicGeometry.IsFinite.instIsIntegralHom AlgebraicGeometry.IsFinite.instOfIsClosedImmersion AlgebraicGeometry.IsClosedImmersion.instOfIsIsoScheme AlgebraicGeometry.isIso_of_isEmpty instIsIsoSchemeOverInferInstanceOverClassOfIsEmpty
isOpenMap_over 📖	mathematical	—	IsOpenMap TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.AffineSpace AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat TopCat.instCategory ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier AlgebraicGeometry.PresheafedSpace.Hom.base AlgebraicGeometry.LocallyRingedSpace.Hom.toHom AlgebraicGeometry.Scheme.Hom.toLRSHom' CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.MorphismProperty.cancel_left_of_respectsIso AlgebraicGeometry.instRespectsIsoSchemeTopologicallyIsOpenMap CategoryTheory.Iso.isIso_inv SpecIso_inv_over MvPolynomial.isOpenMap_comap_C AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.IsZariskiLocalAtTarget.iff_of_openCover AlgebraicGeometry.isOpenMap_isZariskiLocalAtTarget AlgebraicGeometry.Scheme.local_affine isPullback_map CategoryTheory.Iso.isIso_hom CategoryTheory.IsPullback.isoPullback_hom_snd
isPullback_map 📖	mathematical	—	CategoryTheory.IsPullback AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace map CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	AlgebraicGeometry.instHasTerminalScheme CategoryTheory.IsPullback.paste_horiz_iff CategoryTheory.IsPullback.flip CategoryTheory.IsPullback.of_hasPullback map_over CategoryTheory.Limits.terminal.comp_from toSpecMvPoly.eq_1 map_toSpecMvPoly
isoOfIsAffine_hom 📖	mathematical	—	CategoryTheory.Iso.hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid isoOfIsAffine CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.toSpecΓ AlgebraicGeometry.Spec.map CommRingCat.ofHom MvPolynomial.eval₂Hom CommRingCat.Hom.hom AlgebraicGeometry.Scheme.Hom.appTop CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over coord	—	—
isoOfIsAffine_hom_appTop 📖	mathematical	—	AlgebraicGeometry.Scheme.Hom.appTop AlgebraicGeometry.AffineSpace AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CategoryTheory.Iso.hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory isoOfIsAffine CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.ΓSpecIso CommRingCat.ofHom MvPolynomial.eval₂Hom CommRingCat.Hom.hom CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over coord	—	AlgebraicGeometry.Scheme.toSpecΓ_appTop AlgebraicGeometry.Scheme.ΓSpecIso_naturality
isoOfIsAffine_inv 📖	mathematical	—	CategoryTheory.Iso.inv AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid isoOfIsAffine homOfVector CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Spec.map CommRingCat.ofHom MvPolynomial.C AlgebraicGeometry.Scheme.isoSpec DFunLike.coe CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.ΓSpecIso MvPolynomial.X	—	—
isoOfIsAffine_inv_appTop_coord 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.AffineSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop CategoryTheory.Iso.inv AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory isoOfIsAffine coord AlgebraicGeometry.Scheme.ΓSpecIso MvPolynomial.X	—	homOfVector_appTop_coord
isoOfIsAffine_inv_over 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AlgebraicGeometry.AffineSpace CategoryTheory.Iso.inv isoOfIsAffine CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over AlgebraicGeometry.Spec.map CommRingCat.ofHom MvPolynomial.C AlgebraicGeometry.Scheme.isoSpec	—	CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.instHasTerminalScheme
isoOfIsAffine_inv_over_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of MvPolynomial CommRingCat.carrier CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AlgebraicGeometry.AffineSpace CategoryTheory.Iso.inv isoOfIsAffine CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over AlgebraicGeometry.Spec.map CommRingCat.ofHom MvPolynomial.C AlgebraicGeometry.Scheme.isoSpec	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoOfIsAffine_inv_over
map_SpecMap 📖	mathematical	—	map AlgebraicGeometry.Spec AlgebraicGeometry.Spec.map CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CategoryTheory.Iso.hom SpecIso CommRingCat.ofHom MvPolynomial.map CommRingCat.Hom.hom CategoryTheory.Iso.inv	—	CategoryTheory.Iso.inv_comp_eq hom_ext CategoryTheory.Category.assoc map_over SpecIso_inv_over_assoc SpecIso_inv_over MvPolynomial.map_comp_C CommRingCat.ofHom_comp CommRingCat.ofHom_hom CommRingCat.comp_apply map_appTop_coord SpecIso_inv_appTop_coord AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality CategoryTheory.ConcreteCategory.hom_ofHom MvPolynomial.map_X
map_Spec_map 📖	mathematical	—	map AlgebraicGeometry.Spec AlgebraicGeometry.Spec.map CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace CommRingCat.of MvPolynomial CommRingCat.carrier CommRing.toCommSemiring CommRingCat.commRing AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid CategoryTheory.Iso.hom SpecIso CommRingCat.ofHom MvPolynomial.map CommRingCat.Hom.hom CategoryTheory.Iso.inv	—	map_SpecMap
map_appTop_coord 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.AffineSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop map coord	—	homOfVector_appTop_coord
map_comp 📖	mathematical	—	map CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace	—	hom_ext map_over CategoryTheory.Category.assoc map_over_assoc map_appTop_coord
map_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_comp
map_id 📖	mathematical	—	map CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace	—	hom_ext CategoryTheory.comp_over map_over CategoryTheory.Category.comp_id CategoryTheory.instHomIsOverId map_appTop_coord
map_over 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace map CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.instHasTerminalScheme
map_over_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace map CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_over
map_reindex 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace map reindex	—	hom_ext CategoryTheory.Category.assoc CategoryTheory.comp_over reindex_over map_over CategoryTheory.comp_over_assoc reindex_appTop_coord map_appTop_coord
map_reindex_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace map reindex	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_reindex
map_toSpecMvPoly 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid map toSpecMvPoly	—	Equiv.injective toSpecMvPolyIntEquiv_comp coord.eq_1 map_appTop_coord
map_toSpecMvPoly_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace map AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid toSpecMvPoly	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_toSpecMvPoly
not_isIntegralHom 📖	mathematical	—	AlgebraicGeometry.IsIntegralHom AlgebraicGeometry.AffineSpace CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	—
of_mvPolynomial_int_ext 📖	—	DFunLike.coe CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid CommRingCat.carrier CategoryTheory.ConcreteCategory.hom CommRingCat CommRingCat.instCategory RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier MvPolynomial.X	—	—	MvPolynomial.ringHom_ext' RingHom.ext_int MvPolynomial.map_X CommRingCat.hom_ext RingHom.ext MvPolynomial.map_C DFunLike.congr_fun
over_over 📖	mathematical	—	CategoryTheory.over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over CategoryTheory.Limits.pullback.fst AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid CategoryTheory.Limits.terminal AlgebraicGeometry.instHasTerminalScheme CategoryTheory.Limits.terminal.from	—	AlgebraicGeometry.instHasTerminalScheme
reindex_appTop_coord 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.AffineSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop reindex coord	—	homOfVector_appTop_coord
reindex_comp 📖	mathematical	—	reindex CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace	—	hom_ext CategoryTheory.comp_over reindex_over CategoryTheory.Category.assoc reindex_appTop_coord
reindex_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace reindex	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' reindex_comp
reindex_id 📖	mathematical	—	reindex CategoryTheory.CategoryStruct.id AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace	—	hom_ext CategoryTheory.comp_over reindex_over CategoryTheory.instHomIsOverId reindex_appTop_coord
reindex_over 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace reindex CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.Limits.pullback.lift_fst AlgebraicGeometry.instHasTerminalScheme
reindex_over_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp AlgebraicGeometry.Scheme CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.AffineSpace reindex CategoryTheory.over CategoryTheory.OverClass CategoryTheory.CanonicallyOverClass.toOverClass over	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' reindex_over
spec_le_iff 📖	mathematical	—	TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace AlgebraicGeometry.Spec Preorder.toLE AlgebraicGeometry.Scheme.instPreorderCarrierCarrierCommRingCat Ideal CommRingCat.carrier CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing PartialOrder.toPreorder Submodule.instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule PrimeSpectrum.asIdeal	—	—
toSpecMvPolyIntEquiv_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike toSpecMvPolyIntEquiv CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop CategoryTheory.Iso.inv AlgebraicGeometry.Scheme.ΓSpecIso MvPolynomial.X	—	—
toSpecMvPolyIntEquiv_comp 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike toSpecMvPolyIntEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder CommRingCat.carrier CategoryTheory.ConcreteCategory.hom RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring CommRingCat.commRing RingHom.instFunLike CommRingCat.instConcreteCategoryRingHomCarrier AlgebraicGeometry.Scheme.Hom.appTop	—	—
toSpecMvPolyIntEquiv_symm_apply 📖	mathematical	—	DFunLike.coe Equiv Quiver.Hom AlgebraicGeometry.Scheme CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AlgebraicGeometry.Scheme.instCategory AlgebraicGeometry.Spec CommRingCat.of MvPolynomial ULift.commSemiring Int.instCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass ULift.commRing Int.instCommRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid EquivLike.toFunLike Equiv.instEquivLike Equiv.symm toSpecMvPolyIntEquiv CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens Top.top OrderTop.toTop Preorder.toLE SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice TopologicalSpace.Opens.instCompleteLattice AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder AlgebraicGeometry.Scheme.toSpecΓ AlgebraicGeometry.Spec.map CommRingCat.ofHom CommRingCat.carrier CommRingCat.commRing MvPolynomial.eval₂Hom CommRing.toCommSemiring RingHom.comp Semiring.toNonAssocSemiring CommSemiring.toSemiring algebraMap Ring.toIntAlgebra CommRing.toRing RingEquiv.toRingHom ULift.ringEquiv NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	—

---

← Back to Index