ModuleRealProPFrobeniusFixedField.lean
Nyll.SawinTotallyRealTowers.RealProPFrobeniusFixedField
6 declarations indexed from sourceView source ↗ Module documentation
The actual fixed field of a Frobenius cut
Take the fixed field of the constructed closed normal subgroup inside the maximal real extension, then lift it into the same algebraic closure of ℚ. Its Galois group is the actual quotient from S3.
Declarations
ClassFieldTower.Sawin.fixedFieldMaximalIsGalois
Source context 7 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))
ClassFieldTower.Sawin.realProPFrobeniusFixedField
DocumentationThe Frobenius-cut fixed field in the original algebraic closure.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))
private local instance fixedFieldMaximalIsGalois :
IsGalois ℚ (maximalRealProPOutside p T) :=
maximalRealProPOutside_isGalois p T
ClassFieldTower.Sawin.realProPFrobeniusFixedField_le
DocumentationThe constructed cut field is contained in its actual maximal parent.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))
private local instance fixedFieldMaximalIsGalois :
IsGalois ℚ (maximalRealProPOutside p T) :=
maximalRealProPOutside_isGalois p T
ClassFieldTower.Sawin.realProPFrobeniusFixedField_isGalois
DocumentationNormality of the actual cut kernel makes its fixed field Galois over ℚ.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))
private local instance fixedFieldMaximalIsGalois :
IsGalois ℚ (maximalRealProPOutside p T) :=
maximalRealProPOutside_isGalois p T
ClassFieldTower.Sawin.realProPFrobeniusFixedField_isTotallyReal
DocumentationTotal reality descends to the internal fixed field and is preserved by its lift.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))
private local instance fixedFieldMaximalIsGalois :
IsGalois ℚ (maximalRealProPOutside p T) :=
maximalRealProPOutside_isGalois p T
ClassFieldTower.Sawin.realProPFrobeniusCutEquivFixedField
DocumentationThe actual S3 quotient is the full Galois group of the constructed cut field.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTower.Sawin
open ProCGroups.Presentations
variable (p : ℕ) (T : Set (HeightOneSpectrum (𝓞 ℚ)))
variable (v : ℕ → HeightOneSpectrum (𝓞 ℚ))
private local instance fixedFieldMaximalIsGalois :
IsGalois ℚ (maximalRealProPOutside p T) :=
maximalRealProPOutside_isGalois p T