NYLL
Module

ProperNoetherianConnectedFibers.lean

Nyll.EtaleFundamentalGroups.FiniteEtale.ProperNoetherianConnectedFibers
2 declarations indexed from sourceView source ↗

Module documentation

Geometrically connected fibres of the actual proper normalization

The actual pushforward section isomorphism survives localization to each target stalk and then the nonflat change to its residue field. Scalar sections over that field imply geometric connectedness. For a proper flat geometrically reduced family, the previously computed finite étale second normalization map supplies flatness and geometric reducedness of the first.

Imports11
Imported by3

Declarations

theorem

geometricallyConnected_of_proper_flat_geometricallyReduced_of_isIso_c

L41 ↗
AlgebraicGeometry.geometricallyConnected_of_proper_flat_geometricallyReduced_of_isIso_c
Documentation

A proper flat finitely presented geometrically reduced family over an arbitrary base with scalar pushforward structure sheaf has geometrically connected fibres. The fibre section isomorphisms are constructed through stalk and residue-field base change.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem geometricallyConnected_of_proper_flat_geometricallyReduced_of_isIso_c
    {X S : Scheme.{u}} (f : X ⟶ S)
    [IsProper f] [Flat f] [LocallyOfFinitePresentation f]
    [GeometricallyReduced f] [IsIso f.c] :
    GeometricallyConnected f
theorem

geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced_noetherian

L82 ↗
AlgebraicGeometry.geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced_noetherian
Documentation

The actual first map of relative normalization has geometrically connected fibres for a proper flat geometrically reduced family over a locally Noetherian base. The second map's étaleness and all section comparisons are supplied by the proved constructions.

Source context 4 commands

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

noncomputable section
open CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry
universe u
Lean source · statement
theorem geometricallyConnected_toNormalization_of_proper_flat_geometricallyReduced_noetherian
    {X S : Scheme.{u}} [IsLocallyNoetherian S] (f : X ⟶ S)
    [IsProper f] [Flat f] [GeometricallyReduced f] :
    GeometricallyConnected f.toNormalization

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