NYLL
Module

SmoothIrreducibleComponents.lean

Nyll.SchemeTheory.Divisors.SmoothIrreducibleComponents
2 declarations indexed from sourceView source ↗

Module documentation

Components smooth over a normal affine base

The local normality theorem for smooth morphisms supplies the domain stalks needed to identify reduced irreducible components as finite étale covers.

Imports3
Imported by2

Declarations

theorem

reducedIrreducibleComponentι_isFiniteEtale_of_smooth

L28 ↗
AlgebraicGeometry.Scheme.reducedIrreducibleComponentι_isFiniteEtale_of_smooth
Documentation

A reduced irreducible component of a scheme smooth over a normal affine Noetherian integral base is open and closed.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
Lean source · statement
theorem reducedIrreducibleComponentι_isFiniteEtale_of_smooth
    {X S : Scheme.{u}} [IsAffine S] [IsLocallyNoetherian S]
    [IsDomain Γ(S, ⊤)] [IsIntegrallyClosed Γ(S, ⊤)]
    (p : X ⟶ S) [Smooth p]
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X) :
    IsFiniteEtale (X.reducedIrreducibleComponentι Z hZ)
theorem

reducedIrreducibleComponentMap_isFiniteEtale_of_smooth

L40 ↗
AlgebraicGeometry.Scheme.reducedIrreducibleComponentMap_isFiniteEtale_of_smooth
Documentation

A finite étale morphism remains finite étale on reduced components above a component that is smooth over a normal affine Noetherian integral base.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
Lean source · statement
theorem reducedIrreducibleComponentMap_isFiniteEtale_of_smooth
    {X Y S : Scheme.{u}} [IsAffine S] [IsLocallyNoetherian S]
    [IsDomain Γ(S, ⊤)] [IsIntegrallyClosed Γ(S, ⊤)]
    (f : X ⟶ Y) [IsFiniteEtale f] (p : Y ⟶ S)
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y)
    (himage : f '' Z = W)
    [Smooth (Y.reducedIrreducibleComponentι W hW ≫ p)] :
    IsFiniteEtale (X.reducedIrreducibleComponentMap f Z hZ W hW himage)

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