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 MvPolynomial.instCommRingMvPolynomial 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	—	AlgebraicGeometry.isAffine_Spec isoOfIsAffine_hom_appTop AlgebraicGeometry.Scheme.ΓSpecIso_naturality_assoc CommRingCat.hom_ext MvPolynomial.ringHom_ext' RingHom.ext MvPolynomial.map_C MvPolynomial.eval₂_C MvPolynomial.eval₂Hom_comp_C MvPolynomial.map_X MvPolynomial.eval₂_X MvPolynomial.eval₂Hom_X'
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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 RingHom.instFunLike CategoryTheory.ConcreteCategory.hom 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 PrimeSpectrum.instIsEmptyOfSubsingleton 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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	—	CategoryTheory.comp_over reindex_over CategoryTheory.Category.assoc reindex_appTop_coord hom_ext
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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 MvPolynomial.instCommRingMvPolynomial ULift.commRing Int.instCommRing 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 NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring	—	—

---

← Back to Index