NYLL
Module

LocalHorizontalEtaleBranch.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.LocalHorizontalEtaleBranch
9 declarations indexed from sourceView source ↗

Module documentation

Locally horizontal component branches on etale charts

Only the boundary components through the chosen point need to dominate the base in order to obtain characteristic zero along all branches at that point. The canonical height-one prime of any specified incident component lifts to the strict etale chart, with its contraction recorded explicitly.

Imports2
Imported by2

Declarations

theorem

isPrime_transport_stalk

L25 ↗
Ideal.isPrime_transport_stalk
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.isPrime_transport_stalk
    {T : Scheme.{u}} {x x' : T} (h : x = x')
    (p : Ideal (T.presheaf.stalk x)) (hp : p.IsPrime) :
    (h ▸ p).IsPrime
theorem

height_transport_stalk

L32 ↗
Ideal.height_transport_stalk
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_transport_stalk
    {T : Scheme.{u}} {x x' : T} (h : x = x')
    (p : Ideal (T.presheaf.stalk x)) :
    (h ▸ p).height = p.height
theorem

stalkIdeal_le_transport

L39 ↗
AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_le_transport
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 AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_le_transport
    {T : Scheme.{u}} (I : T.IdealSheafData) {x x' : T} (h : x = x')
    {p : Ideal (T.presheaf.stalk x)} (hp : I.stalkIdeal x ≤ p) :
    I.stalkIdeal x' ≤ h ▸ p
theorem

height_eq_height_comap_of_flat_of_quasiFinite

L46 ↗
Ideal.height_eq_height_comap_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_eq_height_comap_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] :
    q.height = (q.comap f).height
def

ComponentsThroughPointAreHorizontal

L126 ↗
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.ComponentsThroughPointAreHorizontal
Documentation

Exactly the components through z dominate the base.

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
def ComponentsThroughPointAreHorizontal
    (D : EffectiveCartierDivisor X) (structural : X ⟶ S)
    (z : D.1.subscheme) : Prop
theorem

hasCharacteristicZeroBranchesAt

L135 ↗
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.ComponentsThroughPointAreHorizontal.hasCharacteristicZeroBranchesAt
Documentation

Local componentwise horizontality at a divisor point forces characteristic zero along every height-one branch through that point.

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 ComponentsThroughPointAreHorizontal.hasCharacteristicZeroBranchesAt
    [IsLocallyNoetherian X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) (structural : X ⟶ S)
    {z : D.1.subscheme}
    (hD : D.ComponentsThroughPointAreHorizontal structural z)
    [CharZero (S.residueField (genericPoint S))] :
    D.1.HasCharacteristicZeroBranchesAt (D.1.subschemeι z)
theorem

exists_etaleHeightOnePrime_liesOver

L193 ↗
AlgebraicGeometry.Scheme.IdealSheafData.exists_etaleHeightOnePrime_liesOver
Documentation

A height-one branch prime lifts through an etale stalk map. The lifted prime still contains the pulled-back boundary stalk ideal.

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 exists_etaleHeightOnePrime_liesOver
    [IsLocallyNoetherian X]
    (I : X.IdealSheafData) (f : Y ⟶ X) [Etale f] (y : Y)
    (p : Ideal (X.presheaf.stalk (f y))) [p.IsPrime]
    (hpheight : p.height = 1) (hIp : I.stalkIdeal (f y) ≤ p) :
    ∃ (q : Ideal (Y.presheaf.stalk y)) (_hqPrime : q.IsPrime),
      q.height = 1 ∧ (I.comap f).stalkIdeal y ≤ q ∧
        q.comap (f.stalkMap y).hom = p
theorem

exists_etaleHeightOnePrime_over_componentBranchPrimeAt

L269 ↗
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.exists_etaleHeightOnePrime_over_componentBranchPrimeAt
Documentation

