Reduced

📁 Source: Mathlib/AlgebraicGeometry/Geometrically/Reduced.lean

Statistics

Metric	Count
Definitions	0
Theorems eq_geometrically, geometrically_isReduced, isReduced_of_flat_of_finite_irreducibleComponents, isReduced_of_flat_of_isLocallyNoetherian, geometricallyReduced_iff, instGeometricallyReducedFiberToSpecResidueField, instGeometricallyReducedFstScheme, instGeometricallyReducedMorphismRestrict, instGeometricallyReducedSndScheme, instIsReducedFiberOfGeometricallyReduced, instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian, instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1, instIsStableUnderBaseChangeSchemeGeometricallyReduced	13
Total	13

AlgebraicGeometry

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
geometricallyReduced_iff 📖	mathematical	—	GeometricallyReduced geometrically IsReduced	—	—
instGeometricallyReducedFiberToSpecResidueField 📖	mathematical	—	GeometricallyReduced Scheme.Hom.fiber Spec Scheme.residueField Scheme.Hom.fiberToSpecResidueField	—	CategoryTheory.MorphismProperty.pullback_snd CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyReduced
instGeometricallyReducedFstScheme 📖	mathematical	—	GeometricallyReduced CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.fst	—	CategoryTheory.MorphismProperty.pullback_fst Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyReduced
instGeometricallyReducedMorphismRestrict 📖	mathematical	—	GeometricallyReduced Scheme.Opens.toScheme CategoryTheory.Functor.obj Scheme.Opens Preorder.smallCategory TopologicalSpace.Opens TopCat.carrier PresheafedSpace.carrier CommRingCat CommRingCat.instCategory SheafedSpace.toPresheafedSpace LocallyRingedSpace.toSheafedSpace Scheme.toLocallyRingedSpace TopCat.str PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder TopologicalSpace.Opens.map PresheafedSpace.Hom.base LocallyRingedSpace.Hom.toHom Scheme.Hom.toLRSHom' morphismRestrict	—	CategoryTheory.MorphismProperty.of_isPullback instIsStableUnderBaseChangeSchemeGeometricallyReduced CategoryTheory.IsPullback.flip isPullback_morphismRestrict
instGeometricallyReducedSndScheme 📖	mathematical	—	GeometricallyReduced CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback CategoryTheory.Limits.pullback.snd	—	CategoryTheory.MorphismProperty.pullback_snd Scheme.Pullback.instHasPullback CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange instIsStableUnderBaseChangeSchemeGeometricallyReduced
instIsReducedFiberOfGeometricallyReduced 📖	mathematical	—	IsReduced Scheme.Hom.fiber	—	GeometricallyReduced.geometrically_isReduced CommRingCat.Colimits.hasColimits_commRingCat CategoryTheory.IsPullback.of_hasPullback
instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian 📖	mathematical	—	IsReduced CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback	—	GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian Scheme.Pullback.instHasPullback instGeometricallyReducedSndScheme Flat.instSndScheme
instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1 📖	mathematical	—	IsReduced CategoryTheory.Limits.pullback Scheme Scheme.instCategory Scheme.Pullback.instHasPullback	—	GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian Scheme.Pullback.instHasPullback instGeometricallyReducedFstScheme Flat.instFstScheme
instIsStableUnderBaseChangeSchemeGeometricallyReduced 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange Scheme Scheme.instCategory GeometricallyReduced	—	instIsStableUnderBaseChangeSchemeGeometrically GeometricallyReduced.eq_geometrically

