NYLL
Module

EtaleIrreducibleComponents.lean

Nyll.SchemeTheory.Divisors.EtaleIrreducibleComponents
3 declarations indexed from sourceView source ↗

Module documentation

Finite étale reduced components

Domain stalks make irreducible components open on a locally Noetherian scheme. For a reduced scheme, the reduced closed component then coincides with that open subscheme. In particular its inclusion is both finite and étale.

Imports3
Imported by3

Declarations

theorem

isOpen_irreducibleComponent_of_isDomain_stalk

L31 ↗
AlgebraicGeometry.Scheme.isOpen_irreducibleComponent_of_isDomain_stalk
Documentation

Every component is open when all stalks of a locally Noetherian scheme are domains.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
Lean source · statement
theorem isOpen_irreducibleComponent_of_isDomain_stalk
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (hdom : ∀ x : X, IsDomain (X.presheaf.stalk x))
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X) : IsOpen Z
theorem

isOpenImmersion_of_isClosedImmersion_of_isOpen_range

L46 ↗
AlgebraicGeometry.Scheme.isOpenImmersion_of_isClosedImmersion_of_isOpen_range
Documentation

A closed immersion into a reduced scheme is open if its range is open.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
Lean source · statement
theorem isOpenImmersion_of_isClosedImmersion_of_isOpen_range
    {X Y : Scheme.{u}} [IsReduced Y] (f : X ⟶ Y) [IsClosedImmersion f]
    (hopen : IsOpen (Set.range f)) : IsOpenImmersion f
theorem

reducedIrreducibleComponentι_isFiniteEtale

L68 ↗
AlgebraicGeometry.Scheme.reducedIrreducibleComponentι_isFiniteEtale
Documentation

On a reduced locally Noetherian scheme with domain stalks, the canonical reduced component inclusion is finite étale.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
Lean source · statement
theorem reducedIrreducibleComponentι_isFiniteEtale
    (X : Scheme.{u}) [IsLocallyNoetherian X]
    (hdom : ∀ x : X, IsDomain (X.presheaf.stalk x))
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X) :
    IsFiniteEtale (X.reducedIrreducibleComponentι Z hZ)

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