The canonical branch prime of a specified divisor component has a height-one lift on every pointed etale neighbourhood. The final equality is literal lying-over after transporting the original branch ideal along the equality of centre points.

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 Y S : Scheme.{u}}
Lean source · full declaration
theorem exists_etaleHeightOnePrime_over_componentBranchPrimeAt
    [IsLocallyNoetherian X]
    (D : EffectiveCartierDivisor X)
    (Z : Set D.1.subscheme)
    (hZ : Z ∈ irreducibleComponents D.1.subscheme)
    (z : D.1.subscheme) (hz : z ∈ Z)
    (f : Y ⟶ X) [Etale f] (y : Y)
    (hfy : f y = D.1.subschemeι z) :
    let p : Ideal (X.presheaf.stalk (f y)) :=
      hfy.symm ▸ (D.1.componentBranchPrimeAt Z hZ z hz).asIdeal
    ∃ (q : Ideal (Y.presheaf.stalk y)) (_hqPrime : q.IsPrime),
      q.height = 1 ∧ (D.1.comap f).stalkIdeal y ≤ q ∧
        q.comap (f.stalkMap y).hom = p := by
  dsimp only
  let e : D.1.subschemeι z = f y := hfy.symm
  let p : Ideal (X.presheaf.stalk (f y)) :=
    e ▸ (D.1.componentBranchPrimeAt Z hZ z hz).asIdeal
  have hbranchPrime :
      (D.1.componentBranchPrimeAt Z hZ z hz).asIdeal.IsPrime :=
    (D.1.componentBranchPrimeAt Z hZ z hz).isPrime
  have hpPrime : p.IsPrime := Ideal.isPrime_transport_stalk e
    (D.1.componentBranchPrimeAt Z hZ z hz).asIdeal hbranchPrime
  let : p.IsPrime := hpPrime
  have hpheight : p.height = 1 := by
    rw [Ideal.height_transport_stalk e]
    exact D.2.componentBranchPrimeAt_height_eq_one Z hZ z hz
  have hIp : D.1.stalkIdeal (f y) ≤ p := by
    exact D.1.stalkIdeal_le_transport e
      (D.1.stalkIdeal_le_componentBranchPrimeAt Z hZ z hz)
  exact @Scheme.IdealSheafData.exists_etaleHeightOnePrime_liesOver
    X Y inferInstance D.1 f inferInstance y p hpPrime hpheight hIp
theorem

exists_etaleStrictChart_componentBranch

L305 ↗
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.ComponentsThroughPointAreHorizontal.exists_etaleStrictChart_componentBranch
Documentation

A normal-crossings point with only its incident components horizontal admits a strict etale chart carrying both characteristic-zero branches and a height-one prime lying over the canonical branch of a specified incident component.

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 Y S : Scheme.{u}}
Lean source · full declaration
theorem ComponentsThroughPointAreHorizontal.exists_etaleStrictChart_componentBranch
    [IsLocallyNoetherian X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) (structural : X ⟶ S)
    (Z : Set D.1.subscheme)
    (hZ : Z ∈ irreducibleComponents D.1.subscheme)
    (z : D.1.subscheme) (hz : z ∈ Z)
    (hD : D.ComponentsThroughPointAreHorizontal structural z)
    [CharZero (S.residueField (genericPoint S))]
    (hNC : D.1.IsNormalCrossingsAt (D.1.subschemeι z)) :
    ∃ (U : Scheme.{u}) (f : U ⟶ X) (u : U)
      (hfu : f u = D.1.subschemeι z),
      Etale f ∧ (D.1.comap f).IsStrictNormalCrossings ∧
        (D.1.comap f).HasCharacteristicZeroBranchesAt u ∧
          let p : Ideal (X.presheaf.stalk (f u)) :=
            hfu.symm ▸ (D.1.componentBranchPrimeAt Z hZ z hz).asIdeal
          ∃ (q : Ideal (U.presheaf.stalk u)) (_hqPrime : q.IsPrime),
            q.height = 1 ∧ (D.1.comap f).stalkIdeal u ≤ q ∧
              q.comap (f.stalkMap u).hom = p := by
  obtain ⟨U, f, u, hf, hfu, hstrict⟩ := hNC
  let : Etale f := hf
  refine ⟨U, f, u, hfu, hf, hstrict, ?_, ?_⟩
  · apply Scheme.IdealSheafData.HasCharacteristicZeroBranchesAt.comap_of_etale
      f u
    simpa only [hfu] using
      hD.hasCharacteristicZeroBranchesAt D structural
  · exact D.exists_etaleHeightOnePrime_over_componentBranchPrimeAt
      Z hZ z hz f u hfu

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.