NYLL
Module

EtaleIrreducibleComponentMap.lean

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

Module documentation

Étale morphisms on reduced components

Pulling back a reduced component of the base produces an actual finite étale cover. A component of the original source lifts to a closed component in that pullback. Domain stalks make this lifted component open, which proves that the induced map of reduced components is finite étale.

Imports1
Imported by2

Declarations

theorem

reducedIrreducibleComponentMap_isFiniteEtale

L28 ↗
AlgebraicGeometry.Scheme.reducedIrreducibleComponentMap_isFiniteEtale
Documentation

A finite étale map restricts to a finite étale map on chosen reduced components if the base change to the target component has domain stalks.

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
    {X Y : Scheme.{u}} (f : X ⟶ Y) [IsFiniteEtale f]
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (W : Set Y) (hW : W ∈ irreducibleComponents Y)
    (himage : f '' Z = W)
    [IsLocallyNoetherian (pullback f (Y.reducedIrreducibleComponentι W hW))]
    (hdom : ∀ x : (pullback f (Y.reducedIrreducibleComponentι W hW) : Scheme.{u}),
      IsDomain ((pullback f (Y.reducedIrreducibleComponentι W hW)).presheaf.stalk x)) :
    IsFiniteEtale (X.reducedIrreducibleComponentMap f Z hZ W hW himage)
theorem

componentToBase_comap_eq

L87 ↗
AlgebraicGeometry.Scheme.IdealSheafData.componentToBase_comap_eq
Documentation

The structural morphism of a pulled-back component is the composite of the actual map of reduced components with the downstairs structural map.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits TopologicalSpace
namespace AlgebraicGeometry.Scheme
universe u
namespace IdealSheafData
Lean source · statement
theorem componentToBase_comap_eq
    {X Y S : Scheme.{u}} (I : X.IdealSheafData) (f : Y ⟶ X) (p : X ⟶ S)
    (Z : Set (I.comap f).subscheme)
    (hZ : Z ∈ irreducibleComponents (I.comap f).subscheme)
    (W : Set I.subscheme) (hW : W ∈ irreducibleComponents I.subscheme)
    (himage : I.comapSubschemeTo f '' Z = W) :
    (I.comap f).componentToBase (f ≫ p) Z hZ =
      (I.comap f).subscheme.reducedIrreducibleComponentMap
        (I.comapSubschemeTo f) Z hZ W hW himage ≫ I.componentToBase p W hW

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