Geometric properties of schemes over a field

TheoremGeometrically irreducible morphisms are geometrically connected#✓fully proved

A geometrically irreducible morphism is geometrically connected.

theorem AlgebraicGeometry.GeometricallyIrreducible.geometricallyConnected
    {X Y : Scheme.{u}} (f : X ⟶ Y) [GeometricallyIrreducible f] :
    GeometricallyConnected f

TheoremGeometric irreducibility over an algebraically closed field#✓fully proved

An irreducible scheme over an algebraically closed field is geometrically irreducible.

theorem GeometricallyIrreducible.of_irreducibleSpace_of_isAlgClosed {k : Type u} [Field k]
    [IsAlgClosed k] {X : Scheme.{u}} (f : X ⟶ Spec (CommRingCat.of k))
    [IrreducibleSpace X] :
    GeometricallyIrreducible f

Uses 1 · Used by 1

Proof usesField-with-domain tensor products over an algebraically closed field

Used byIntegral schemes over algebraically closed fields: geometric integrality

TheoremReduced schemes over a perfect field are geometrically reduced#✓fully proved

A reduced scheme over a perfect field is geometrically reduced.

theorem AlgebraicGeometry.GeometricallyReduced.of_isReduced_of_perfectField
    {k : Type u} [Field k] [PerfectField k] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of k)) [IsReduced X] :
    AlgebraicGeometry.GeometricallyReduced f

Uses 1 · Used by 1

Proof usesReduced algebras stay reduced under base change over a perfect field

Used byIntegral schemes over algebraically closed fields: geometric integrality

TheoremIntegral schemes over algebraically closed fields: geometric integrality#✓fully proved

An integral scheme over an algebraically closed field is geometrically integral.

theorem GeometricallyIntegral.of_isIntegral_of_isAlgClosed
    {K : Type u} [Field K] [IsAlgClosed K] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X] : GeometricallyIntegral f

Uses 2

Proof usesGeometric irreducibility over an algebraically closed field · Reduced schemes over a perfect field are geometrically reduced

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.