Module

QuadraticFieldDiscriminant.lean

Nyll.SawinTotallyRealTowers.QuadraticFieldDiscriminant

3 declarations indexed from sourceView source ↗

Module documentation

Discriminants of squarefree quadratic number fields

The constructed bases of the full ring of integers determine the number field discriminant. Integer traces agree with rational traces after scalar extension, so the two-by-two trace determinants give 4d or d according to the signed radicand modulo four.

Imports8

Nyll.SawinTotallyRealTowers.QuadraticBasisDiscriminant
Nyll.SawinTotallyRealTowers.QuadraticIntegerBasis
Mathlib.NumberTheory.NumberField.Discriminant.Defs
Mathlib.NumberTheory.NumberField.Norm
Mathlib.Tactic.FinCases
Mathlib.Tactic.LinearCombination
Mathlib.Tactic.NormNum
Mathlib.Tactic.Ring

Imported by4

theorem

coe_discr_int_fin_two

L32 ↗

ClassFieldTower.Sawin.coe_discr_int_fin_two

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · full declaration

theorem coe_discr_int_fin_two
    (L : Type u) [Field L] [NumberField L] (b : Fin 2 → 𝓞 L) :
    (Algebra.discr ℤ b : ℚ) = Algebra.discr ℚ (fun i ↦ (b i : L)) := by
  simp only [Algebra.discr_def, Matrix.det_fin_two, Algebra.traceMatrix_apply,
    Algebra.traceForm_apply, Int.cast_sub, Int.cast_mul, Algebra.coe_trace_int,
    RingOfIntegers.coe_eq_algebraMap, map_mul]

theorem

numberField_discr_of_mod_four_ne_one

L41 ↗

ClassFieldTower.Sawin.numberField_discr_of_mod_four_ne_one

Documentation

A signed squarefree radicand not congruent to one modulo four gives number field discriminant 4d.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem numberField_discr_of_mod_four_ne_one
    (L : Type u) [Field L] [NumberField L] [Algebra.IsQuadraticExtension ℚ L]
    (d : ℤ) (hd : Squarefree d.natAbs) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ))
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (hMod : d % 4 ≠ 1) : NumberField.discr L = 4 * d

theorem

numberField_discr_of_mod_four_eq_one

L65 ↗

ClassFieldTower.Sawin.numberField_discr_of_mod_four_eq_one

Documentation

A signed squarefree radicand congruent to one modulo four gives number field discriminant d.

Source context 4 commands

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

open scoped NumberField
open NumberField
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem numberField_discr_of_mod_four_eq_one
    (L : Type u) [Field L] [NumberField L] [Algebra.IsQuadraticExtension ℚ L]
    (d : ℤ) (hd : Squarefree d.natAbs) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L (d : ℚ))
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (hMod : d % 4 = 1) : NumberField.discr L = d

Module documentation

Discriminants of squarefree quadratic number fields

Declarations

coe_discr_int_fin_two

numberField_discr_of_mod_four_ne_one

numberField_discr_of_mod_four_eq_one