Geometrically Irreducible Schemes

Main results

• AlgebraicGeometry.GeometricallyIrreducible: We say that morphism f : X ⟶ Y is geometrically irreducible if for all Spec K ⟶ Y with K a field, X ×[Y] Spec K is irrreducible. We also provide the fact that this is stable under base change (by infer_instance)
• GeometricallyIrreducible.iff_geometricallyIrreducible_fiber: A scheme is geometrically irreducible over S iff the fibers of all s : S are geometrically irreducible.
• AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace: If X is geometrically irreducible and universally open (e.g. when flat + finite presentation), over an irreducible scheme, then X is also irreducible. In particular, the base change of a geometrically irreducible and universally open scheme to an irreducible scheme is irreducible (by infer_instance).

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

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

• geometrically_irreducibleSpace : geometrically (fun (x : Scheme) => IrreducibleSpace ↥x) f

theorem AlgebraicGeometry.geometricallyIrreducible_iff {X Y : Scheme} (f : X ⟶ Y) : GeometricallyIrreducible f ↔ geometrically (fun (x : Scheme) => IrreducibleSpace ↥x) f

theorem AlgebraicGeometry.GeometricallyIrreducible.eq_geometrically : @GeometricallyIrreducible = geometrically fun (x : Scheme) => IrreducibleSpace ↥x

instance AlgebraicGeometry.instIsStableUnderBaseChangeSchemeGeometricallyIrreducible : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @GeometricallyIrreducible

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

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

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

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

instance AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatFiberOfGeometricallyIrreducible {X S : Scheme} (f : X ⟶ S) (s : ↥S) [GeometricallyIrreducible f] : IrreducibleSpace ↥(Scheme.Hom.fiber f s)

@[instance 100]

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

theorem AlgebraicGeometry.Scheme.Hom.isIrreducible_preimage {X S : Scheme} (f : X ⟶ S) [GeometricallyIrreducible f] (hf : IsOpenMap ⇑f) {s : Set ↥S} (hs : IsIrreducible s) : IsIrreducible (⇑f ⁻¹' s)

def AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv {X S : Scheme} (f : X ⟶ S) [GeometricallyIrreducible f] (hf : IsOpenMap ⇑f) : ↑(irreducibleComponents ↥X) ≃ ↑(irreducibleComponents ↥S)

If f : X ⟶ S is geometrically irreducible and open, then f induces an equivalence between the irreducible components of X and S.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_symm_apply_coe {X S : Scheme} (f : X ⟶ S) [GeometricallyIrreducible f] (hf : IsOpenMap ⇑f) (a✝ : ↑(irreducibleComponents ↥S)) : ↑((irreducibleComponentsEquiv f hf).symm a✝) = ⇑f ⁻¹' ↑a✝

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.irreducibleComponentsEquiv_apply_coe {X S : Scheme} (f : X ⟶ S) [GeometricallyIrreducible f] (hf : IsOpenMap ⇑f) (a✝ : ↑(irreducibleComponents ↥X)) : ↑((irreducibleComponentsEquiv f hf) a✝) = ⇑f '' ↑a✝

theorem AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace {X S : Scheme} (f : X ⟶ S) [GeometricallyIrreducible f] [IrreducibleSpace ↥S] (hf : IsOpenMap ⇑f) : IrreducibleSpace ↥X

theorem AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_subsingleton {X S : Scheme} (f : X ⟶ S) [GeometricallyIrreducible f] [Subsingleton ↥S] [Nonempty ↥S] : IrreducibleSpace ↥X

If X is geometrically irreducible over a point, then it is irreducible.

instance AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyIrreducible f] [UniversallyOpen f] [IrreducibleSpace ↥Y] : IrreducibleSpace ↥(CategoryTheory.Limits.pullback f g)

If X is geometrically irreducible and universally open over S and Y is irreducible, then X ×ₛ Y is irreducible.

The universally open assumption in particular holds when it is flat and locally of finite presentation, or when S is a field.

instance AlgebraicGeometry.instIrreducibleSpaceCarrierCarrierCommRingCatPullbackSchemeOfGeometricallyIrreducibleOfUniversallyOpen_1 {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [GeometricallyIrreducible g] [UniversallyOpen g] [IrreducibleSpace ↥X] : IrreducibleSpace ↥(CategoryTheory.Limits.pullback f g)

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

theorem AlgebraicGeometry.GeometricallyIrreducible.comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [GeometricallyIrreducible f] [GeometricallyIrreducible g] [UniversallyOpen f] [UniversallyOpen g] : GeometricallyIrreducible (CategoryTheory.CategoryStruct.comp f g)