Module

ArithmeticBoundary.lean

Nyll.SchemeTheory.Divisors.ArithmeticBoundary

8 declarations indexed from sourceView source ↗

Module documentation

Arithmetic boundary conditions

This file records the scheme-theoretic data used to state boundary conditions over an integral base, directly on the closed subschemes defined by irreducible components.

The condition uses local Noetherianity rather than a finite-type or Nagata hypothesis. The base is an arbitrary integral scheme; its generic point specifies the generic fibres occurring below.

Imports6

Mathlib.AlgebraicGeometry.Geometrically.Integral
Mathlib.AlgebraicGeometry.Limits
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Nyll.SchemeTheory.Divisors.Basic
Nyll.SchemeTheory.Pi1.FiniteEtale.Basic
Nyll.SchemeTheory.Normalization.Normal

Imported by5

def

reducedIrreducibleComponent

L41 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponent

Documentation

The reduced closed subscheme carried by an irreducible component.

Unlike Scheme.irreducibleComponent, this construction uses the reduced induced structure and therefore does not require the ambient scheme to be globally Noetherian.

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

def reducedIrreducibleComponent (X : Scheme.{u})
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X) : Scheme.{u}

def

reducedIrreducibleComponentι

L48 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponentι

Documentation

The closed immersion of a reduced irreducible component into its ambient scheme.

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

def reducedIrreducibleComponentι (X : Scheme.{u})
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X) :
    X.reducedIrreducibleComponent Z hZ ⟶ X

instance

(anonymous instance)

L54 ↗

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

instance (X : Scheme.{u}) (Z : Set X) (hZ : Z ∈ irreducibleComponents X) :
    IsClosedImmersion (X.reducedIrreducibleComponentι Z hZ)

lemma

reducedIrreducibleComponentι_apply

L62 ↗

AlgebraicGeometry.Scheme.reducedIrreducibleComponentι_apply

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

lemma reducedIrreducibleComponentι_apply (X : Scheme.{u})
    (Z : Set X) (hZ : Z ∈ irreducibleComponents X)
    (z : X.reducedIrreducibleComponent Z hZ) :
    X.reducedIrreducibleComponentι Z hZ z = z.1

def

componentToBase

L74 ↗

AlgebraicGeometry.Scheme.IdealSheafData.componentToBase

Documentation

The structural morphism from the reduced subscheme carried by an irreducible component of an ideal-sheaf subscheme.

Source context 7 commands

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

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

Lean source · statement

def componentToBase (I : X.IdealSheafData) (p : X ⟶ S)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme) :
    I.subscheme.reducedIrreducibleComponent Z hZ ⟶ S

def

IsHorizontalOver

L86 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.IsHorizontalOver

Documentation

Every irreducible component of the divisor dominates the base.

Source context 7 commands

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

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

Lean source · statement

def IsHorizontalOver (D : EffectiveCartierDivisor X) (p : X ⟶ S) : Prop

def

HasNormalCrossingPointOfResidueCharacteristicOnEachComponent

L92 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent

Documentation

Every irreducible component contains a point of the prescribed residue characteristic where the whole divisor has normal crossings.

Source context 7 commands

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

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

Lean source · statement

def HasNormalCrossingPointOfResidueCharacteristicOnEachComponent
    (D : EffectiveCartierDivisor X) (q : ℕ) : Prop

def

pulledBackComponentToBase

L102 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.pulledBackComponentToBase

Documentation

The morphism to the arithmetic base from a reduced component of the pullback of a divisor along a finite etale cover.

Source context 7 commands

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

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

Lean source · statement

def pulledBackComponentToBase
    (D : EffectiveCartierDivisor X) (p : X ⟶ S) (Y : FiniteEtale X)
    (Z : Set (D.1.comap Y.hom).subscheme)
    (hZ : Z ∈ irreducibleComponents (D.1.comap Y.hom).subscheme) :
    (D.1.comap Y.hom).subscheme.reducedIrreducibleComponent Z hZ ⟶ S

Module documentation

Arithmetic boundary conditions

Declarations