Module

SupportedDiscriminantBound.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.SupportedDiscriminantBound

2 declarations indexed from sourceView source ↗

Module documentation

A discriminant bound from a prime-to-degree ramification support

Every prime factor of the different lies above a rational divisor of the discriminant. The CRT trace bound controls its exponent by the exponent in the corresponding rational prime ideal. Hence the different divides (c), and taking the absolute ideal norm gives |disc(L)| <= c^[L:Q]. The Galois hypothesis is retained: it is what makes each e*f divide the whole extension degree.

Imports8

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.GaloisDifferentBound
Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
Mathlib.Data.Multiset.Count
Mathlib.NumberTheory.NumberField.Discriminant.Different
Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Mathlib.RingTheory.Ideal.Norm.AbsNorm
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.RamificationInertia.Ramification

Imported by2

theorem

differentIdeal_dvd_span_of_coprime_support

L36 ↗

AlgebraicNumberTheory.Discriminant.differentIdeal_dvd_span_of_coprime_support

Documentation

The different divides a supported rational integer prime to the Galois degree.

Source context 4 commands

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

open scoped NumberField
open NumberField UniqueFactorizationMonoid
noncomputable section
namespace AlgebraicNumberTheory.Discriminant

Lean source · statement

theorem differentIdeal_dvd_span_of_coprime_support
    (L : Type*) [Field L] [NumberField L] [IsGalois ℚ L]
    (c : ℕ) (hc : 0 < c) (hcn : Nat.Coprime c (Module.finrank ℚ L))
    (hSupport : ∀ q : Nat.Primes, (q : ℤ) ∣ NumberField.discr L → (q : ℕ) ∣ c) :
    differentIdeal ℤ (𝓞 L) ∣ Ideal.span {(c : 𝓞 L)}

theorem

natAbs_discr_le_pow_of_coprime_support

L99 ↗

AlgebraicNumberTheory.Discriminant.natAbs_discr_le_pow_of_coprime_support