Documentation Verification Report

PointsPi

📁 Source: Mathlib/AlgebraicGeometry/PointsPi.lean

Statistics

Metric	Count
Definitions `pointsPi`	1
Theorems `span_eq_top_of_span_image_evalRingHom`, `eq_bot_of_comp_quotientMk_eq_sigmaSpec`, `eq_top_of_sigmaSpec_subset_of_isCompact`, `isIso_of_comp_eq_sigmaSpec`, `pointsPi_injective`, `pointsPi_surjective`, `pointsPi_surjective_of_isAffine`	7
Total	8

AlgebraicGeometry

Definitions

Name	Category	Theorems
`pointsPi` 📖	CompOp	3 math math: `pointsPi_surjective_of_isAffine`, `pointsPi_injective`, `pointsPi_surjective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_bot_of_comp_quotientMk_eq_sigmaSpec` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Spec` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `CommRingCat.of` `HasQuotient.Quotient` `Ideal` `Pi.semiring` `CommRingCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing` `Ideal.instHasQuotient_1` `Pi.commRing` `Ideal.Quotient.commRing` `Spec.map` `CommRingCat.ofHom` `Pi.ring` `CommRing.toRing` `Ideal.instIsTwoSided_1` `sigmaSpec`	`Bot.bot` `Submodule.instBot` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Semiring.toModule`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `Ideal.instIsTwoSided_1` `le_bot_iff` `ι_sigmaSpec` `Spec.preimage_map` `Spec.preimage_comp` `Ideal.Quotient.eq_zero_iff_mem` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass`
`eq_top_of_sigmaSpec_subset_of_isCompact` 📖	mathematical	`Set` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `Spec` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `Set.instHasSubset` `SetLike.coe` `Scheme.Opens` `TopologicalSpace.Opens.instSetLike` `SheafedSpace.instTopologicalSpaceCarrierCarrier` `Scheme.Hom.opensRange` `CategoryTheory.Limits.sigmaObj` `Scheme` `Scheme.instCategory` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `sigmaSpec` `instIsOpenImmersionSigmaSpec` `IsCompact`	`Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `TopologicalSpace.Opens.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instIsOpenImmersionSigmaSpec` `PrimeSpectrum.isOpen_iff` `TopologicalSpace.Opens.is_open'` `IsCompact.elim_finite_subcover` `PrimeSpectrum.basicOpen_eq_zeroLocus_compl` `Set.iInter_coe_set` `Set.iInter_congr_Prop` `PrimeSpectrum.zeroLocus_iUnion₂` `Set.biUnion_of_singleton` `compl_compl` `Finset.coe_map` `Set.image_congr` `Subtype.coe_preimage_self` `Finset.finite_toSet` `Set.iUnion_congr_Prop` `Set.iUnion_exists` `Set.iUnion_coe_set` `PrimeSpectrum.zeroLocus_empty_iff_eq_top` `PrimeSpectrum.zeroLocus_span` `PrimeSpectrum.preimage_comap_zeroLocus` `Set.compl_univ_iff` `Set.preimage_compl` `Set.preimage_eq_univ_iff` `IsOpenImmersion.comp` `Scheme.IsLocallyDirected.instIsOpenImmersionι` `ι_sigmaSpec` `Scheme.Hom.opensRange.congr_simp` `subset_refl` `Set.instReflSubset` `Scheme.Hom.opensRange_comp` `HasSubset.Subset.trans` `Set.instIsTransSubset` `Set.image_subset_range` `top_le_iff` `LE.le.trans` `Eq.ge` `Ideal.span_eq_top_of_span_image_evalRingHom` `Ideal.span_mono`
`isIso_of_comp_eq_sigmaSpec` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `Scheme` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `CategoryTheory.Limits.sigmaObj` `Spec` `Scheme.IsLocallyDirected.instHasColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Discrete.functor` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.map` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Functor.comp` `CategoryTheory.types` `Scheme.forget` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `sigmaSpec`	`CategoryTheory.IsIso`	—	`Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `univLE_of_max` `instIsOpenImmersionSigmaSpec` `eq_top_of_sigmaSpec_subset_of_isCompact` `subset_coborder` `Scheme.Hom.opensRange.congr_simp` `Set.range_comp_subset_range` `isCompact_range` `Scheme.Hom.continuous` `Scheme.topIso_hom` `CategoryTheory.Iso.isIso_hom` `Scheme.Hom.liftCoborder_ι` `IsClosedImmersion.comp` `instIsClosedImmersionLiftCoborder` `IsClosedImmersion.instOfIsIsoScheme` `Ideal.instIsTwoSided_1` `IsClosedImmersion.Spec_iff` `CategoryTheory.IsIso.comp_isIso` `instIsIsoSchemeMapOfCommRingCat` `CategoryTheory.Iso.isIso_inv` `eq_bot_of_comp_quotientMk_eq_sigmaSpec` `CategoryTheory.Category.assoc`
`pointsPi_injective` 📖	mathematical	—	`Quiver.Hom` `Scheme` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `pointsPi`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_of_hasFiniteLimits` `instHasFiniteLimitsScheme` `isIso_of_comp_eq_sigmaSpec` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `UnivLE.self` `CategoryTheory.Limits.Sigma.hom_ext` `ι_sigmaSpec_assoc` `IsImmersion.instιScheme` `instCompactSpaceCarrierCarrierCommRingCatEqualizerSchemeOfQuasiSeparatedSpace` `Scheme.compactSpace_of_isAffine` `isAffine_Spec` `univLE_of_max` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Limits.equalizer.condition`
`pointsPi_surjective` 📖	mathematical	`IsLocalRing` `CommRingCat.carrier` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommRingCat.commRing`	`Quiver.Hom` `Scheme` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CommRingCat.of` `Pi.commRing` `pointsPi`	—	`Scheme.instIsOpenImmersionF` `Scheme.instJointlySurjectivePrecoverage` `Specializes.mem_open` `Specializes.map` `IsLocalRing.specializes_closedPoint` `Scheme.Hom.continuous` `TopologicalSpace.Opens.is_open'` `Scheme.Cover.covers` `pointsPi_surjective_of_isAffine` `instIsAffineXSchemeFiniteSubcover` `Scheme.isAffine_affineCover` `Scheme.IsLocallyDirected.instHasColimit` `IsOpenImmersion.of_isIso` `CategoryTheory.Functor.map_isIso` `CategoryTheory.Discrete.instIsIso` `CategoryTheory.instIsLocallyDirectedDiscrete` `CategoryTheory.Discrete.instSubsingletonDiscreteHom` `CategoryTheory.instSmallDiscrete` `UnivLE.small` `univLE_of_max` `UnivLE.self` `instIsIsoSchemeSigmaSpecOfFinite` `Finite.of_fintype` `pointsPi.eq_1` `Spec.map_comp_assoc` `CommRingCat.ofHom_comp` `ι_sigmaSpec` `CategoryTheory.Category.assoc` `CategoryTheory.IsIso.hom_inv_id_assoc` `CategoryTheory.Limits.Sigma.ι_desc` `IsOpenImmersion.lift_fac`
`pointsPi_surjective_of_isAffine` 📖	mathematical	—	`Quiver.Hom` `Scheme` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `Scheme.instCategory` `Spec` `CommRingCat.of` `Pi.commRing` `CommRingCat.carrier` `CommRingCat.commRing` `pointsPi`	—	`Spec.map_preimage`

AlgebraicGeometry.Ideal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`span_eq_top_of_span_image_evalRingHom` 📖	mathematical	`Ideal.span` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Set.image` `DFunLike.coe` `RingHom` `Pi.nonAssocSemiring` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `Pi.evalRingHom` `Top.top` `Ideal` `Submodule.instTop` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toModule`	`Pi.semiring`	—	`Subtype.range_val` `Finite.of_fintype` `Finsupp.sum_fintype` `MulZeroClass.zero_mul` `Finset.sum_congr` `Finset.sum_apply`

---

← Back to Index