ModuleSchemeNormalCrossingsComponentInertia.lean
Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.SchemeNormalCrossingsComponentInertia
3 declarations indexed from sourceView source ↗ Module documentation
Divisorial inertia on normal-crossings chart components
An etale strict chart can disconnect a connected Galois cover. The pointed connected component supplied by the pullback theorem is nevertheless Galois, and the split strict-normal-crossings inertia theorem applies directly to that component.
Declarations
AlgebraicGeometry.Scheme.IdealSheafData.GaloisCoverQuotientIdealInertiaCoprime
DocumentationThe pointed quotient ideal-inertia statement for one connected Galois cover of a split boundary-away chart.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u uk
variable {X : Scheme.{u}}
AlgebraicGeometry.Scheme.IdealSheafData.exists_galoisComponent_pullbackSupportComplementCoverToBoundaryAway_quotientIdealInertia_coprime
DocumentationOn a split local chart inside an etale normal-crossings neighbourhood, the pointed connected component of a pulled-back global Galois cover has quotient ideal inertia prime to the selected residue characteristic.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u uk
variable {X : Scheme.{u}}
AlgebraicGeometry.Scheme.IdealSheafData.IsNormalCrossingsAt.exists_etaleStrictChart_galoisComponent_quotientIdealInertia_coprime
DocumentationA normal-crossings point has an etale strict chart on which the arithmetic height-two construction produces, for every global Galois cover, a Galois component whose pointed quotient ideal inertia is prime to the residue characteristic.
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory IsLocalRing
open CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u uk
variable {X : Scheme.{u}}
Lean source · full declarationtheorem IsNormalCrossingsAt.exists_etaleStrictChart_galoisComponent_quotientIdealInertia_coprime
[IsIntegral X]
{I : X.IdealSheafData} {x : X}
(hI : I.IsNormalCrossingsAt x) :
∃ (U : Scheme.{u}) (f : U ⟶ X) (u : U),
Etale f ∧ f u = x ∧ (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)
{k : Type uk} [CommRing k] [Nontrivial k]
(_phi : (U.presheaf.stalk u ⧸ q) →+* k)
(p : ℕ) [CharP k p] (_hp : p.Prime),
let A := U.presheaf.stalk u
∃ P : AlgebraicGeometry.Spec A,
q < P.asIdeal ∧ P.asIdeal.height = 2 ∧
let : P.asIdeal.IsPrime := P.isPrime
let V := Localization.AtPrime P.asIdeal
let qV := q.map (algebraMap A V)
∃ (r : ℕ) (t : Fin 2 → V) (branch : Fin 2)
(hVdomain : IsDomain V)
(hVregular : IsRegularRing V)
(hVnormal : IsIntegrallyClosed V)
(hboundary :
((I.comap f).stalkIdeal u).map (algebraMap A V) =
Ideal.span {boundaryProduct t r})
(hNC : IsSplitStrictNormalCrossingsAt
(boundaryProduct t r) t r)
(_hbranch : branch.1 < r)
(_hqV : qV = Ideal.span {t branch})
(_hlocalizedCharZero : ∀ j : Fin 2, j.1 < r →
CharZero (V ⧸ Ideal.span {t j}))
(_hpV : CharP (V ⧸ maximalIdeal V) p),
letI : IsDomain V := hVdomain
letI : IsRegularRing V := hVregular
letI : IsIntegrallyClosed V := hVnormal
let hf :=
Kummer.splitStrictNormalCrossings_boundaryEquation_ne_zero
hNC
letI : IsDomain
(Localization.Away (boundaryProduct t r)) :=
IsLocalization.Away.isDomain
(Localization.Away (boundaryProduct t r)) hf
let j := localizationAwayToSupportComplement
(I.comap f) u P.asIdeal
(boundaryProduct t r) hboundary
let g := comapSupportComplementTo I f
letI : Nonempty (I.comap f).supportComplement :=
⟨j (genericPoint
(Spec (.of
(Localization.Away (boundaryProduct t r)))))⟩
letI : Nonempty I.supportComplement :=
⟨g (Classical.choice
(inferInstance :
Nonempty (I.comap f).supportComplement))⟩
∀ (W : FiniteEtale I.supportComplement), IsGalois W →
∃ (Z : FiniteEtale
(Spec (.of
(Localization.Away (boundaryProduct t r)))))
(component : Z ⟶
pullbackSupportComplementCoverToChartBoundaryAway
I f u P t hboundary W)
(_hZ : IsGalois Z),
Mono component ∧
GaloisCoverQuotientIdealInertiaCoprime
hNC qV Z p := by
obtain ⟨U, f, u, hf, hfu, hstrict⟩ := hI
refine ⟨U, f, u, hf, hfu, hstrict, ?_⟩
intro hCharZero q hqPrime hqheight hIq k instCommRing instNontrivial
phi p hpChar hp
let : q.IsPrime := hqPrime
obtain ⟨P, hqP, hPheight, r, t, branch, hVdomain, hVregular,
hVnormal, hboundary, hNC, hbranch, hqV, hlocalizedCharZero,
hpV, hcoprime⟩ :=
hstrict.exists_arithmeticLocalSplitChart_galoisCover_quotientIdealInertia_coprime
hCharZero q hqheight hIq phi p hp
let : P.asIdeal.IsPrime := P.isPrime
refine ⟨P, hqP, hPheight, r, t, branch, hVdomain, hVregular,
hVnormal, hboundary, hNC, hbranch, hqV, hlocalizedCharZero,
hpV, ?_⟩
dsimp only
let : IsDomain (Localization.AtPrime P.asIdeal) := hVdomain
let : IsRegularRing (Localization.AtPrime P.asIdeal) := hVregular
let : IsIntegrallyClosed (Localization.AtPrime P.asIdeal) := hVnormal
let hf :=
Kummer.splitStrictNormalCrossings_boundaryEquation_ne_zero
hNC
let : IsDomain (Localization.Away (boundaryProduct t r)) :=
IsLocalization.Away.isDomain
(Localization.Away (boundaryProduct t r)) hf
let j := localizationAwayToSupportComplement
(I.comap f) u P.asIdeal (boundaryProduct t r) hboundary
let g := comapSupportComplementTo I f
let : Nonempty (I.comap f).supportComplement :=
⟨j (genericPoint
(Spec (.of (Localization.Away (boundaryProduct t r)))))⟩
let : Nonempty I.supportComplement :=
⟨g (Classical.choice
(inferInstance : Nonempty (I.comap f).supportComplement))⟩
intro W hW
obtain ⟨Z, component, hZ, hcomponent⟩ :=
exists_galoisComponent_pullbackSupportComplementCoverToBoundaryAway
I f u P t hboundary hNC hVdomain W hW
refine ⟨Z, component, hZ, hcomponent, ?_⟩
dsimp only [GaloisCoverQuotientIdealInertiaCoprime]
intro hZ' Omega instField instSepClosed xi z Q hQprime hQqV
exact hcoprime Z hZ' xi z Q hQprime hQqV