Geometrically Integral Schemes

Main results

• AlgebraicGeometry.GeometricallyIntegral: We say that morphism f : X ⟶ Y is geometrically integral if for all Spec K ⟶ Y with K a field, X ×[Y] Spec K is integral. We also provide the fact that this is stable under base change (by infer_instance)
• GeometricallyIntegral.iff_geometricallyIntegral_fiber: A scheme is geometrically integral over S iff the fibers of all s : S are geometrically integral.
• AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_isLocallyNoetherian: If X is geometrically integral, flat, and universally open (e.g. when over a field), over an integral locally noetherian scheme, then X is also integral.
• AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_subsingleton: If X is geometrically integral over a field, then it is integral.

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

We say that morphism f : X ⟶ Y is geometrically integral if for all Spec K ⟶ Y with K a field, X ×[Y] Spec K is integral.

• geometrically_isIntegral : geometrically IsIntegral f

theorem AlgebraicGeometry.geometricallyIntegral_iff {X Y : Scheme} (f : X ⟶ Y) : GeometricallyIntegral f ↔ geometrically IsIntegral f

theorem AlgebraicGeometry.GeometricallyIntegral.eq_geometrically : @GeometricallyIntegral = geometrically IsIntegral

theorem AlgebraicGeometry.GeometricallyIntegral.eq_geometricallyReduced_inf_geometricallyIrreducible : @GeometricallyIntegral = @GeometricallyReduced ⊓ @GeometricallyIrreducible

@[instance 100]

instance AlgebraicGeometry.instGeometricallyReducedOfGeometricallyIntegral {X S : Scheme} (f : X ⟶ S) [GeometricallyIntegral f] : GeometricallyReduced f

@[instance 100]

instance AlgebraicGeometry.instGeometricallyIrreducibleOfGeometricallyIntegral {X S : Scheme} (f : X ⟶ S) [GeometricallyIntegral f] : GeometricallyIrreducible f

theorem AlgebraicGeometry.GeometricallyIntegral.of_geometricallyReduced_of_geometricallyIrreducible {X S : Scheme} (f : X ⟶ S) [GeometricallyReduced f] [GeometricallyIrreducible f] : GeometricallyIntegral f

instance AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIntegral : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @GeometricallyIntegral

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

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

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

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

instance AlgebraicGeometry.instIsIntegralFiberOfGeometricallyIntegral {X S : Scheme} (f : X ⟶ S) (s : ↥S) [GeometricallyIntegral f] : IsIntegral (Scheme.Hom.fiber f s)

@[instance 100]

instance AlgebraicGeometry.instSurjectiveOfGeometricallyIntegral {X S : Scheme} (f : X ⟶ S) [GeometricallyIntegral f] : Surjective f

theorem AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_isLocallyNoetherian {X S : Scheme} (f : X ⟶ S) [GeometricallyIntegral f] [Flat f] [UniversallyOpen f] [IsIntegral S] [IsLocallyNoetherian S] : IsIntegral X

theorem AlgebraicGeometry.GeometricallyIntegral.isIntegral_of_subsingleton {X S : Scheme} (f : X ⟶ S) [GeometricallyIntegral f] [Subsingleton ↥S] [IsIntegral S] : IsIntegral X

If X is geometrically integral over a field, then it is integral.

instance AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyIntegral f] [Flat f] [UniversallyOpen f] [IsIntegral Y] [IsLocallyNoetherian Y] : IsIntegral (CategoryTheory.Limits.pullback f g)

If X is geometrically integral and flat and universally open over S and Y is integral and locally noetherian, then X ×ₛ Y is integral.

instance AlgebraicGeometry.instIsIntegralPullbackSchemeOfGeometricallyIntegralOfFlatOfUniversallyOpenOfIsLocallyNoetherian_1 {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyIntegral g] [Flat g] [UniversallyOpen g] [IsIntegral X] [IsLocallyNoetherian X] : IsIntegral (CategoryTheory.Limits.pullback f g)

theorem AlgebraicGeometry.GeometricallyIntegral.iff_geometricallyIntegral_fiber {X S : Scheme} (f : X ⟶ S) : GeometricallyIntegral f ↔ ∀ (s : ↥S), GeometricallyIntegral (Scheme.Hom.fiberToSpecResidueField f s)