Module

QuadraticTrace.lean

Nyll.SawinTotallyRealTowers.QuadraticTrace

6 declarations indexed from sourceView source ↗

Module documentation

Traces and norms in quadratic coordinates

A square-root generator of a quadratic extension has minimal polynomial X² - d. Its trace and norm, and those of every rational linear combination of 1 and the generator, follow from the power basis and a two-dimensional determinant identity.

Imports4

Nyll.SawinTotallyRealTowers.QuadraticGenerator
Mathlib.RingTheory.Adjoin.PowerBasis
Mathlib.RingTheory.Norm.Basic
Mathlib.RingTheory.Trace.Basic

Imported by4

theorem

minpoly_quadratic_generator

L32 ↗

ClassFieldTower.Sawin.minpoly_quadratic_generator

Documentation

The square-root generator of a quadratic extension has the expected minimal polynomial.

Source context 4 commands

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

noncomputable section
universe u
namespace ClassFieldTower.Sawin
variable (L : Type u) [Field L] [Algebra ℚ L]
    [Algebra.IsQuadraticExtension ℚ L]

Lean source · statement

theorem minpoly_quadratic_generator (d : ℚ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L d)
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    minpoly ℚ α = Polynomial.X ^ 2 - Polynomial.C d

theorem

trace_quadratic_generator

L48 ↗

ClassFieldTower.Sawin.trace_quadratic_generator

Documentation

A square-root generator has trace zero.

Source context 4 commands

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

noncomputable section
universe u
namespace ClassFieldTower.Sawin
variable (L : Type u) [Field L] [Algebra ℚ L]
    [Algebra.IsQuadraticExtension ℚ L]

Lean source · statement

theorem trace_quadratic_generator (d : ℚ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L d)
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    Algebra.trace ℚ L α = 0

theorem

norm_quadratic_generator

L63 ↗

ClassFieldTower.Sawin.norm_quadratic_generator

Documentation

A square-root generator of square d has norm -d.

Source context 4 commands

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

noncomputable section
universe u
namespace ClassFieldTower.Sawin
variable (L : Type u) [Field L] [Algebra ℚ L]
    [Algebra.IsQuadraticExtension ℚ L]

Lean source · statement

theorem norm_quadratic_generator (d : ℚ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L d)
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    Algebra.norm ℚ α = -d

theorem

trace_quadratic_coordinates

L79 ↗

ClassFieldTower.Sawin.trace_quadratic_coordinates

Documentation

The trace is twice the constant coordinate.

Source context 4 commands

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

noncomputable section
universe u
namespace ClassFieldTower.Sawin
variable (L : Type u) [Field L] [Algebra ℚ L]
    [Algebra.IsQuadraticExtension ℚ L]

Lean source · statement

theorem trace_quadratic_coordinates (d a b : ℚ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L d)
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    Algebra.trace ℚ L (algebraMap ℚ L a + algebraMap ℚ L b * α) = 2 * a

theorem

norm_quadratic_affine

L89 ↗

ClassFieldTower.Sawin.norm_quadratic_affine

Source context 4 commands

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

noncomputable section
universe u
namespace ClassFieldTower.Sawin
variable (L : Type u) [Field L] [Algebra ℚ L]
    [Algebra.IsQuadraticExtension ℚ L]

Lean source · statement

theorem norm_quadratic_affine (a b : ℚ) (α : L) :
    Algebra.norm ℚ (algebraMap ℚ L a + algebraMap ℚ L b * α) =
      a ^ 2 + a * b * Algebra.trace ℚ L α + b ^ 2 * Algebra.norm ℚ α

theorem

norm_quadratic_coordinates

L105 ↗

ClassFieldTower.Sawin.norm_quadratic_coordinates

Documentation

The norm is the binary quadratic form a² - d b².

Source context 4 commands

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

noncomputable section
universe u
namespace ClassFieldTower.Sawin
variable (L : Type u) [Field L] [Algebra ℚ L]
    [Algebra.IsQuadraticExtension ℚ L]

Lean source · statement

theorem norm_quadratic_coordinates (d a b : ℚ) (α : L)
    (hSquare : α ^ 2 = algebraMap ℚ L d)
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    Algebra.norm ℚ (algebraMap ℚ L a + algebraMap ℚ L b * α) = a ^ 2 - d * b ^ 2

Module documentation

Traces and norms in quadratic coordinates

Declarations

minpoly_quadratic_generator

trace_quadratic_generator

norm_quadratic_generator

trace_quadratic_coordinates

norm_quadratic_affine

norm_quadratic_coordinates