Module

QuadraticSquareDescent.lean

Nyll.SawinTotallyRealTowers.QuadraticSquareDescent

1 declaration indexed from sourceView source ↗

Module documentation

Square classes that become squares in a quadratic extension

In a quadratic extension generated by a square root of a, an element of the base field becomes a square precisely when its square class is trivial or that of a. The basis 1, α makes the cross coefficient of a square explicit. In characteristic different from two, that coefficient vanishes only when one of the two coordinates vanishes.

Imports9

Mathlib.Algebra.BigOperators.Fin
Mathlib.Algebra.Group.Even
Mathlib.Data.Fin.SuccPred
Mathlib.FieldTheory.IntermediateField.Adjoin.Algebra
Mathlib.LinearAlgebra.Basis.Defs
Mathlib.LinearAlgebra.Dimension.Free
Mathlib.RingTheory.Adjoin.PowerBasis
Mathlib.RingTheory.PowerBasis
Mathlib.Tactic.LinearCombination

Imported by2

theorem

isSquare_algebraMap_iff_of_quadraticGenerator

L33 ↗

ClassFieldTower.Sawin.isSquare_algebraMap_iff_of_quadraticGenerator

Documentation

A quadratic extension generated by a square root kills exactly the trivial square class and the square class of its radicand.

Source context 2 commands

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

universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isSquare_algebraMap_iff_of_quadraticGenerator
    (F : Type u) (E : Type v) [Field F] [Field E] [Algebra F E]
    [Algebra.IsQuadraticExtension F E] (hTwo : (2 : F) ≠ 0)
    (a b : F) (α : E) (hSquare : α ^ 2 = algebraMap F E a)
    (hGenerate : IntermediateField.adjoin F ({α} : Set E) = ⊤) :
    IsSquare (algebraMap F E b) ↔ IsSquare b ∨ ∃ q : F, b = a * q ^ 2

Module documentation

Square classes that become squares in a quadratic extension

Declarations

isSquare_algebraMap_iff_of_quadraticGenerator