NYLL
Module

GeometricallyConnectedOfGlobalSections.lean

Nyll.SchemeTheory.Affine.GeometricallyConnectedOfGlobalSections
1 declaration indexed from sourceView source ↗

Module documentation

Geometric connectedness from scalar global sections

If a qcqs scheme over a field has exactly the base field as its global sections through the actual structure map, it is geometrically connected. Every extension of the base field is flat, so flat base change preserves the sections isomorphism and the idempotent argument applies after each field extension. This supplies the geometric step for normalization fibres once their actual section maps have been computed.

Imports3
Imported by2

Declarations

lemma

geometricallyConnected_of_isIso_appTop_to_field

L32 ↗
AlgebraicGeometry.geometricallyConnected_of_isIso_appTop_to_field
Documentation

A qcqs scheme over a field is geometrically connected if its structure morphism induces an isomorphism on global sections.

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
lemma geometricallyConnected_of_isIso_appTop_to_field
    {K : Type u} [Field K] {X : Scheme.{u}}
    (f : X ⟶ Spec (CommRingCat.of K))
    [QuasiCompact f] [QuasiSeparated f] [IsIso f.appTop] :
    GeometricallyConnected f

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