Module

SurjectiveArithmeticBoundary.lean

Nyll.SchemeTheory.Divisors.SurjectiveArithmeticBoundary

8 declarations indexed from sourceView source ↗

Module documentation

Boundary components surjective over an arithmetic base

This file distinguishes surjectivity of every boundary component from the weaker condition that every component merely dominates the base. Over the integer base, componentwise surjectivity supplies a point of every prime residue characteristic on every component. The structure morphism to Spec ℤ is the canonical map to the terminal scheme.

Imports2

Mathlib.RingTheory.Ideal.Int
Nyll.SchemeTheory.Divisors.ReducedIrreducibleComponentGeometry

Imported by3

def

HasSurjectiveComponentsOver

L35 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOver

Documentation

Every reduced irreducible component of the divisor maps surjectively to the base scheme. This is stronger than IsHorizontalOver, which only asks for dense image.

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.EffectiveCartierDivisor
variable {X S : Scheme.{u}}

Lean source · statement

def HasSurjectiveComponentsOver
    (D : EffectiveCartierDivisor X) (structural : X ⟶ S) : Prop

theorem

isHorizontalOver

L42 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOver.isHorizontalOver

Documentation

Componentwise surjectivity implies componentwise dominance.

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.EffectiveCartierDivisor
variable {X S : Scheme.{u}}

Lean source · statement

theorem HasSurjectiveComponentsOver.isHorizontalOver
    {D : EffectiveCartierDivisor X} {structural : X ⟶ S}
    (hD : D.HasSurjectiveComponentsOver structural) :
    D.IsHorizontalOver structural

theorem

exists_point_on_component_over

L53 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOver.exists_point_on_component_over

Documentation

Componentwise surjectivity lifts a prescribed base point to a point on the prescribed irreducible component of the divisor.

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.EffectiveCartierDivisor
variable {X S : Scheme.{u}}

Lean source · statement

theorem HasSurjectiveComponentsOver.exists_point_on_component_over
    {D : EffectiveCartierDivisor X} {structural : X ⟶ S}
    (hD : D.HasSurjectiveComponentsOver structural)
    (Z : Set D.1.subscheme)
    (hZ : Z ∈ irreducibleComponents D.1.subscheme) (s : S) :
    ∃ x : D.1.subscheme,
      x ∈ Z ∧ structural (D.1.subschemeι x) = s

def

HasSurjectiveComponentsOverIntegers

L72 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers

Documentation

The canonical integer-base version of componentwise surjectivity.

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.EffectiveCartierDivisor
variable {X S : Scheme.{u}}

Lean source · statement

def HasSurjectiveComponentsOverIntegers
    (D : EffectiveCartierDivisor X) : Prop

theorem

isHorizontalOverIntegers

L78 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers.isHorizontalOverIntegers

Documentation

Integer-base componentwise surjectivity implies horizontality for the canonical structure morphism.

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.EffectiveCartierDivisor
variable {X S : Scheme.{u}}

Lean source · statement

theorem HasSurjectiveComponentsOverIntegers.isHorizontalOverIntegers
    {D : EffectiveCartierDivisor X}
    (hD : D.HasSurjectiveComponentsOverIntegers) :
    D.IsHorizontalOver (specULiftZIsTerminal.from X)

def

integerPrimePoint

L90 ↗

AlgebraicGeometry.Scheme.integerPrimePoint

Documentation

The closed point (p) of Spec (ULift ℤ) attached to a rational prime.

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 integerPrimePoint (p : ℕ) (hp : p.Prime) :
    Spec (CommRingCat.of (ULift.{u} ℤ))

theorem

ringChar_residueField_integerPrimePoint

L99 ↗

AlgebraicGeometry.Scheme.ringChar_residueField_integerPrimePoint

Documentation

The residue field at the integer prime point (p) has characteristic p.

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 ringChar_residueField_integerPrimePoint
    (p : ℕ) (hp : p.Prime) :
    ringChar
        ((Spec (CommRingCat.of (ULift.{u} ℤ))).residueField
          (integerPrimePoint p hp)) = p

theorem

hasNormalCrossingPointOfResidueCharacteristicOnEachComponent

L128 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers.hasNormalCrossingPointOfResidueCharacteristicOnEachComponent

Documentation

If every component is surjective over the canonical integer base, then every component contains a normal-crossings point of each rational-prime residue characteristic.

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.EffectiveCartierDivisor
variable {X : Scheme.{u}}

Lean source · statement

theorem
  HasSurjectiveComponentsOverIntegers.hasNormalCrossingPointOfResidueCharacteristicOnEachComponent
    {D : EffectiveCartierDivisor X}
    (hD : D.HasSurjectiveComponentsOverIntegers)
    (hNC : D.IsNormalCrossings) (p : ℕ) (hp : p.Prime) :
    D.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent p

Module documentation

Boundary components surjective over an arithmetic base

Declarations