ClassFieldTower.Sawin.sawinQuadraticCompositum_eq_adjoin_roots
The finite compositum is the intermediate field generated by the five chosen roots in the fixed algebraic closure.
Source context 1 command
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFieldTower.SawinLean source · full declaration
theorem sawinQuadraticCompositum_eq_adjoin_roots :
sawinQuadraticCompositum.toIntermediateField =
IntermediateField.adjoin ℚ
(Set.range (fun i : Fin 5 ↦ quadraticClosureRoot (sawinQuadraticRadicand i : ℚ))) := by
let M : IntermediateField ℚ (AlgebraicClosure ℚ) :=
IntermediateField.adjoin ℚ
(Set.range (fun i : Fin 5 ↦ quadraticClosureRoot (sawinQuadraticRadicand i : ℚ)))
change sawinQuadraticCompositum.toIntermediateField = M
apply le_antisymm
· have hLayer : ∀ i : Fin 5, (sawinQuadraticLayer i).toIntermediateField ≤ M := by
intro i
apply IntermediateField.adjoin_simple_le_iff.mpr
exact IntermediateField.subset_adjoin ℚ _ ⟨i, rfl⟩
exact Finset.sup_induction
(p := fun E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ) ↦
E.toIntermediateField ≤ M)
bot_le
(fun E hE F hF ↦
(show E.toIntermediateField ⊔ F.toIntermediateField ≤ M from sup_le hE hF))
(fun i _hi ↦ hLayer i)
· apply IntermediateField.adjoin_le_iff.mpr
rintro x ⟨i, rfl⟩
apply sawinQuadraticLayer_le_compositum i
exact IntermediateField.mem_adjoin_simple_self ℚ
(quadraticClosureRoot (sawinQuadraticRadicand i : ℚ))