Structures · Geometry
AlgebraicGeometry.IsReduced
A scheme X is reduced if all 𝒪ₓ(U) are reduced.
- Defined in
- Mathlib.AlgebraicGeometry.Properties
- Shape
- One type argument · adds component_reduced
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances7
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.Spec
- CategoryTheory.PreZeroHypercover.X
- AlgebraicGeometry.AffineSpace
- AlgebraicGeometry.Scheme.Hom.normalization
How is a type an instance?
Loading the hierarchy index…
Assumed by41
- AlgebraicGeometry.isReduced_of_isOpenImmersion
- AlgebraicGeometry.isIntegral_of_irreducibleSpace_of_isReduced
- AlgebraicGeometry.ext_of_isDominant_of_isSeparated
- AlgebraicGeometry.Scheme.RationalMap.toPartialMap
- AlgebraicGeometry.IsReduced.of_openCover
- AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff
- AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian
- AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated_of_le
- AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_isSeparated
- AlgebraicGeometry.isSchemeTheoreticallyDominant_iff_isDominant
- AlgebraicGeometry.ext_of_isDominant
- AlgebraicGeometry.isFinite_iff_locallyOfFiniteType_of_jacobsonSpace
- AlgebraicGeometry.ext_of_isDominant_of_isSeparated'
- AlgebraicGeometry.isIso_of_isClosedImmersion_of_surjective
- AlgebraicGeometry.Scheme.PartialMap.equiv_iff_of_domain_eq_of_isSeparated
- AlgebraicGeometry.IsSchemeTheoreticallyDominant.of_isDominant
- AlgebraicGeometry.isField_stalk_of_closure_mem_irreducibleComponents
- AlgebraicGeometry.Scheme.nilradical_eq_bot
- AlgebraicGeometry.IsSchemeTheoreticallyDominant.isReduced
- AlgebraicGeometry.basicOpen_eq_bot_iff
- AlgebraicGeometry.eq_zero_of_basicOpen_eq_bot
- AlgebraicGeometry.Scheme.PartialMap.toPartialMap_toRationalMap_restrict
- AlgebraicGeometry.ext_of_fromSpecResidueField_eq
- AlgebraicGeometry.ext_of_apply_eq
- AlgebraicGeometry.Scheme.PartialMap.equiv_toPartialMap_iff_of_isSeparated
- AlgebraicGeometry.instIsReducedXScheme
- AlgebraicGeometry.AffineSpace.instIsReduced
- AlgebraicGeometry.isReduced_stalk_of_isReduced
- AlgebraicGeometry.instIsArtinianSchemeOfSubsingletonCarrierCarrierCommRingCatOfIsReduced
- AlgebraicGeometry.Scheme.instIsOverToPartialMapOfIsSeparatedOfIsOver
- AlgebraicGeometry.instIsLocallyArtinianOfDiscreteTopologyCarrierCarrierCommRingCatOfIsReduced
- AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents
- AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian
- AlgebraicGeometry.Scheme.PartialMap.isOver_toRationalMap_iff_of_isSeparated
- AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1
- AlgebraicGeometry.IsReduced.component_reduced
- AlgebraicGeometry.instIsReducedToScheme
- AlgebraicGeometry.Scheme.RationalMap.toPartialMap.congr_simp
- AlgebraicGeometry.Scheme.Hom.instIsReducedNormalization
- AlgebraicGeometry.Scheme.RationalMap.toRationalMap_toPartialMap
- AlgebraicGeometry.Scheme.Hom.dense_smoothLocus_of_perfectField
Ancestors0
No ancestors.