EtaleFundamentalGroups.Inertia.finiteIdealNormalizationExponent_coprime_of_isUnit_base
Every integer invertible in the original base is coprime to the actual normalization exponent. The residue-field calculation and the characteristic power supplier are confined to this single finite extension.
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups.Inertia
universe u vLean source · statement
theorem finiteIdealNormalizationExponent_coprime_of_isUnit_base
(A : Type u) (B : Type v)
[CommRing A] [IsDomain A] [IsDiscreteValuationRing A]
[CommRing B] [IsDedekindDomain B] [Algebra A B]
[Module.Finite A B] [Module.IsTorsionFree A B]
[IsGaloisGroup (B ≃ₐ[A] B) A B]
(Q : Ideal B) [Q.IsMaximal] [Q.LiesOver (IsLocalRing.maximalIdeal A)] (hQ : Q ≠ ⊥)
(n : ℕ) (hn : IsUnit (n : A)) :
Nat.Coprime n (finiteIdealNormalizationExponent A B (B ≃ₐ[A] B) Q hQ)