Structures · Geometry
AlgebraicGeometry.GeometricallyReduced
We say that morphism f : X ⟶ Y is geometrically reduced if for all Spec K ⟶ Y with K
a field, X ×[Y] Spec K is reduced.
- Shape
- One type argument · adds geometrically_isReduced
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by1
Forgetful instances
Provided automatically by
Concrete types that are instances4
- CategoryTheory.Limits.pullback
- AlgebraicGeometry.Scheme.Hom.fiber
- AlgebraicGeometry.Scheme.Opens.toScheme
- AlgebraicGeometry.AffineSpace
How is a type an instance?
Loading the hierarchy index…
Assumed by12
- AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian
- AlgebraicGeometry.smooth_of_grpObj
- AlgebraicGeometry.instGeometricallyReducedSndScheme
- AlgebraicGeometry.GeometricallyReduced.geometrically_isReduced
- AlgebraicGeometry.instGeometricallyReducedFstScheme
- AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents
- AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian
- AlgebraicGeometry.instGeometricallyReducedMorphismRestrict
- AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1
- AlgebraicGeometry.instIsReducedFiberOfGeometricallyReduced
- AlgebraicGeometry.instGeometricallyReducedFiberToSpecResidueField
- AlgebraicGeometry.GeometricallyIntegral.of_geometricallyReduced_of_geometricallyIrreducible
Ancestors0
No ancestors.