Module

GaloisDifferentBound.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.GaloisDifferentBound

1 declaration indexed from sourceView source ↗

Module documentation

The different at a prime not dividing a Galois degree

The local factor P^e of q times the integer ring has absolute norm q^(ef). The Galois fundamental identity makes ef a divisor of the extension degree, so it is prime to q. The literal CRT trace witness then proves that P^e does not divide the different. No completion comparison or an assumed different-exponent formula is used.

Imports6

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.TameDifferentTrace
Mathlib.NumberTheory.RamificationInertia.Galois
Mathlib.RingTheory.RamificationInertia.Ramification
Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Mathlib.RingTheory.RamificationInertia.Inertia
Mathlib.FieldTheory.Galois.Basic

Imported by2

theorem

ramification_power_not_dvd_differentIdeal_of_not_dvd_degree

L33 ↗

AlgebraicNumberTheory.Discriminant.ramification_power_not_dvd_differentIdeal_of_not_dvd_degree

Documentation

A full ramification power cannot divide the different at a rational prime that does not divide the finite Galois degree.

Source context 4 commands

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

open scoped NumberField
open NumberField
noncomputable section
namespace AlgebraicNumberTheory.Discriminant

Lean source · statement

theorem ramification_power_not_dvd_differentIdeal_of_not_dvd_degree
    (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L]
    (q : ℕ) (hq : q.Prime) (P : Ideal (𝓞 L)) [P.IsMaximal]
    [P.LiesOver (Ideal.span {(q : ℤ)})]
    (hDegree : ¬ q ∣ Module.finrank ℚ L) :
    ¬ P ^ P.ramificationIdx ℤ ∣ differentIdeal ℤ (𝓞 L)

Module documentation

The different at a prime not dividing a Galois degree

Declarations

ramification_power_not_dvd_differentIdeal_of_not_dvd_degree