NYLL
Module

SmoothGeometricallyIntegral.lean

Nyll.SchemeTheory.Morphisms.SmoothGeometricallyIntegral
1 declaration indexed from sourceView source ↗

Module documentation

Smooth geometrically connected morphisms are geometrically integral

After an arbitrary field-valued base change, smoothness supplies domain stalks and local Noetherianity. Geometric connectedness supplies connectedness, so the resulting scheme is integral.

Imports5
Imported by2

Declarations

theorem

geometricallyIntegral_of_geometricallyConnected

L30 ↗
AlgebraicGeometry.Smooth.geometricallyIntegral_of_geometricallyConnected
Documentation

Every smooth geometrically connected morphism is geometrically integral.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem Smooth.geometricallyIntegral_of_geometricallyConnected
    {X S : Scheme.{u}} (f : X ⟶ S) [Smooth f] [GeometricallyConnected f] :
    GeometricallyIntegral f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.