Geometrically irreducible schemes over a field

A scheme X over a field k is geometrically irreducible if any base change X_K for a field extension K of k is irreducible.

@[reducible, inline]

abbrev AlgebraicGeometry.GeometricallyIrreducible {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) : Prop

A scheme X over a field k is geometrically irreducible if any base change X_K is irreducible for a field extension K of k.

Equations

• AlgebraicGeometry.GeometricallyIrreducible s = AlgebraicGeometry.Geometrically (fun (X : AlgebraicGeometry.Scheme) => IrreducibleSpace ↥X) s

instance AlgebraicGeometry.instInheritedFromSourceSchemeIrreducibleSpaceCarrierCarrierCommRingCatSurjective : CategoryTheory.ObjectProperty.InheritedFromSource (fun (X : Scheme) => IrreducibleSpace ↥X) @Surjective

instance AlgebraicGeometry.instIsClosedUnderIsomorphismsSchemeIrreducibleSpaceCarrierCarrierCommRingCat_geometricallyP : CategoryTheory.ObjectProperty.IsClosedUnderIsomorphisms fun (X : Scheme) => IrreducibleSpace ↥X

theorem AlgebraicGeometry.nonempty_pullback_of_subsingleton_of_nonempty {X Y S : Scheme} [Nonempty ↥X] [Nonempty ↥Y] [Nonempty ↥S] [Subsingleton ↥S] (f : X ⟶ S) (g : Y ⟶ S) : Nonempty ↥(CategoryTheory.Limits.pullback f g)

theorem AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_self {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [GeometricallyIrreducible s] : IrreducibleSpace ↥X

theorem AlgebraicGeometry.GeometricallyIrreducible.iff_irreducibleSpace_pullback {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) : GeometricallyIrreducible s ↔ ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K], IrreducibleSpace ↥(CategoryTheory.Limits.pullback s (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k)))

theorem AlgebraicGeometry.GeometricallyIrreducible.irreducibleSpace_of_isPullback {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [GeometricallyIrreducible s] {Y : Scheme} {K : Type u} [Field K] [Algebra k K] {t : Y ⟶ Spec (CommRingCat.of K)} {f : Y ⟶ X} (h : CategoryTheory.IsPullback f t s (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k))) : IrreducibleSpace ↥Y

theorem AlgebraicGeometry.GeometricallyIrreducible.iff_spec {k : Type u} [Field k] (R : Type u) [CommRing R] [Algebra k R] : GeometricallyIrreducible (Spec (CommRingCat.of R) ↘ Spec (CommRingCat.of k)) ↔ Algebra.GeometricallyIrreducible k R

The affine scheme Spec R is geometrically irreducible over k if and only if the k-algebra R is geometrically irreducible.

theorem AlgebraicGeometry.GeometricallyIrreducible.of_isOpenImmersion {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) (U : Scheme) (i : U ⟶ X) [IsOpenImmersion i] [Nonempty ↥U] [GeometricallyIrreducible s] : GeometricallyIrreducible (CategoryTheory.CategoryStruct.comp i s)

Every nonempty open subscheme of a geometrically irreducible scheme is geometrically irreducible.

theorem AlgebraicGeometry.GeometricallyIrreducible.geometricallyIrreducible_of_isAffineOpen {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [GeometricallyIrreducible s] (U : X.Opens) (hU : IsAffineOpen U) (hU' : U.carrier.Nonempty) : Algebra.GeometricallyIrreducible k ↑(X.presheaf.obj (Opposite.op U))

If X is geometrically irreducible over k and U is an affine open, Γ(X, U) is geometrically irreducible over k.

theorem AlgebraicGeometry.GeometricallyIrreducible.irreducible_of_openCover {X : Scheme} (𝒰 : X.OpenCover) [Nonempty 𝒰.I₀] (hn : ∀ (i j : 𝒰.I₀), Nonempty ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))) (h : ∀ (i : 𝒰.I₀), IrreducibleSpace ↥(𝒰.X i)) : IrreducibleSpace ↥X

Irreducibility of a scheme can be checked on an open cover with pairwise non-empty intersections.

theorem nonempty_pullback_baseChange_of_surjective {X U₁ U₂ S S' : AlgebraicGeometry.Scheme} (s : X ⟶ S) (f₁ : U₁ ⟶ X) (f₂ : U₂ ⟶ X) (hn : Nonempty ↥(CategoryTheory.Limits.pullback f₁ f₂)) (g : S' ⟶ S) [hg : AlgebraicGeometry.Surjective g] : Nonempty ↥(CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f₁ s) g s g f₁ (CategoryTheory.CategoryStruct.id S') (CategoryTheory.CategoryStruct.id S) ⋯ ⋯) (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f₂ s) g s g f₂ (CategoryTheory.CategoryStruct.id S') (CategoryTheory.CategoryStruct.id S) ⋯ ⋯))

theorem AlgebraicGeometry.GeometricallyIrreducible.of_openCover {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) (𝒰 : X.OpenCover) [Nonempty 𝒰.I₀] (hn : ∀ (i j : 𝒰.I₀), Nonempty ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))) (h : ∀ (i : 𝒰.I₀), GeometricallyIrreducible (CategoryTheory.CategoryStruct.comp (𝒰.f i) s)) : GeometricallyIrreducible s

If X is covered by geometrically irreducible open subschemes with pairwise non-empty intersections, X is geometrically irreducible.

theorem AlgebraicGeometry.GeometricallyIrreducible.of_finite {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) (H : ∀ (K : Type u) [inst : Field K] [inst_1 : Algebra k K] [Module.Finite k K] [Algebra.IsSeparable k K], IrreducibleSpace ↥(CategoryTheory.Limits.pullback s (Spec (CommRingCat.of K) ↘ Spec (CommRingCat.of k)))) : GeometricallyIrreducible s

Being geometrically irreducible can be checked on finite extensions.

theorem AlgebraicGeometry.GeometricallyIrreducible.of_isSepClosed {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) (Ω : Type u) [Field Ω] [Algebra k Ω] [IsSepClosed Ω] [IrreducibleSpace ↥(CategoryTheory.Limits.pullback s (Spec (CommRingCat.of Ω) ↘ Spec (CommRingCat.of k)))] : GeometricallyIrreducible s

Being geometrically irreducible can be checked on a separably closed field.

theorem AlgebraicGeometry.GeometricallyIrreducible.iff_irreducibleSpace_separableClosure {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) : GeometricallyIrreducible s ↔ IrreducibleSpace ↥(CategoryTheory.Limits.pullback s (Spec (CommRingCat.of (SeparableClosure k)) ↘ Spec (CommRingCat.of k)))

X is geometrically irreducible over s if and only if X_K is irreducible for K a separable closure of k.

def AlgebraicGeometry.GeometricallyIrreducible.irreducibleComponentsOrderIsoPullback {k : Type u} [Field k] {X : Scheme} (s : X ⟶ Spec (CommRingCat.of k)) [GeometricallyIrreducible s] {Y : Scheme} (t : Y ⟶ Spec (CommRingCat.of k)) : ↑(irreducibleComponents ↥Y) ≃o ↑(irreducibleComponents ↥(CategoryTheory.Limits.pullback s t))

If X is geometrically irreducible over k and Y is any k-scheme, then X ×[k] Y ⟶ Y induces an order preserving bijection between irreducible components.

Equations

• One or more equations did not get rendered due to their size.