AlgebraicGeometry.GeometricallyReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_geometrically 📖	mathematical	—	AlgebraicGeometry.GeometricallyReduced AlgebraicGeometry.geometrically AlgebraicGeometry.IsReduced	—	AlgebraicGeometry.geometricallyReduced_iff
geometrically_isReduced 📖	mathematical	—	AlgebraicGeometry.geometrically AlgebraicGeometry.IsReduced	—	—
isReduced_of_flat_of_finite_irreducibleComponents 📖	mathematical	—	AlgebraicGeometry.IsReduced	—	CommRingCat.Colimits.hasColimits_commRingCat AlgebraicGeometry.instQuasiSoberCarrierCarrierCommRingCat AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponents IsIrreducible.closure_genericPoint isClosed_of_mem_irreducibleComponents AlgebraicGeometry.Scheme.IsLocallyDirected.instHasColimit AlgebraicGeometry.IsOpenImmersion.of_isIso CategoryTheory.Functor.map_isIso CategoryTheory.Discrete.instIsIso CategoryTheory.instIsLocallyDirectedDiscrete CategoryTheory.Discrete.instSubsingletonDiscreteHom CategoryTheory.instSmallDiscrete small_subtype small_set UnivLE.small UnivLE.self Equiv.finite_iff Finite.instSigma AlgebraicGeometry.IsArtinianScheme.finite AlgebraicGeometry.instIsArtinianSchemeSpecOfIsArtinianRingCarrier instIsArtinianOfIsSemisimpleModuleOfFinite IsSemisimpleRing.isSemisimpleModule instIsSemisimpleModuleOfIsSimpleModule instIsSimpleModule FiniteDimensional.finiteDimensional_self Set.Finite.isCompact Set.toFinite Subtype.finite AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isDominant AlgebraicGeometry.isDominant_iff denseRange_iff_closure_range Set.eq_univ_iff_forall irreducibleComponent_mem_irreducibleComponents AlgebraicGeometry.LocallyRingedSpace.instIsLocalRingCarrierStalkCommRingCatPresheaf CategoryTheory.Limits.Sigma.ι_desc AlgebraicGeometry.Scheme.fromSpecStalk_closedPoint IsGenericPoint.specializes IsIrreducible.isGenericPoint_genericPoint isClosed_irreducibleComponent mem_irreducibleComponent Specializes.mem_closed isClosed_closure subset_closure AlgebraicGeometry.Scheme.Pullback.instHasPullback CategoryTheory.IsUniversalColimit.isPullback_of_isColimit_left CategoryTheory.FinitaryPreExtensive.isUniversal_finiteCoproducts CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive AlgebraicGeometry.instFinitaryExtensiveScheme CategoryTheory.IsPullback.of_hasPullback CategoryTheory.Limits.colimit.ι_desc AlgebraicGeometry.isReduced_of_isOpenImmersion CategoryTheory.Iso.isIso_inv AlgebraicGeometry.IsReduced.of_openCover geometrically_isReduced AlgebraicGeometry.IsSchemeTheoreticallyDominant.isReduced AlgebraicGeometry.IsSchemeTheoreticallyDominant.pullbackFst AlgebraicGeometry.instQuasiCompactFstScheme
isReduced_of_flat_of_isLocallyNoetherian 📖	mathematical	—	AlgebraicGeometry.IsReduced	—	AlgebraicGeometry.IsReduced.of_openCover AlgebraicGeometry.Scheme.instIsStableUnderBaseChangePrecoverageOfIsJointlySurjectivePreservingOfIsStableUnderBaseChange AlgebraicGeometry.Scheme.instIsJointlySurjectivePreservingIsOpenImmersion AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange AlgebraicGeometry.Scheme.Pullback.instHasPullback AlgebraicGeometry.isReduced_of_isOpenImmersion AlgebraicGeometry.Scheme.instIsOpenImmersionF AlgebraicGeometry.instIsLocallyNoetherianXScheme AlgebraicGeometry.Scheme.compactSpace_of_isAffine AlgebraicGeometry.Scheme.isAffine_affineCover TopologicalSpace.NoetherianSpace.finite_irreducibleComponents AlgebraicGeometry.IsNoetherian.noetherianSpace isReduced_of_flat_of_finite_irreducibleComponents AlgebraicGeometry.instGeometricallyReducedSndScheme AlgebraicGeometry.Flat.instSndScheme

---

← Back to Index