Module

ReducedIrreducibleComponentGeometry.lean

Nyll.SchemeTheory.Divisors.ReducedIrreducibleComponentGeometry

10 declarations indexed from sourceView source ↗

Module documentation

Geometry of reduced irreducible components

The reduced closed subscheme carried by an irreducible component is integral. Its generic point maps to the canonical generic point of the chosen component. These facts let later local-chart constructions select the correct prime of an ambient affine neighbourhood without introducing an extra component point.

Imports5

Nyll.SchemeTheory.Divisors.IrreducibleComponentMap
Nyll.SchemeTheory.FunctionFields.Functoriality
Mathlib.AlgebraicGeometry.Cover.Open
Mathlib.AlgebraicGeometry.Noetherian
Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Imported by7

instance

reducedIrreducibleComponent_isIntegral

L38 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponent_isIntegral

Documentation

The reduced closed subscheme supported on an irreducible component is integral.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) (Z : Set X)
  (hZ : Z ∈ irreducibleComponents X)

Lean source · statement

instance reducedIrreducibleComponent_isIntegral :
    IsIntegral (X.reducedIrreducibleComponent Z hZ)

theorem

range_reducedIrreducibleComponentι

L54 ↗

AlgebraicGeometry.Scheme.range_reducedIrreducibleComponentι

Documentation

The reduced component immersion has exactly the chosen component as its set-theoretic range.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) (Z : Set X)
  (hZ : Z ∈ irreducibleComponents X)

Lean source · statement

theorem range_reducedIrreducibleComponentι :
    Set.range (X.reducedIrreducibleComponentι Z hZ) = Z

theorem

reducedIrreducibleComponentι_genericPoint

L68 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponentι_genericPoint

Documentation

The generic point of the reduced component maps to the canonical generic point of its chosen topological irreducible component.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme
variable (X : Scheme.{u}) (Z : Set X)
  (hZ : Z ∈ irreducibleComponents X)

Lean source · statement

theorem reducedIrreducibleComponentι_genericPoint :
    X.reducedIrreducibleComponentι Z hZ
        (genericPoint (X.reducedIrreducibleComponent Z hZ)) =
      (genericPoints.ofComponent ⟨Z, hZ⟩).1

def

componentGenericPoint

L91 ↗

AlgebraicGeometry.Scheme.IdealSheafData.componentGenericPoint

Documentation

The point of the ambient scheme underlying the generic point of a chosen irreducible component of an ideal-sheaf subscheme.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X S : Scheme.{u}}

Lean source · statement

def componentGenericPoint (I : X.IdealSheafData)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme) : X

theorem

componentGenericPoint_eq

L99 ↗

AlgebraicGeometry.Scheme.IdealSheafData.componentGenericPoint_eq

Documentation

The component generic point is the image of the canonical topological generic point of that component.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X S : Scheme.{u}}

Lean source · statement

theorem componentGenericPoint_eq (I : X.IdealSheafData)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme) :
    I.componentGenericPoint Z hZ =
      I.subschemeι (genericPoints.ofComponent ⟨Z, hZ⟩).1

theorem

componentGenericPoint_mem_support

L108 ↗

AlgebraicGeometry.Scheme.IdealSheafData.componentGenericPoint_mem_support

Documentation

The generic point of every irreducible component of an ideal-sheaf subscheme lies in the support of the ideal sheaf.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X S : Scheme.{u}}

Lean source · statement

theorem componentGenericPoint_mem_support (I : X.IdealSheafData)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme) :
    I.componentGenericPoint Z hZ ∈ I.support

theorem

isRegularAt_componentGenericPoint

L117 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsAmbientRegularAlongSupport.isRegularAt_componentGenericPoint

Documentation

Ambient regularity along the support applies, without a separately chosen point hypothesis, at the generic point of every component.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X S : Scheme.{u}}

Lean source · statement

theorem IsAmbientRegularAlongSupport.isRegularAt_componentGenericPoint
    {I : X.IdealSheafData} (hI : I.IsAmbientRegularAlongSupport)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme) :
    X.IsRegularAt (I.componentGenericPoint Z hZ)

theorem

exists_affineChart_at_componentGenericPoint

L126 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.exists_affineChart_at_componentGenericPoint

Documentation

The effective-Cartier structure supplies an affine principal chart at the generic point of a chosen component. In particular, no chart or local equation has to be added as an independent hypothesis downstream.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X S : Scheme.{u}}

Lean source · statement

theorem IsEffectiveCartier.exists_affineChart_at_componentGenericPoint
    {I : X.IdealSheafData} (hI : I.IsEffectiveCartier)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme) :
    ∃ (U : X.affineOpens)
      (_hx : I.componentGenericPoint Z hZ ∈ U.1) (f : Γ(X, U.1)),
      IsRegular f ∧ I.ideal U = Ideal.span {f}

theorem

coheight_componentGenericPoint_eq_one

L138 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.coheight_componentGenericPoint_eq_one

Documentation

The generic point of a component of an effective Cartier divisor on a locally Noetherian scheme has codimension one. A Cartier equation is a non-zero-divisor, so no minimal prime can contain it; global integrality of the ambient scheme is unnecessary.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X S : Scheme.{u}}

Lean source · statement

theorem IsEffectiveCartier.coheight_componentGenericPoint_eq_one
    [IsLocallyNoetherian X]
    {I : X.IdealSheafData} (hI : I.IsEffectiveCartier)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme) :
    Order.coheight (I.componentGenericPoint Z hZ) = 1

theorem

componentToBase_genericPoint

L252 ↗

AlgebraicGeometry.Scheme.IdealSheafData.componentToBase_genericPoint

Documentation

A dominant structural morphism from a reduced component sends its generic point to the generic point of the integral base.

Source context 6 commands

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

noncomputable section
open CategoryTheory TopologicalSpace
namespace AlgebraicGeometry
universe u
namespace Scheme.IdealSheafData
variable {X S : Scheme.{u}}

Lean source · statement

theorem componentToBase_genericPoint (I : X.IdealSheafData) (p : X ⟶ S)
    [IsIntegral S]
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme)
    (hDense : DenseRange (I.componentToBase p Z hZ)) :
    I.componentToBase p Z hZ
        (genericPoint (I.subscheme.reducedIrreducibleComponent Z hZ)) =
      genericPoint S

Module documentation

Geometry of reduced irreducible components

Declarations