Module

ConnectedComplement.lean

Nyll.SchemeTheory.Divisors.ConnectedComplement

6 declarations indexed from sourceView source ↗

Module documentation

Density and connectedness of divisor complements

The complement of an effective Cartier divisor is dense, without a reducedness hypothesis. A dense open subset of a connected space is connected if every point of its complement admits an irreducible open neighborhood.

For a locally Noetherian scheme, an irreducible neighborhood is constructed from a domain stalk: the image of its local spectrum is irreducible and contains all generizations, so only one irreducible component passes through the point on an affine chart. Removing the other finitely many components produces the required neighborhood.

The algebraic implication from IsRegularLocalRing to IsDomain is not assumed or axiomatized here. These lemmas do not by themselves complete the regular-boundary case until that implication is available.

Imports9

Nyll.SchemeTheory.Divisors.LocalComplement
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.AlgebraicGeometry.Stalk
Mathlib.AlgebraicGeometry.Properties
Mathlib.RingTheory.Localization.Away.Basic
Mathlib.RingTheory.Spectrum.Prime.Topology
Mathlib.Topology.Connected.Basic
Mathlib.Topology.NoetherianSpace
Mathlib.Topology.Sober

Imported by3

theorem

dense_basicOpen_of_isRegular

L44 ↗

PrimeSpectrum.dense_basicOpen_of_isRegular

Documentation

A principal open defined by a non-zero-divisor is dense.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace Set
namespace PrimeSpectrum
universe u

Lean source · statement

theorem dense_basicOpen_of_isRegular
    {R : Type u} [CommRing R] {f : R} (hf : IsRegular f) :
    Dense (basicOpen f : Set (PrimeSpectrum R))

theorem

connectedSpace_open_of_dense_of_irreducible_boundary_neighborhoods

L69 ↗

SchemeTheory.connectedSpace_open_of_dense_of_irreducible_boundary_neighborhoods

Documentation

Irreducible neighborhoods at the missing points prevent a dense open subset of a connected space from disconnecting.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace Set
namespace SchemeTheory
universe u

Lean source · statement

theorem connectedSpace_open_of_dense_of_irreducible_boundary_neighborhoods
    {X : Type u} [TopologicalSpace X] [ConnectedSpace X]
    (U : Set X) (hU : IsOpen U) (hdense : Dense U)
    (hlocal : ∀ x ∉ U, ∃ V : Set X, IsOpen V ∧ x ∈ V ∧ IsIrreducible V) :
    ConnectedSpace U

theorem

exists_irreducible_open_of_generizations_subset

L116 ↗

SchemeTheory.exists_irreducible_open_of_generizations_subset

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace Set
namespace SchemeTheory
universe u

Lean source · statement

theorem exists_irreducible_open_of_generizations_subset
    {X : Type u} [TopologicalSpace X] [NoetherianSpace X] [QuasiSober X]
    (x : X) (S : Set X) (hS : IsIrreducible S)
    (hgen : ∀ y, y ⤳ x → y ∈ S) :
    ∃ V : Set X, IsOpen V ∧ x ∈ V ∧ IsIrreducible V

theorem

dense_supportComplement

L156 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.dense_supportComplement

Documentation

An effective Cartier divisor misses a dense open subset of its ambient scheme.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace Set
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem EffectiveCartierDivisor.dense_supportComplement
    {X : Scheme.{u}} (D : X.EffectiveCartierDivisor) :
    Dense (D.1.supportComplement : Set X)

theorem

exists_isIrreducible_open_of_isDomain_stalk

L189 ↗

AlgebraicGeometry.Scheme.exists_isIrreducible_open_of_isDomain_stalk

Documentation

A domain stalk on a locally Noetherian scheme has an irreducible open neighborhood.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace Set
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem exists_isIrreducible_open_of_isDomain_stalk
    {X : Scheme.{u}} [IsLocallyNoetherian X] (x : X)
    [IsDomain (X.presheaf.stalk x)] :
    ∃ V : Set X, IsOpen V ∧ x ∈ V ∧ IsIrreducible V

theorem

connectedSpace_supportComplement_of_domain_stalks

L221 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.connectedSpace_supportComplement_of_domain_stalks

Documentation

For a divisor whose boundary stalks are domains, the dense open complement is connected. This does not assume integrality or normality away from the boundary.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace Set
namespace AlgebraicGeometry.Scheme
universe u

Lean source · statement

theorem EffectiveCartierDivisor.connectedSpace_supportComplement_of_domain_stalks
    {X : Scheme.{u}} [ConnectedSpace X] [IsLocallyNoetherian X]
    (D : X.EffectiveCartierDivisor)
    (hD : ∀ x ∈ D.1.support, IsDomain (X.presheaf.stalk x)) :
    ConnectedSpace D.1.supportComplement

Module documentation

Density and connectedness of divisor complements

Declarations

dense_basicOpen_of_isRegular

connectedSpace_open_of_dense_of_irreducible_boundary_neighborhoods

exists_irreducible_open_of_generizations_subset

dense_supportComplement

exists_isIrreducible_open_of_isDomain_stalk

connectedSpace_supportComplement_of_domain_stalks