NYLL
Module

SmoothStalkNormality.lean

Nyll.SchemeTheory.LocalGeometry.SmoothStalkNormality
1 declaration indexed from sourceView source ↗

Module documentation

Integral closure of source stalks under smooth morphisms

For a smooth morphism to an affine scheme whose global section ring is a domain and integrally closed, every source stalk has these properties. The proof uses the smooth algebra on an affine source chart and its prime localization.

Imports3
Imported by26

Declarations

theorem

isDomain_and_isIntegrallyClosed_stalk

L35 ↗
AlgebraicGeometry.Smooth.isDomain_and_isIntegrallyClosed_stalk
Source context 4 commands

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

section ProofImplementation
namespace AlgebraicCurves.Geometry.Schemes.Proofs.Smooth_isDomain_and_isIntegrallyClosed_stalk
universe u
open CategoryTheory CategoryTheory.Limits AlgebraicGeometry TopologicalSpace
Lean source · statement
theorem _root_.AlgebraicGeometry.Smooth.isDomain_and_isIntegrallyClosed_stalk
    {U S : Scheme.{u}} (f : U ⟶ S) [Smooth f]
    [IsAffine S] [IsDomain Γ(S, ⊤)] [IsIntegrallyClosed Γ(S, ⊤)] (y : U) :
    IsDomain (U.presheaf.stalk y) ∧ IsIntegrallyClosed (U.presheaf.stalk y)

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