A chosen square root of a nonsquare rational number generates an actual finite Galois intermediate field of degree two. Its internal generator, square relation, and generation theorem let later arithmetic constructions supply reality and ramification conditions without assuming an extension.
A square root of a rational number in the fixed algebraic closure.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawindef quadraticClosureRoot (d : ℚ) : AlgebraicClosure ℚThe chosen element has the prescribed square.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem quadraticClosureRoot_sq (d : ℚ) :
quadraticClosureRoot d ^ 2 = algebraMap ℚ (AlgebraicClosure ℚ) dSurrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem quadraticClosureRoot_isIntegral (d : ℚ) :
IsIntegral ℚ (quadraticClosureRoot d)Nonsquareness identifies the minimal polynomial of the chosen root.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem minpoly_quadraticClosureRoot (d : ℚ) (hd : ¬ IsSquare d) :
minpoly ℚ (quadraticClosureRoot d) = X ^ 2 - C dSurrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem finrank_adjoin_quadraticClosureRoot (d : ℚ) (hd : ¬ IsSquare d) :
Module.finrank ℚ
(IntermediateField.adjoin ℚ ({quadraticClosureRoot d} : Set (AlgebraicClosure ℚ))) = 2The quadratic Galois subfield of the fixed algebraic closure obtained by adjoining a square root of a nonsquare rational number.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawindef quadraticClosure (d : ℚ) (hd : ¬ IsSquare d) :
FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ) where
toIntermediateField := IntermediateField.adjoin ℚ {quadraticClosureRoot d}
finiteDimensional := IntermediateField.adjoin.finiteDimensional
(quadraticClosureRoot_isIntegral d)
isGalois := by
let : Algebra.IsQuadraticExtension ℚ
(IntermediateField.adjoin ℚ ({quadraticClosureRoot d} : Set (AlgebraicClosure ℚ))) :=
{ finrank_eq_two' := finrank_adjoin_quadraticClosureRoot d hd }
exact Algebra.IsQuadraticExtension.isGalois ℚ
(IntermediateField.adjoin ℚ ({quadraticClosureRoot d} : Set (AlgebraicClosure ℚ)))The underlying intermediate field is the field generated by the chosen root.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem quadraticClosure_toIntermediateField (d : ℚ) (hd : ¬ IsSquare d) :
(quadraticClosure d hd).toIntermediateField =
IntermediateField.adjoin ℚ ({quadraticClosureRoot d} : Set (AlgebraicClosure ℚ))The constructed field has degree two over ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem quadraticClosure_finrank (d : ℚ) (hd : ¬ IsSquare d) :
Module.finrank ℚ (quadraticClosure d hd) = 2The constructed field is a quadratic extension, for use at arithmetic boundaries requiring Mathlib's quadratic-extension class.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem quadraticClosure_isQuadraticExtension (d : ℚ) (hd : ¬ IsSquare d) :
Algebra.IsQuadraticExtension ℚ (quadraticClosure d hd) where
finrank_eq_two' := quadraticClosure_finrank d hdThe chosen square root viewed inside its quadratic field.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawindef quadraticClosureGenerator (d : ℚ) (hd : ¬ IsSquare d) :
quadraticClosure d hdThe internal generator satisfies the same square equation.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem quadraticClosureGenerator_sq (d : ℚ) (hd : ¬ IsSquare d) :
quadraticClosureGenerator d hd ^ 2 = algebraMap ℚ (quadraticClosure d hd) dThe internal square root generates the whole constructed field.
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
namespace ClassFieldTower.Sawintheorem quadraticClosureGenerator_adjoin (d : ℚ) (hd : ¬ IsSquare d) :
IntermediateField.adjoin ℚ
({quadraticClosureGenerator d hd} : Set (quadraticClosure d hd)) = ⊤