Geometrically Reduced Schemes

Main results

• 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. We also provide the fact that this is stable under base change (by infer_instance)
• GeometricallyReduced.iff_geometricallyReduced_fiber: A scheme is geometrically reduced over S iff the fibers of all s : S are geometrically reduced.
• AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian: If X is geometrically reduced and flat over a reduced and locally noetherian scheme, then X is also reduced. In particular, the base change of a geometrically reduced and flat scheme to an reduced and locally noetherian scheme is reduced (by infer_instance).

TODO

Get rid of the noetherian assumption.

class AlgebraicGeometry.GeometricallyReduced {X Y : Scheme} (f : X ⟶ Y) : Prop

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.

• geometrically_isReduced : geometrically IsReduced f

theorem AlgebraicGeometry.geometricallyReduced_iff {X Y : Scheme} (f : X ⟶ Y) : GeometricallyReduced f ↔ geometrically IsReduced f

theorem AlgebraicGeometry.GeometricallyReduced.eq_geometrically : @GeometricallyReduced = geometrically IsReduced

instance AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyReduced : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @GeometricallyReduced

instance AlgebraicGeometry.instGeometricallyReducedFstScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyReduced g] : GeometricallyReduced (CategoryTheory.Limits.pullback.fst f g)

instance AlgebraicGeometry.instGeometricallyReducedSndScheme {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyReduced f] : GeometricallyReduced (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.instGeometricallyReducedMorphismRestrict {X S : Scheme} (f : X ⟶ S) (V : S.Opens) [GeometricallyReduced f] : GeometricallyReduced (f ∣_ V)

instance AlgebraicGeometry.instGeometricallyReducedFiberToSpecResidueField {X S : Scheme} (f : X ⟶ S) (s : ↥S) [GeometricallyReduced f] : GeometricallyReduced (Scheme.Hom.fiberToSpecResidueField f s)

instance AlgebraicGeometry.instIsReducedFiberOfGeometricallyReduced {X S : Scheme} (f : X ⟶ S) (s : ↥S) [GeometricallyReduced f] : IsReduced (Scheme.Hom.fiber f s)

theorem AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_finite_irreducibleComponents {X Y : Scheme} (f : X ⟶ Y) [GeometricallyReduced f] [Flat f] [IsReduced Y] [Finite ↑(irreducibleComponents ↥Y)] : IsReduced X

theorem AlgebraicGeometry.GeometricallyReduced.isReduced_of_flat_of_isLocallyNoetherian {X Y : Scheme} (f : X ⟶ Y) [GeometricallyReduced f] [Flat f] [IsReduced Y] [IsLocallyNoetherian Y] : IsReduced X

instance AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyReduced f] [Flat f] [IsReduced Y] [IsLocallyNoetherian Y] : IsReduced (CategoryTheory.Limits.pullback f g)

If X is geometrically reduced over S, and Y is both reduced and locally noetherian, then X ×ₛ Y is also reduced.

TODO: get rid of the noetherian hypothesis.

instance AlgebraicGeometry.instIsReducedPullbackSchemeOfGeometricallyReducedOfFlatOfIsLocallyNoetherian_1 {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyReduced g] [Flat g] [IsReduced X] [IsLocallyNoetherian X] : IsReduced (CategoryTheory.Limits.pullback f g)