NYLL
Module

DegreeProduct.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.DegreeProduct
2 declarations indexed from sourceView source ↗

Module documentation

A finite-group degree product

Once the chosen inertia groups generate the full abelian Galois group and their orders satisfy the local prime-power bounds, the global degree is at most the totient of the conductor candidate. This file isolates that finite group calculation from the arithmetic construction of the chosen primes.

Imports3
Imported by2

Declarations

theorem

totient_prod_primePowers

L29 ↗
AlgebraicNumberTheory.Ramification.totient_prod_primePowers
Documentation

Euler's totient is multiplicative on a finite product of powers of distinct primes.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory.Ramification
open RamificationTheory
open scoped BigOperators IsMulCommutative
Lean source · statement
theorem totient_prod_primePowers
    (S : Finset Nat.Primes) (e : Nat.Primes → ℕ) :
    Nat.totient (∏ p ∈ S, p.1 ^ e p) =
      ∏ p ∈ S, Nat.totient (p.1 ^ e p)
theorem

finrank_le_totient_prod_primePowers_of_inertia_bounds

L48 ↗
AlgebraicNumberTheory.Ramification.finrank_le_totient_prod_primePowers_of_inertia_bounds
Documentation

The finite-group degree bound obtained from the inertia subgroups.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
namespace AlgebraicNumberTheory.Ramification
open RamificationTheory
open scoped BigOperators IsMulCommutative
Lean source · statement
theorem finrank_le_totient_prod_primePowers_of_inertia_bounds
    (M : Type) [Field M] [Algebra ℚ M]
    [FiniteDimensional ℚ M] [IsAbelianGalois ℚ M]
    (S : Finset Nat.Primes) (e : Nat.Primes → ℕ)
    (I : Nat.Primes → Subgroup (M ≃ₐ[ℚ] M))
    (hgenerate : S.sup I = ⊤)
    (hcard : ∀ p ∈ S, Nat.card (I p) ≤ Nat.totient (p.1 ^ e p)) :
    Module.finrank ℚ M ≤
      Nat.totient (∏ p ∈ S, p.1 ^ e p)

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.