AlgebraicNumberTheory.Ramification.finrank_le_totient_prod_primePowers_of_chosen_primes
The generic global degree estimate used by the concrete inertia-field compositum.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace AlgebraicNumberTheory.Ramification
open NumberField
open HilbertRamification.Dedekind
open scoped NumberField IsMulCommutativeLean source · statement
theorem finrank_le_totient_prod_primePowers_of_chosen_primes
(M : Type) [Field M] [NumberField M] [IsAbelianGalois ℚ M]
(S : Finset Nat.Primes) (e : Nat.Primes → ℕ)
(chosen : ∀ p : Nat.Primes,
Ideal.primesOver (rationalPrimeIdeal p) (𝓞 M))
(hunramifiedOutside :
∀ (Q : Ideal (𝓞 M)) [Q.IsPrime] [Q.IsMaximal],
(¬ ∃ p ∈ S, rationalPrimeIdeal p = Q.under ℤ) →
Algebra.IsUnramifiedAt ℤ Q)
(hcard : ∀ p ∈ S,
Nat.card
(inertiaGroup (chosen p).1 (M ≃ₐ[ℚ] M)) ≤
Nat.totient (p.1 ^ e p)) :
Module.finrank ℚ M ≤
Nat.totient (∏ p ∈ S, p.1 ^ e p)