Module

SquareRootAdjoin.lean

Nyll.SawinTotallyRealTowers.SquareRootAdjoin

5 declarations indexed from sourceView source ↗

Module documentation

Adjoining a square root of a nonsquare

Over any base field, a square root of a nonsquare has minimal polynomial X² - a and generates an extension of degree two. No assumption on the characteristic or on the ambient extension is required.

Imports7

Mathlib.Algebra.Group.Even
Mathlib.Algebra.Polynomial.Degree.Operations
Mathlib.Algebra.Polynomial.Monic
Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
Mathlib.FieldTheory.KummerPolynomial
Mathlib.FieldTheory.Minpoly.Field
Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Imported by2

theorem

minpoly_squareRoot_of_not_isSquare

L30 ↗

ClassFieldTower.Sawin.minpoly_squareRoot_of_not_isSquare

Documentation

A square root of a nonsquare has the indicated minimal polynomial.

Source context 3 commands

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

open Polynomial
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem minpoly_squareRoot_of_not_isSquare
    (F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω]
    (a : F) (α : Ω) (hSquare : α ^ 2 = algebraMap F Ω a) (ha : ¬ IsSquare a) :
    minpoly F α = X ^ 2 - C a

theorem

finrank_adjoin_squareRoot

L43 ↗

ClassFieldTower.Sawin.finrank_adjoin_squareRoot

Documentation

Adjoining a square root of a nonsquare gives a field of degree two.

Source context 3 commands

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

open Polynomial
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem finrank_adjoin_squareRoot
    (F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω]
    (a : F) (α : Ω) (hSquare : α ^ 2 = algebraMap F Ω a) (ha : ¬ IsSquare a) :
    Module.finrank F (IntermediateField.adjoin F ({α} : Set Ω)) = 2

theorem

isQuadraticExtension_adjoin_squareRoot

L55 ↗

ClassFieldTower.Sawin.isQuadraticExtension_adjoin_squareRoot

Documentation

The actual simple intermediate field supplies the quadratic-extension class, and hence finite dimensionality, at later algebraic boundaries.

Source context 3 commands

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

open Polynomial
universe u v
namespace ClassFieldTower.Sawin

Lean source · full declaration

theorem isQuadraticExtension_adjoin_squareRoot
    (F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω]
    (a : F) (α : Ω) (hSquare : α ^ 2 = algebraMap F Ω a) (ha : ¬ IsSquare a) :
    Algebra.IsQuadraticExtension F (IntermediateField.adjoin F ({α} : Set Ω)) where
  finrank_eq_two' := finrank_adjoin_squareRoot F Ω a α hSquare ha

theorem

adjoinSquareRoot_gen_sq

L62 ↗

ClassFieldTower.Sawin.adjoinSquareRoot_gen_sq

Documentation

The canonical internal generator retains the square equation.

Source context 3 commands

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

open Polynomial
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem adjoinSquareRoot_gen_sq
    (F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω]
    (a : F) (α : Ω) (hSquare : α ^ 2 = algebraMap F Ω a) :
    IntermediateField.AdjoinSimple.gen F α ^ 2 =
      algebraMap F (IntermediateField.adjoin F ({α} : Set Ω)) a

theorem

adjoinSquareRoot_gen_adjoin

L73 ↗

ClassFieldTower.Sawin.adjoinSquareRoot_gen_adjoin

Documentation

The canonical internal generator generates the whole simple extension.

Source context 3 commands

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

open Polynomial
universe u v
namespace ClassFieldTower.Sawin

Lean source · statement

theorem adjoinSquareRoot_gen_adjoin
    (F : Type u) (Ω : Type v) [Field F] [Field Ω] [Algebra F Ω]
    (α : Ω) :
    IntermediateField.adjoin F ({IntermediateField.AdjoinSimple.gen F α} :
      Set (IntermediateField.adjoin F ({α} : Set Ω))) = ⊤

Module documentation

Adjoining a square root of a nonsquare

Declarations

minpoly_squareRoot_of_not_isSquare

finrank_adjoin_squareRoot

isQuadraticExtension_adjoin_squareRoot

adjoinSquareRoot_gen_sq

adjoinSquareRoot_gen_adjoin