NYLL
Module

ComponentMappedFiniteQuotientInertia.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.ComponentMappedFiniteQuotientInertia
8 declarations indexed from sourceView source ↗

Module documentation

Component-specific mapped finite-quotient inertia

The original complement only needs to be connected. Integrality and normality are constructed on the two-dimensional split chart and its connected Galois cover; neither is imposed on the ambient scheme or on the original complement. The local inertia order is supplied by the arithmetic normal-crossings theorem, and the pointed pullback-component map injects this group into the deck group of each original Galois cover.

Imports3
Imported by3

Declarations

def

HasMappedQuotientIdealInertiaCoprime

L35 ↗
AlgebraicGeometry.Scheme.IdealSheafData.HasMappedQuotientIdealInertiaCoprime
Documentation

The complete mapped finite-quotient inertia conclusion attached to one height-one prime on an etale chart of an ideal with connected complement.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def HasMappedQuotientIdealInertiaCoprime
    {X U : Scheme.{u}}
    (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
    (f : U ⟶ X) (u : U)
    (q : Ideal (U.presheaf.stalk u)) (p : ℕ) : Prop
def

LocalChartMappedQuotientInertiaCoprime

L138 ↗
AlgebraicGeometry.Scheme.IdealSheafData.LocalChartMappedQuotientInertiaCoprime
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def LocalChartMappedQuotientInertiaCoprime
    {X U : Scheme.{u}}
    (I : X.IdealSheafData) [ConnectedSpace I.supportComplement]
    (f : U ⟶ X) (u : U)
    (P : PrimeSpectrum (U.presheaf.stalk u))
    (r : ℕ) (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hVdomain : IsDomain (Localization.AtPrime P.asIdeal))
    (hVregular : IsRegularRing (Localization.AtPrime P.asIdeal))
    (hVnormal : IsIntegrallyClosed (Localization.AtPrime P.asIdeal))
    (hboundary :
      ((I.comap f).stalkIdeal u).map
          (algebraMap (U.presheaf.stalk u) (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r})
    (hLocalNC : IsSplitStrictNormalCrossingsAt
      (boundaryProduct t r) t r)
    (qV : Ideal (Localization.AtPrime P.asIdeal)) (p : ℕ) : Prop
def

PullbackComponentMappedQuotientInertiaCoprime

L225 ↗
AlgebraicGeometry.Scheme.IdealSheafData.PullbackComponentMappedQuotientInertiaCoprime
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
def PullbackComponentMappedQuotientInertiaCoprime
    {V : Type u} [CommRing V] [IsDomain V] [IsLocalRing V]
    [IsRegularRing V] [IsIntegrallyClosed V]
    {r : ℕ} {t : Fin 2 → V}
    (hNC : IsSplitStrictNormalCrossingsAt (boundaryProduct t r) t r)
    (qV : Ideal V) (p : ℕ)
    {U : Scheme.{u}} [ConnectedSpace U]
    (c : Spec (.of (Localization.Away (boundaryProduct t r))) ⟶ U)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶
      Spec (.of (Localization.Away (boundaryProduct t r))))
    (W : FiniteEtale U) (hW : IsGalois W)
    (w : (FiniteEtale.fiber (xi ≫ c)).obj W) : Prop
theorem

exists_pullbackComponentMappedQuotientInertiaCoprime

L293 ↗
AlgebraicGeometry.Scheme.IdealSheafData.exists_pullbackComponentMappedQuotientInertiaCoprime
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem exists_pullbackComponentMappedQuotientInertiaCoprime
    {V : Type u} [CommRing V] [IsDomain V] [IsLocalRing V]
    [IsRegularRing V] [IsIntegrallyClosed V]
    {r : ℕ} {t : Fin 2 → V}
    (hNC : IsSplitStrictNormalCrossingsAt (boundaryProduct t r) t r)
    (qV : Ideal V) (p : ℕ)
    {U : Scheme.{u}} [ConnectedSpace U]
    (c : Spec (.of (Localization.Away (boundaryProduct t r))) ⟶ U)
    {Omega : Type u} [Field Omega] [IsSepClosed Omega]
    (xi : Spec (.of Omega) ⟶
      Spec (.of (Localization.Away (boundaryProduct t r))))
    (W : FiniteEtale U) (hW : IsGalois W)
    (w : (FiniteEtale.fiber (xi ≫ c)).obj W)
    (hLocal : PointedGaloisQuotientInertiaCoprime hNC qV p) :
    PullbackComponentMappedQuotientInertiaCoprime hNC qV p c xi W hW w
theorem

localChartMappedQuotientInertiaCoprime_of_pointed

L327 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localChartMappedQuotientInertiaCoprime_of_pointed
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · full declaration
theorem localChartMappedQuotientInertiaCoprime_of_pointed
    {X U : Scheme.{u}}
    {I : X.IdealSheafData} [ConnectedSpace I.supportComplement]
    (f : U ⟶ X) (u : U)
    (P : PrimeSpectrum (U.presheaf.stalk u))
    (r : ℕ) (t : Fin 2 → Localization.AtPrime P.asIdeal)
    (hVdomain : IsDomain (Localization.AtPrime P.asIdeal))
    (hVregular : IsRegularRing (Localization.AtPrime P.asIdeal))
    (hVnormal : IsIntegrallyClosed (Localization.AtPrime P.asIdeal))
    (hboundary :
      ((I.comap f).stalkIdeal u).map
          (algebraMap (U.presheaf.stalk u) (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r})
    (hLocalNC : IsSplitStrictNormalCrossingsAt
      (boundaryProduct t r) t r)
    (qV : Ideal (Localization.AtPrime P.asIdeal)) (p : ℕ)
    (hLocal :
      let V := Localization.AtPrime P.asIdeal
      letI : IsDomain V := hVdomain
      letI : IsRegularRing V := hVregular
      letI : IsIntegrallyClosed V := hVnormal
      PointedGaloisQuotientInertiaCoprime hLocalNC qV p) :
    LocalChartMappedQuotientInertiaCoprime I f u P r t hVdomain
      hVregular hVnormal hboundary hLocalNC qV p := by
  dsimp only [LocalChartMappedQuotientInertiaCoprime]
  let V := Localization.AtPrime P.asIdeal
  let : IsDomain V := hVdomain
  let : IsRegularRing V := hVregular
  let : IsIntegrallyClosed V := hVnormal
  let boundary := boundaryProduct t r
  have hboundary_ne : boundary ≠ 0 :=
    EtaleFundamentalGroups.Kummer.splitStrictNormalCrossings_boundaryEquation_ne_zero
      hLocalNC
  let Away := Localization.Away boundary
  let : IsDomain Away :=
    IsLocalization.Away.isDomain Away hboundary_ne
  let : IsIntegrallyClosed Away :=
    isIntegrallyClosed_of_isLocalization Away
      (Submonoid.powers boundary)
      (Submonoid.powers_le.mpr
        (mem_nonZeroDivisors_iff_ne_zero.mpr hboundary_ne))
  let c := IdealSheafData.boundaryAwayToSupportComplement
    I f u P t hboundary
  intro W hW
  let s := genericPoint (Spec (.of Away))
  let Omega := AlgebraicClosure ((Spec (.of Away)).residueField s)
  let xi : Spec (.of Omega) ⟶ Spec (.of Away) :=
    Spec.map (CommRingCat.ofHom
      (algebraMap ((Spec (.of Away)).residueField s) Omega)) ≫
      (Spec (.of Away)).fromSpecResidueField s
  let : IsGalois W := hW
  let w : (FiniteEtale.fiber (xi ≫ c)).obj W :=
    Classical.choice
      (nonempty_fiber_of_isConnected (FiniteEtale.fiber (xi ≫ c)) W)
  exact exists_pullbackComponentMappedQuotientInertiaCoprime
    hLocalNC qV p c xi W hW w hLocal
theorem

hasMappedQuotientIdealInertiaCoprime_of_localChart

L384 ↗
AlgebraicGeometry.Scheme.IdealSheafData.hasMappedQuotientIdealInertiaCoprime_of_localChart
Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · full declaration
theorem hasMappedQuotientIdealInertiaCoprime_of_localChart
    {X U : Scheme.{u}}
    {I : X.IdealSheafData} [ConnectedSpace I.supportComplement]
    (f : U ⟶ X) (u : U)
    (q : Ideal (U.presheaf.stalk u)) (p : ℕ)
    (P : PrimeSpectrum (U.presheaf.stalk u))
    (hqP : q < P.asIdeal) (hPheight : P.asIdeal.height = 2)
    (r : ℕ) (t : Fin 2 → Localization.AtPrime P.asIdeal) (branch : Fin 2)
    (hVdomain : IsDomain (Localization.AtPrime P.asIdeal))
    (hVregular : IsRegularRing (Localization.AtPrime P.asIdeal))
    (hVnormal : IsIntegrallyClosed (Localization.AtPrime P.asIdeal))
    (hboundary :
      ((I.comap f).stalkIdeal u).map
          (algebraMap (U.presheaf.stalk u) (Localization.AtPrime P.asIdeal)) =
        Ideal.span {boundaryProduct t r})
    (hLocalNC : IsSplitStrictNormalCrossingsAt
      (boundaryProduct t r) t r)
    (hbranch : branch.1 < r)
    (hqV : q.map
      (algebraMap (U.presheaf.stalk u) (Localization.AtPrime P.asIdeal)) =
        Ideal.span {t branch})
    (hlocalizedCharZero : ∀ j : Fin 2, j.1 < r →
      CharZero (Localization.AtPrime P.asIdeal ⧸ Ideal.span {t j}))
    (hpV : CharP
      (Localization.AtPrime P.asIdeal ⧸ maximalIdeal (Localization.AtPrime P.asIdeal)) p)
    (hLocal :
      let V := Localization.AtPrime P.asIdeal
      let qV := q.map (algebraMap (U.presheaf.stalk u) V)
      letI : IsDomain V := hVdomain
      letI : IsRegularRing V := hVregular
      letI : IsIntegrallyClosed V := hVnormal
      PointedGaloisQuotientInertiaCoprime hLocalNC qV p) :
    I.HasMappedQuotientIdealInertiaCoprime f u q p := by
  dsimp only [HasMappedQuotientIdealInertiaCoprime]
  refine ⟨P, hqP, hPheight, r, t, branch, hVdomain, hVregular,
    hVnormal, hboundary, hLocalNC, hbranch, hqV,
    hlocalizedCharZero, hpV, ?_⟩
  exact localChartMappedQuotientInertiaCoprime_of_pointed
    f u P r t hVdomain hVregular hVnormal hboundary hLocalNC
      (q.map (algebraMap (U.presheaf.stalk u)
        (Localization.AtPrime P.asIdeal))) p hLocal
theorem

hasMappedQuotientIdealInertiaCoprime

L429 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossings.hasMappedQuotientIdealInertiaCoprime
Documentation

Strict normal crossings and characteristic zero along all chart branches produce the complete mapped inertia conclusion for one selected height-one chart prime. Only the original complement is required to be connected.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData
Lean source · statement
theorem IsStrictNormalCrossings.hasMappedQuotientIdealInertiaCoprime
    {X U : Scheme.{u}}
    {I : X.IdealSheafData} [ConnectedSpace I.supportComplement]
    (f : U ⟶ X) (u : U)
    (hstrict : (I.comap f).IsStrictNormalCrossings)
    (hCharZero : (I.comap f).HasCharacteristicZeroBranchesAt u)
    (q : Ideal (U.presheaf.stalk u)) [q.IsPrime]
    (hqheight : q.height = 1)
    (hIq : (I.comap f).stalkIdeal u ≤ q)
    (p : ℕ) [CharP (U.residueField u) p] (hp : p.Prime) :
    I.HasMappedQuotientIdealInertiaCoprime f u q p
theorem

exists_etaleStrictChart_component_mappedQuotientIdealInertia_coprime

L470 ↗
AlgebraicGeometry.Scheme.EffectiveCartierDivisor.ComponentsThroughPointAreHorizontal.exists_etaleStrictChart_component_mappedQuotientIdealInertia_coprime
Documentation

For a specified component through a locally horizontal normal-crossings point, the canonical component branch lifts to a strict etale chart and has actual mapped ideal inertia of order prime to the residue characteristic in every connected Galois finite quotient of the original connected complement. The ambient scheme need not be integral or normal.

Source context 8 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing TopologicalSpace
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
universe u
namespace AlgebraicGeometry.Scheme.EffectiveCartierDivisor
variable {X S : Scheme.{u}}
namespace ComponentsThroughPointAreHorizontal
Lean source · full declaration
theorem exists_etaleStrictChart_component_mappedQuotientIdealInertia_coprime
    [IsLocallyNoetherian X] [IsIntegral S]
    (D : EffectiveCartierDivisor X) [ConnectedSpace D.1.supportComplement]
    (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))
    (p : ℕ) [CharP (X.residueField (D.1.subschemeι z)) p]
    (hp : p.Prime) :
    ∃ (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 branchPrime : 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 = branchPrime ∧
                D.1.HasMappedQuotientIdealInertiaCoprime f u q p := by
  obtain ⟨U, f, u, hfu, hf, hstrict, hCharZero,
      q, hqPrime, hqheight, hIq, hqcomap⟩ :=
    hD.exists_etaleStrictChart_componentBranch
      D structural Z hZ z hz hNC
  let : Etale f := hf
  let : q.IsPrime := hqPrime
  have hresidueChar : ringChar (U.residueField u) = p := by
    rw [Scheme.Hom.ringChar_residueField_eq f u, hfu]
    exact ringChar.eq (X.residueField (D.1.subschemeι z)) p
  let : CharP (U.residueField u) p := ringChar.of_eq hresidueChar
  refine ⟨U, f, u, hfu, hf, hstrict, hCharZero,
    q, hqPrime, hqheight, hIq, hqcomap, ?_⟩
  exact hstrict.hasMappedQuotientIdealInertiaCoprime
    f u hCharZero q hqheight hIq p hp

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