theorem
L70 ↗finite_inertia_control
Yamaguchi26SolvableCoverings.finite_inertia_control
補題 1.2の固定部分群についての補助定理。 水平境界の成分 E に剰余標数 p の正規交差点があれば、 任意の連結有限 étale Galois 被覆の E における惰性群の位数は p と互いに素。
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
open EtaleFundamentalGroups EtaleFundamentalGroups.Inertia
namespace Yamaguchi26SolvableCoverings
variable {X : Scheme.{0}} [ConnectedSpace X] [IsLocallyNoetherian X]Lean source · full declaration
theorem finite_inertia_control
(D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
(hreg : D.IsAmbientRegularAlongSupport) (E : Component D)
(p : ℕ) (hp : p.Prime)
(hnc : ∃ x : D.1.subscheme, x ∈ E.val ∧
ringChar (X.residueField (D.1.subschemeι x)) = p ∧
D.IsNormalCrossingsAt (D.1.subschemeι x)) :
letI : ConnectedSpace D.1.supportComplement :=
boundaryComplement_connectedSpace D hreg
∀ (W : FiniteEtale D.1.supportComplement) (_hW : IsGalois W)
(z : Spec (.of (AlgebraicClosure (X.residueField (componentPoint D E)))) ⟶
(W.hom ≫ D.1.supportComplement.ι).normalization),
z ≫ (W.hom ≫ D.1.supportComplement.ι).fromNormalization =
componentGeometricPoint D E →
¬ p ∣ Nat.card (finiteCoverInertia D W E z) := by
let : ConnectedSpace D.1.supportComplement := boundaryComplement_connectedSpace D hreg
intro W hW z hz
obtain ⟨U, f, hf, u, q, hq, hmapped, hpoint⟩ :=
exists_arithmeticBoundaryChart_with_componentGeometricPoint D hhor hreg E p hp hnc
let : Etale f := hf
let : q.IsPrime := hq
obtain ⟨P, hqP, hPheight, r, t, branch, hVdomain, hVregular, hVnormal,
hboundary, hNC, hbranch, hqV, hCharZero, hpV, _hmapped⟩ := hmapped
let : P.asIdeal.IsPrime := P.isPrime
let V := Localization.AtPrime P.asIdeal
let : IsDomain V := hVdomain
let : IsRegularRing V := hVregular
let : IsIntegrallyClosed V := hVnormal
obtain ⟨y, hyideal, hy⟩ := hpoint P.asIdeal P.isPrime hqP.le
have hzy : z ≫ (W.hom ≫ D.1.supportComplement.ι).fromNormalization =
y ≫ Scheme.localizationAtPrimeTo U u P.asIdeal ≫ f := by
exact hz.trans (by simpa only [Scheme.localizationAtPrimeTo, Category.assoc] using hy.symm)
obtain ⟨qA, hqA, hfixA⟩ :=
exists_boundaryAway_normalizationPoint D.1 f u P t hboundary W z y hzy
let b := boundaryProduct t r
have hb : b ≠ 0 := Kummer.splitStrictNormalCrossings_boundaryEquation_ne_zero hNC
let Away := Localization.Away b
let : IsDomain Away := IsLocalization.Away.isDomain Away hb
let : IsIntegrallyClosed Away := isIntegrallyClosed_of_isLocalization Away
(Submonoid.powers b)
(Submonoid.powers_le.mpr (mem_nonZeroDivisors_iff_ne_zero.mpr hb))
let c := D.1.boundaryAwayToSupportComplement f u P t hboundary
let a : Spec (.of Away) ⟶ Spec (.of V) :=
Spec.map (CommRingCat.ofHom (algebraMap V Away))
let s := genericPoint (Spec (.of Away))
let Ω := AlgebraicClosure ((Spec (.of Away)).residueField s)
let xi : Spec (.of Ω) ⟶ Spec (.of Away) :=
Spec.map (CommRingCat.ofHom (algebraMap ((Spec (.of Away)).residueField s) Ω)) ≫
(Spec (.of Away)).fromSpecResidueField s
obtain ⟨Z, i, qZ, zZ, w, hi, hZ, hiz, hqZ, hlift⟩ :=
exists_galoisComponent_normalizationPoint_fixed_lift c xi W hW a qA
let : Mono i := hi
let : IsGalois Z := hZ
let : IsIntegral Z.left := isIntegral_left_of_isConnected_finiteEtale Z
let K := (Spec (.of Away)).functionField
let L := Z.left.functionField
let : Algebra K L := finiteEtaleFunctionFieldAlgebra Z
let : Algebra V K := localizationAwaySpecFunctionFieldAlgebra b hb
let : Algebra V L := finiteEtaleAwayFunctionFieldAlgebra b hb Z
let : IsScalarTower V K L := finiteEtaleAway_functionField_isScalarTower b hb Z
let : IsFractionRing V K := localizationAwaySpecFunctionField_isFractionRing b hb
let : FiniteDimensional K L := finiteDimensional_functionField_of_finiteEtale_isConnected Z
let : _root_.IsGalois K L := isGalois_functionField_of_isGalois_finiteEtale Z hZ
obtain ⟨φ, hφbase, hφfix⟩ := exists_finiteEtaleAway_normalizationPoint_inertia_iff V b hb Z qZ
let Q := RingHom.ker φ
have hQprime : Q.IsPrime := RingHom.ker_isPrime φ
have hQbranch : Q.LiesOver (Ideal.span ({t branch} : Set V)) := by
have h := ker_liesOver_of_specMap_comp φ y (hφbase.trans (hqZ.trans hqA))
simpa only [hyideal, hqV] using h
let φV : (V ⧸ Ideal.span ({t branch} : Set V)) →+* (V ⧸ IsLocalRing.maximalIdeal V) :=
(localizationAtPrimeBranchQuotientToResidue q P.asIdeal hqP.le).comp
(Ideal.quotEquivOfEq hqV.symm).toRingHom
have hcoprime :=
Kummer.splitStrictNormalCrossings_finiteEtaleGaloisCover_normalizationInertia_coprime
(A := V) (k := V ⧸ IsLocalRing.maximalIdeal V)
hNC branch hbranch hCharZero Z hZ Q hQprime hQbranch φV p hpV hp
let J := Q.inertia Gal(L/K)
let e : (Aut Z)ᵐᵒᵖ ≃* Gal(L/K) := finiteEtaleAutOpFunctionFieldMulEquiv Z hZ
let μ : Gal(L/K) →* (Aut W)ᵐᵒᵖ :=
(FiniteEtale.galoisPullbackComponentQuotientMonoidHom c xi W hW w Z i zZ hiz hZ hi).comp
e.symm.toMonoidHom
have hincl : (finiteCoverInertia D W E z).op ≤ J.map μ := by
intro σ hσ
have hσfixed : z ≫ normalizationEndomorphism (W.hom ≫ D.1.supportComplement.ι)
σ.unop.hom.left (by
rw [← Category.assoc]
exact congrArg (fun k => k ≫ D.1.supportComplement.ι) σ.unop.hom.w) = z := hσ
obtain ⟨τ, hτimage, hτfixed⟩ := hlift σ.unop ((hfixA σ.unop).mpr hσfixed)
refine ⟨finiteEtaleAutFunctionFieldAlgEquiv Z τ, (hφfix τ).mpr hτfixed, ?_⟩
change (FiniteEtale.galoisPullbackComponentQuotientMonoidHom
c xi W hW w Z i zZ hiz hZ hi) (e.symm (e (MulOpposite.op τ))) = σ
rw [e.symm_apply_apply]
exact hτimage
have hdvd : Nat.card (finiteCoverInertia D W E z) ∣ Nat.card J := by
rw [Nat.card_congr (finiteCoverInertia D W E z).equivOp]
exact (Subgroup.card_dvd_of_le hincl).trans (J.card_map_dvd μ)
exact hp.coprime_iff_not_dvd.mp (hcoprime.of_dvd_left hdvd).symm