Documentation Verification Report

Basic

📁 Source: Mathlib/Geometry/RingedSpace/Basic.lean

Statistics

Metric	Count
Definitions `RingedSpace`, `basicOpen`, `instCoeSortType`, `zeroLocus`	4
Theorems `basicOpen_le`, `basicOpen_mul`, `basicOpen_of_isUnit`, `basicOpen_pow`, `basicOpen_res`, `basicOpen_res_eq`, `exists_res_eq_zero_of_germ_eq_zero`, `isUnit_of_isUnit_germ`, `isUnit_res_basicOpen`, `isUnit_res_of_isUnit_germ`, `mem_basicOpen`, `mem_basicOpen'`, `mem_top_basicOpen`, `mem_zeroLocus_iff`, `res_zero`, `zeroLocus_empty_eq_univ`, `zeroLocus_isClosed`, `zeroLocus_singleton`	18
Total	22

AlgebraicGeometry

Definitions

Name	Category	Theorems
`RingedSpace` 📖	CompOp	—

AlgebraicGeometry.RingedSpace

Definitions

Name	Category	Theorems
`basicOpen` 📖	CompOp	22 math math: `basicOpen_res`, `AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_iff_forall_evaluation_eq_zero`, `mem_top_basicOpen`, `basicOpen_pow`, `basicOpen_of_isUnit`, `mem_zeroLocus_iff`, `basicOpen_le`, `AlgebraicGeometry.LocallyRingedSpace.basicOpen_zero`, `basicOpen_mul`, `basicOpen_res_eq`, `isUnit_res_basicOpen`, `AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen`, `AlgebraicGeometry.LocallyRingedSpace.Γevaluation_eq_zero_iff_notMem_basicOpen`, `AlgebraicGeometry.LocallyRingedSpace.Γevaluation_ne_zero_iff_mem_basicOpen`, `AlgebraicGeometry.LocallyRingedSpace.evaluation_ne_zero_iff_mem_basicOpen`, `AlgebraicGeometry.LocallyRingedSpace.basicOpen_eq_bot_of_isNilpotent`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpecMapBasicOpen_eq`, `AlgebraicGeometry.LocallyRingedSpace.evaluation_eq_zero_iff_notMem_basicOpen`, `mem_basicOpen`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_basicOpen_eq`, `zeroLocus_singleton`, `mem_basicOpen'`
`instCoeSortType` 📖	CompOp	—
`zeroLocus` 📖	CompOp	5 math math: `zeroLocus_isClosed`, `mem_zeroLocus_iff`, `zeroLocus_empty_eq_univ`, `AlgebraicGeometry.LocallyRingedSpace.toΓSpec_preimage_zeroLocus_eq`, `zeroLocus_singleton`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`basicOpen_le` 📖	mathematical	—	`TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `basicOpen`	—	`CommRingCat.Colimits.hasColimits_commRingCat`
`basicOpen_mul` 📖	mathematical	—	`basicOpen` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `CommRingCat.commRing` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	`TopologicalSpace.Opens.ext` `Set.ext` `CommRingCat.Colimits.hasColimits_commRingCat` `mem_basicOpen` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `instIsDedekindFiniteMonoid` `basicOpen_le`
`basicOpen_of_isUnit` 📖	mathematical	`IsUnit` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	`basicOpen`	—	`le_antisymm` `basicOpen_le` `CommRingCat.Colimits.hasColimits_commRingCat` `mem_basicOpen` `RingHom.isUnit_map`
`basicOpen_pow` 📖	mathematical	—	`basicOpen` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`zero_add` `pow_one` `pow_add` `basicOpen_mul` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `instIsRightCancelAddOfAddRightReflectLE` `contravariant_swap_add_of_contravariant_add` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `instIsLeftCancelAddOfAddLeftReflectLE` `IsOrderedCancelAddMonoid.toAddLeftReflectLE` `Nat.instIsOrderedCancelAddMonoid` `contravariant_lt_of_covariant_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `covariant_swap_add_of_covariant_add` `Nat.instCanonicallyOrderedAdd` `inf_of_le_left` `instReflLe`
`basicOpen_res` 📖	mathematical	—	`basicOpen` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.Functor.map` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `TopologicalSpace.Opens.instCompleteLattice`	—	`TopologicalSpace.Opens.ext` `Set.ext` `CommRingCat.Colimits.hasColimits_commRingCat` `TopCat.Presheaf.germ_res_apply'`
`basicOpen_res_eq` 📖	mathematical	—	`basicOpen` `Opposite.unop` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.Functor.map`	—	`le_antisymm` `basicOpen_res` `inf_le_right` `CommRingCat.id_apply` `CategoryTheory.Functor.map_id` `CategoryTheory.IsIso.hom_inv_id` `CategoryTheory.Functor.map_comp` `CommRingCat.comp_apply`
`exists_res_eq_zero_of_germ_eq_zero` 📖	mathematical	`DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	`TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.carrier` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.Functor.map` `Quiver.Hom.op` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `TopCat.Presheaf.germ_eq` `CommRingCat.FilteredColimits.forget_preservesFilteredColimits`
`isUnit_of_isUnit_germ` 📖	mathematical	`IsUnit` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat` `CommRingCat.instCategory` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.carrier` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.PresheafedSpace.presheaf` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ`	`IsUnit` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `TopCat.Presheaf.section_ext` `CommRingCat.FilteredColimits.forget_preservesFilteredColimits` `CommRingCat.hasLimits` `CommRingCat.forget_preservesLimits` `CommRingCat.forgetReflectIsos` `TopCat.Presheaf.germ_res_apply` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `TopCat.Sheaf.existsUnique_gluing'` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid` `TopCat.Sheaf.eq_of_locally_eq'` `IsUnit.exists_right_inv` `isUnit_res_of_isUnit_germ`
`isUnit_res_basicOpen` 📖	mathematical	—	`IsUnit` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `basicOpen` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.Functor.map` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.homOfLE` `basicOpen_le`	—	`isUnit_of_isUnit_germ` `basicOpen_le` `CommRingCat.Colimits.hasColimits_commRingCat` `TopCat.Presheaf.germ_res_apply`
`isUnit_res_of_isUnit_germ` 📖	mathematical	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopologicalSpace.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `IsUnit` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.presheaf` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ`	`TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `IsUnit` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `CategoryTheory.Functor.map` `Quiver.Hom.op`	—	`CommRingCat.Colimits.hasColimits_commRingCat` `IsUnit.exists_right_inv` `TopCat.Presheaf.germ_exist` `CommRingCat.FilteredColimits.forget_preservesFilteredColimits` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `TopCat.Presheaf.germ_res_apply` `TopCat.Presheaf.germ_eq` `CategoryTheory.Functor.map_comp` `IsUnit.of_mul_eq_one` `instIsDedekindFiniteMonoid`
`mem_basicOpen` 📖	mathematical	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopologicalSpace.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike`	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopologicalSpace.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `basicOpen` `IsUnit` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.presheaf` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ`	—	`CommRingCat.Colimits.hasColimits_commRingCat`
`mem_basicOpen'` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopologicalSpace.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `basicOpen` `IsUnit` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.presheaf` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.germ`	—	`mem_basicOpen`
`mem_top_basicOpen` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopologicalSpace.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `basicOpen` `Top.top` `TopCat.str` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `IsUnit` `CommRingCat.carrier` `TopCat.Presheaf.stalk` `CommRingCat.Colimits.hasColimits_commRingCat` `AlgebraicGeometry.PresheafedSpace.presheaf` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `DFunLike.coe` `CategoryTheory.Functor.obj` `Opposite` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `CategoryTheory.ConcreteCategory.hom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `TopCat.Presheaf.Γgerm`	—	`mem_basicOpen`
`mem_zeroLocus_iff` 📖	mathematical	—	`TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `Set` `Set.instMembership` `zeroLocus` `TopologicalSpace.Opens` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `SetLike.instMembership` `TopologicalSpace.Opens.instSetLike` `basicOpen`	—	—
`res_zero` 📖	mathematical	`TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder`	`TopCat.Presheaf.restrictOpen` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `RingHom` `CommRingCat.carrier` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `RingHom.instFunLike` `CommRingCat.instConcreteCategoryRingHomCarrier` `AlgebraicGeometry.PresheafedSpace.presheaf` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `Opposite.op` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`zeroLocus_empty_eq_univ` 📖	mathematical	—	`zeroLocus` `Set` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Set.instEmptyCollection` `Set.univ`	—	`Set.iInter_congr_Prop` `Set.iInter_of_empty` `instIsEmptyFalse` `Set.iInter_univ`
`zeroLocus_isClosed` 📖	mathematical	—	`IsClosed` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `zeroLocus`	—	`isClosed_biInter` `TopologicalSpace.Opens.isOpen`
`zeroLocus_singleton` 📖	mathematical	—	`zeroLocus` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `Set` `Set.instSingletonSet` `Compl.compl` `Set.instCompl` `TopologicalSpace.Opens.carrier` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `basicOpen`	—	`Set.iInter_congr_Prop` `Set.iInter_iInter_eq_left`

---

← Back to Index