theorem
L31 ↗natCoprime_natCard_localizedNormalizationInertia_of_etale_splitStrictNormalCrossingsLatticeCover
EtaleFundamentalGroups.Kummer.natCoprime_natCard_localizedNormalizationInertia_of_etale_splitStrictNormalCrossingsLatticeCover
Localized normalization inertia in an étale lattice cover of the complement of a split strict-normal-crossings boundary has order prime to every residue characteristic detected on the original boundary ring.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace EtaleFundamentalGroups.Kummer
open scoped BigOperators
universe uR uS uA ukLean source · full declaration
theorem
natCoprime_natCard_localizedNormalizationInertia_of_etale_splitStrictNormalCrossingsLatticeCover
{R : Type uR} {S L : Type uS} {k : Type uk}
[CommRing R] [IsDomain R] [IsLocalRing R]
[CommRing S] [Algebra R S]
{d r : ℕ} (f : R) (t : Fin d → R)
(hNC : IsSplitStrictNormalCrossingsAt f t r)
[IsLocalization.Away f S]
(hBoundaryCharZero :
∀ i : Fin d, i.1 < r → CharZero (R ⧸ Ideal.span {t i}))
[AddCommGroup L] [Module.Free ℤ L] [Module.Finite ℤ L]
(H : Submodule ℤ L) [Finite (L ⧸ H)]
[HasEnoughRootsOfUnity S
(Monoid.exponent (Multiplicative (L ⧸ H)))]
(hEtale : (AddMonoidAlgebra.mapDomainRingHom S
H.subtype.toAddMonoidHom).Etale)
[CommRing k] [Nontrivial k]
(φ : R →+* k) (p : ℕ) [CharP k p] (hp : p.Prime) :
letI : IsLocalization.Away
(∏ i ∈ boundaryIndices d r, t i) S := by
change IsLocalization.Away (boundaryProduct t r) S
exact IsLocalization.Away.of_associated hNC.2.2.2.2.1
let hBoundary_ne :
(∏ i ∈ boundaryIndices d r, t i) ≠ 0 :=
Finset.prod_ne_zero_iff.mpr fun i hi ↦
(hNC.2.2.2.1 i (Finset.mem_filter.mp hi).2).ne_zero
letI : IsDomain S :=
IsLocalization.Away.isDomain S hBoundary_ne
let A₀ := AddMonoidAlgebra S H
let B := AddMonoidAlgebra S L
letI : UniqueSums L := latticeUniqueSums_of_freeIntModule L
letI : UniqueSums H :=
latticeSubgroupUniqueSums H.toAddSubgroup
letI : IsDomain A₀ := inferInstance
letI : IsDomain B := inferInstance
letI : Algebra A₀ B :=
latticeMapDomainAlgebra H.toAddSubgroup
letI : FaithfulSMul A₀ B :=
latticeMapDomainFaithfulSMul H.toAddSubgroup
let K := FractionRing A₀
let E := FractionRing B
letI : Algebra K E := FractionRing.liftAlgebra A₀ E
∀ (A : Type uA) [CommRing A] [IsDomain A]
[Algebra A K] [IsFractionRing A K]
[Algebra A E] [IsScalarTower A K E]
(P : Ideal A) [P.IsPrime]
(Q : Ideal (integralClosure A E)),
Nat.Coprime
(Nat.card
(localizedNormalizationInertia (K := K) (L := E) P Q)) p := by
dsimp only
have ht : ∀ i ∈ boundaryIndices d r, Prime (t i) := by
intro i hi
exact hNC.2.2.2.1 i (Finset.mem_filter.mp hi).2
have hCharZero :
∀ i ∈ boundaryIndices d r,
CharZero (R ⧸ Ideal.span {t i}) := by
intro i hi
exact hBoundaryCharZero i (Finset.mem_filter.mp hi).2
let : IsLocalization.Away
(∏ i ∈ boundaryIndices d r, t i) S := by
change IsLocalization.Away (boundaryProduct t r) S
exact IsLocalization.Away.of_associated hNC.2.2.2.2.1
exact
natCoprime_natCard_localizedNormalizationInertia_of_etale_boundaryLatticeCover
(R := R) (S := S) (L := L) (k := k)
(boundaryIndices d r) t ht hCharZero H hEtale φ p hp