Module

TameDifferentTrace.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.TameDifferentTrace

1 declaration indexed from sourceView source ↗

Module documentation

A trace witness bounds a primary factor of the different

For a coprime factorization of q times the integer ring, the Chinese remainder idempotent (1, 0) has trace equal to the dimension of the first factor. If that factor has norm q^m and q does not divide m, its trace is nonzero modulo q. Mathlib's trace-dual criterion then shows that the first factor cannot divide the different. The factor need not be prime.

Imports8

Mathlib.NumberTheory.NumberField.Discriminant.Different
Mathlib.RingTheory.Ideal.Int
Mathlib.FieldTheory.Finiteness
Mathlib.RingTheory.DedekindDomain.Different
Mathlib.RingTheory.Ideal.Quotient.Operations
Mathlib.RingTheory.Ideal.Norm.AbsNorm
Mathlib.RingTheory.Trace.Defs
Mathlib.RingTheory.Trace.Basic

Imported by2

theorem

not_dvd_differentIdeal_of_coprime_norm_exponent

L35 ↗

AlgebraicNumberTheory.Discriminant.not_dvd_differentIdeal_of_coprime_norm_exponent

Documentation

A primary factor whose residue dimension is prime to q cannot divide an entire additional power into the different.

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 not_dvd_differentIdeal_of_coprime_norm_exponent
    (L : Type*) [Field L] [NumberField L]
    (q m : ℕ) (hq : q.Prime)
    (R Q : Ideal (𝓞 L)) (hRQ : IsCoprime R Q)
    (hMul : R * Q = (Ideal.span {(q : ℤ)}).map (algebraMap ℤ (𝓞 L)))
    (hNorm : R.absNorm = q ^ m) (hm : ¬ q ∣ m) :
    ¬ R ∣ differentIdeal ℤ (𝓞 L)

Module documentation

A trace witness bounds a primary factor of the different

Declarations

not_dvd_differentIdeal_of_coprime_norm_exponent