Module

RealProTwoFrattiniField.lean

Nyll.SawinTotallyRealTowers.RealProTwoFrattiniField

1 declaration indexed from sourceView source ↗

Module documentation

The Frattini fixed field of the initial real pro-two group

The group-theoretic intersection over quadratic quotients and the arithmetic classification of all quadratic layers identify the actual Frattini fixed field. No finite-generation hypothesis is used.

Imports7

Nyll.SawinTotallyRealTowers.FixedFieldIntersection
Nyll.SawinTotallyRealTowers.ProTwoFrattini
Nyll.SawinTotallyRealTowers.RealProTwoQuadraticFixedFields
Nyll.SawinTotallyRealTowers.MaximalRealProPGroup
Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
Mathlib.Order.CompleteLattice.Basic
Mathlib.Topology.Algebra.OpenSubgroup

Imported by2

theorem

maximalRealProTwo_frattini_fixedField

L27 ↗

ClassFieldTower.Sawin.maximalRealProTwo_frattini_fixedField

Documentation

The Frattini fixed field, lifted to the fixed algebraic closure, is exactly the constructed five-generator multiquadratic field.

Source context 1 command

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

namespace ClassFieldTower.Sawin

Lean source · statement

theorem maximalRealProTwo_frattini_fixedField :
    IntermediateField.lift (IntermediateField.fixedField
      (ClassFieldTower.ProP.profiniteFrattini
        (maximalRealProPOutside 2 sawinRationalPrimeSupport ≃ₐ[ℚ]
          maximalRealProPOutside 2 sawinRationalPrimeSupport))) =
      sawinQuadraticCompositum.toIntermediateField

Module documentation

The Frattini fixed field of the initial real pro-two group

Declarations

maximalRealProTwo_frattini_fixedField