Module

EtaleBranchCharacteristicZero.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.EtaleBranchCharacteristicZero

6 declarations indexed from sourceView source ↗

Module documentation

Characteristic-zero branches on etale normal-crossings charts

Height-one primes contract to height-one primes along an etale stalk map. Consequently, characteristic zero along every branch of a horizontal boundary passes to the strict chart witnessing normal crossings.

Imports5

Nyll.EtaleFundamentalGroups.FiniteEtale.Boundary.ArithmeticAllBranchCharacteristicZero
Nyll.SchemeTheory.Divisors.LocalComplement
Nyll.SchemeTheory.Divisors.SurjectiveArithmeticBoundary
Mathlib.AlgebraicGeometry.Morphisms.QuasiFinite
Mathlib.RingTheory.Ideal.KrullsHeightTheorem

Imported by3

theorem

height_comap_eq_one_of_flat_of_quasiFinite

L27 ↗

Ideal.height_comap_eq_one_of_flat_of_quasiFinite

Source context 3 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
universe u

Lean source · statement

theorem Ideal.height_comap_eq_one_of_flat_of_quasiFinite
    {R S : Type u} [CommRing R] [CommRing S]
    (f : R →+* S) (q : Ideal S) [q.IsPrime]
    (hflat : f.Flat) (hqf : f.QuasiFinite)
    [IsNoetherianRing R] [IsNoetherianRing S] (hq : q.height = 1) :
    (q.comap f).height = 1

theorem

comap_of_etale

L76 ↗

AlgebraicGeometry.Scheme.IdealSheafData.HasCharacteristicZeroBranchesAt.comap_of_etale

Documentation

Characteristic zero along every height-one boundary branch passes through an etale chart. The proof contracts a chart prime through the stalk map; support functoriality supplies containment of the original stalk ideal, so no affineness hypothesis or global stalk-ideal comparison is required.

Source context 5 commands

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

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

Lean source · statement

theorem HasCharacteristicZeroBranchesAt.comap_of_etale
    [IsLocallyNoetherian X]
    {I : X.IdealSheafData} (f : Y ⟶ X) [Etale f] (y : Y)
    (hI : I.HasCharacteristicZeroBranchesAt (f y)) :
    (I.comap f).HasCharacteristicZeroBranchesAt y

theorem

exists_etaleStrictChart_hasCharacteristicZeroBranchesAt

L135 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.IsHorizontalOver.exists_etaleStrictChart_hasCharacteristicZeroBranchesAt

Documentation

A horizontal normal-crossings boundary has an etale strict chart whose height-one boundary branches all have characteristic zero.

Source context 5 commands

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

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

Lean source · statement

theorem IsHorizontalOver.exists_etaleStrictChart_hasCharacteristicZeroBranchesAt
    [IsLocallyNoetherian X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) (structural : X ⟶ S)
    (hHorizontal : D.IsHorizontalOver structural)
    [CharZero (S.residueField (genericPoint S))]
    {x : X} (hNC : D.1.IsNormalCrossingsAt x) :
    ∃ (U : Scheme.{u}) (f : U ⟶ X) (u : U),
      Etale f ∧ f u = x ∧ (D.1.comap f).IsStrictNormalCrossings ∧
        (D.1.comap f).HasCharacteristicZeroBranchesAt u

instance

(anonymous instance)

L153 ↗

Source context 6 commands

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

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

Lean source · statement

instance : IsDomain (ULift.{u} ℤ)

theorem

exists_etaleStrictChart_hasCharacteristicZeroBranchesAt_overIntegers

L157 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.IsHorizontalOver.exists_etaleStrictChart_hasCharacteristicZeroBranchesAt_overIntegers

Documentation

Integer-base specialization of the horizontal etale-chart theorem.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
universe u
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
variable {X S : Scheme.{u}}
section IntegerBase
local instance : IsDomain (ULift.{u} ℤ) :=
  (ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ

Lean source · statement

theorem IsHorizontalOver.exists_etaleStrictChart_hasCharacteristicZeroBranchesAt_overIntegers
    [IsLocallyNoetherian X]
    (D : EffectiveCartierDivisor X)
    (hHorizontal : D.IsHorizontalOver (specULiftZIsTerminal.from X))
    {x : X} (hNC : D.1.IsNormalCrossingsAt x) :
    ∃ (U : Scheme.{u}) (f : U ⟶ X) (u : U),
      Etale f ∧ f u = x ∧ (D.1.comap f).IsStrictNormalCrossings ∧
        (D.1.comap f).HasCharacteristicZeroBranchesAt u

theorem

exists_etaleStrictChart_hasCharacteristicZeroBranchesAt

L175 ↗

AlgebraicGeometry.Scheme.EffectiveCartierDivisor.HasSurjectiveComponentsOverIntegers.exists_etaleStrictChart_hasCharacteristicZeroBranchesAt

Documentation

Componentwise surjectivity over the integer base supplies the same characteristic-zero etale strict chart.

Source context 7 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
universe u
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
variable {X S : Scheme.{u}}
section IntegerBase
local instance : IsDomain (ULift.{u} ℤ) :=
  (ULift.ringEquiv : ULift.{u} ℤ ≃+* ℤ).toMulEquiv.isDomain ℤ

Lean source · statement

theorem HasSurjectiveComponentsOverIntegers.exists_etaleStrictChart_hasCharacteristicZeroBranchesAt
    [IsLocallyNoetherian X]
    (D : EffectiveCartierDivisor X)
    (hD : D.HasSurjectiveComponentsOverIntegers)
    {x : X} (hNC : D.1.IsNormalCrossingsAt x) :
    ∃ (U : Scheme.{u}) (f : U ⟶ X) (u : U),
      Etale f ∧ f u = x ∧ (D.1.comap f).IsStrictNormalCrossings ∧
        (D.1.comap f).HasCharacteristicZeroBranchesAt u

Module documentation

Characteristic-zero branches on etale normal-crossings charts

Declarations

height_comap_eq_one_of_flat_of_quasiFinite

comap_of_etale

exists_etaleStrictChart_hasCharacteristicZeroBranchesAt

(anonymous instance)

exists_etaleStrictChart_hasCharacteristicZeroBranchesAt_overIntegers

exists_etaleStrictChart_hasCharacteristicZeroBranchesAt