NYLL
Module

RealProTwoQuadraticFixedFields.lean

Nyll.SawinTotallyRealTowers.RealProTwoQuadraticFixedFields
2 declarations indexed from sourceView source ↗

Module documentation

Index-two fixed fields of the real pro-two extension

Finite Galois layers inside the maximal real extension correspond to open normal subgroups. Restricting and then lifting recovers the original ambient field. The index-degree equality identifies its quadratic layers, whose compositum has already been determined arithmetically.

Imports8
Imported by2

Declarations

theorem

exists_indexTwo_fixedField_of_quadratic_le

L27 ↗
ClassFieldTower.Sawin.exists_indexTwo_fixedField_of_quadratic_le
Source context 1 command

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

namespace ClassFieldTower.Sawin
Lean source · statement
theorem exists_indexTwo_fixedField_of_quadratic_le
    (M : IntermediateField ℚ (AlgebraicClosure ℚ)) [IsGalois ℚ M]
    (E : FiniteGaloisIntermediateField ℚ (AlgebraicClosure ℚ))
    (hDegree : Module.finrank ℚ E = 2) (hEM : E.toIntermediateField ≤ M) :
    ∃ U : OpenNormalSubgroup (M ≃ₐ[ℚ] M),
      (U : Subgroup (M ≃ₐ[ℚ] M)).index = 2 ∧
        IntermediateField.lift (IntermediateField.fixedField (U : Subgroup (M ≃ₐ[ℚ] M))) =
          E.toIntermediateField
theorem

sawinQuadraticCompositum_eq_iSup_indexTwo_fixedFields

L53 ↗
ClassFieldTower.Sawin.sawinQuadraticCompositum_eq_iSup_indexTwo_fixedFields
Documentation

The ambient compositum of index-two open-normal fixed fields is exactly the concrete compositum of the five admissible quadratic extensions.

Source context 1 command

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

namespace ClassFieldTower.Sawin
Lean source · statement
theorem sawinQuadraticCompositum_eq_iSup_indexTwo_fixedFields :
    sawinQuadraticCompositum.toIntermediateField =
      ⨆ (U : OpenNormalSubgroup
          (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
            maximalRealProPOutside 2 sawinRationalPrimeSupport))
        (_ : (U : Subgroup
          (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
            maximalRealProPOutside 2 sawinRationalPrimeSupport)).index = 2),
        IntermediateField.lift (IntermediateField.fixedField
          (U : Subgroup
            (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
              maximalRealProPOutside 2 sawinRationalPrimeSupport)))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.