Yamaguchi26SolvableCoverings.isBoundaryUnramified_of_abelian_embedding
A finite cover whose deck group embeds into an abelian group has trivial boundary stabilizers under the arithmetic hypotheses. Cyclotomic inversion makes each character value have order dividing two, while Theorem 1.2 gives an odd order from the actual stabilizer subgroup.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open AlgebraicGeometry.FiniteEtale CategoryTheory.PreGaloisCategory
namespace Yamaguchi26SolvableCoverings
universe v
variable {X : Scheme.{0}} [ConnectedSpace X] [IsLocallyNoetherian X]Lean source · full declaration
theorem isBoundaryUnramified_of_abelian_embedding
(D : X.EffectiveCartierDivisor) (hhor : IsHorizontal D)
(hreg : D.IsAmbientRegularAlongSupport)
(hnc : D.HasNormalCrossingPointOfResidueCharacteristicOnEachComponent 2)
(hgeom : HasGeometricallyIntegralGenericComponents D.1) :
let : ConnectedSpace D.1.supportComplement := boundaryComplement_connectedSpace D hreg
∀ (W : FiniteEtale D.1.supportComplement) (_hW : IsGalois W)
{A : Type v} [CommGroup A] (e : (Aut W)ᵐᵒᵖ →* A),
Function.Injective e → IsBoundaryUnramified D W := by
intro hConnected
let : ConnectedSpace D.1.supportComplement := hConnected
intro W hW A _ e he E z hz
apply (Subgroup.eq_bot_iff_forall _).mpr
intro σ hσ
let s : finiteCoverInertia D W E z := ⟨σ, hσ⟩
have hodd : ¬ 2 ∣ Nat.card (finiteCoverInertia D W E z) :=
finite_inertia_control D hhor hreg E 2 Nat.prime_two (hnc E.val E.property) W hW z hz
have hinv : e (MulOpposite.op σ) = (e (MulOpposite.op σ))⁻¹ := by
have h := e.map_isConj (finiteCoverInertia_isConj_inv D hhor hreg hgeom W hW E z hz s)
simpa only [map_inv] using isConj_iff_eq.mp h
have htwo : (e (MulOpposite.op σ)) ^ 2 = 1 := by
rw [pow_two]
exact (congrArg (fun t => e (MulOpposite.op σ) * t) hinv).trans (mul_inv_cancel _)
have hcard : (e (MulOpposite.op σ)) ^ Nat.card (finiteCoverInertia D W E z) = 1 := by
have h := congrArg (fun t : finiteCoverInertia D W E z => e (MulOpposite.op (t : Aut W)))
(pow_card_eq_one' (x := s))
simpa only [Subgroup.coe_pow, MulOpposite.op_pow, map_pow,
Subgroup.coe_one, MulOpposite.op_one, map_one] using h
have hone : e (MulOpposite.op σ) = 1 := orderOf_eq_one_iff.mp
(Nat.eq_one_of_dvd_coprimes (Nat.prime_two.coprime_iff_not_dvd.mpr hodd)
(orderOf_dvd_of_pow_eq_one htwo) (orderOf_dvd_of_pow_eq_one hcard))
exact MulOpposite.op_injective (he (hone.trans (map_one e).symm))