ModuleOpenNormalArithmeticStage.lean
Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.OpenNormalArithmeticStage
6 declarations indexed from sourceView source ↗ Module documentation
Arithmetic fields attached to open normal quotients
An open normal quotient of the maximal everywhere-unramified pro-p Galois group is realized by the Galois group of a concrete finite everywhere-unramified p-extension. This is the finite-stage arithmetic bridge used before introducing any cohomological local--global map.
Declarations
ClassFieldTower.Martinet.Shafarevich.openNormalClosedSubgroup
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open ProCGroups
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
ClassFieldTower.Martinet.Shafarevich.openNormalFixedFieldInMaximal
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open ProCGroups
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
ClassFieldTower.Martinet.Shafarevich.openNormalFixedField
DocumentationThe fixed field of an open normal subgroup, transported from the maximal compositum into the chosen algebraic closure.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open ProCGroups
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage
DocumentationFor odd p, the fixed field of an open normal subgroup is a bundled finite Galois everywhere-unramified p-extension.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open ProCGroups
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
ClassFieldTower.Martinet.Shafarevich.openNormalArithmeticStage_field
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open ProCGroups
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]
ClassFieldTower.Martinet.Shafarevich.openNormalQuotientEquivArithmeticStageGalois
DocumentationThe quotient by an open normal subgroup is the Galois group of its concrete finite everywhere-unramified arithmetic stage.
Source context 8 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
universe u
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet
open ProCGroups
variable (F : Type u) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime]