NYLL
Module

CyclotomicArithmeticStageMapped.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.CyclotomicArithmeticStageMapped
12 declarations indexed from sourceView source ↗

Module documentation

The cyclotomic stage in a synchronized algebraic closure

Mapping the actual compositum along a supplied algebraic-closure equivalence gives a finite everywhere-unramified p-extension in the cyclotomic base's standard algebraic closure. The equivalence is the concrete closure comparison used by absolute-Galois restriction; no new choice of closure comparison is made here.

The mapped field is named separately from its arithmetic bundle so that the coefficient and embedding interfaces do not unfold the bundle's finite-dimensionality and unramifiedness proofs during type synthesis.

Imports1
Imported by2

Declarations

instance

mappedCyclotomicBaseFinite

L38 ↗
ClassFieldTower.Martinet.Shafarevich.mappedCyclotomicBaseFinite
Source context 9 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
Lean source · statement
instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo
instance

mappedCyclotomicBaseNumber

L41 ↗
ClassFieldTower.Martinet.Shafarevich.mappedCyclotomicBaseNumber
Source context 10 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
Lean source · statement
instance mappedCyclotomicBaseNumber : NumberField Cyclo
instance

mappedCyclotomicSourceFinite

L44 ↗
ClassFieldTower.Martinet.Shafarevich.mappedCyclotomicSourceFinite
Source context 11 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
Lean source · statement
instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage
instance

mappedCyclotomicSourceNumber

L47 ↗
ClassFieldTower.Martinet.Shafarevich.mappedCyclotomicSourceNumber
Source context 12 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
Lean source · statement
instance mappedCyclotomicSourceNumber : NumberField TopStage
instance

mappedCyclotomicSourceGalois

L50 ↗
ClassFieldTower.Martinet.Shafarevich.mappedCyclotomicSourceGalois
Source context 13 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
Lean source · statement
instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage
def

cyclotomicArithmeticStageMappedField

L54 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedField
Documentation

The actual image of the compositum in the synchronized closure.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
local instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
def cyclotomicArithmeticStageMappedField
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    IntermediateField Cyclo (AlgebraicClosure Cyclo)
def

cyclotomicArithmeticStageMappedEquiv

L60 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedEquiv
Documentation

The compositum is equivalent to its actual image over the cyclotomic base.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
local instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
def cyclotomicArithmeticStageMappedEquiv
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    TopStage ≃ₐ[Cyclo] cyclotomicArithmeticStageMappedField F p hpOdd U e
def

cyclotomicArithmeticStageMappedExtension

L67 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedExtension
Documentation

All finite, Galois, p-group, and unramified certificates transported to the actual mapped field inside the standard algebraic closure.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
local instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
def cyclotomicArithmeticStageMappedExtension
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    FiniteEverywhereUnramifiedProPExtension Cyclo p
theorem

cyclotomicArithmeticStageMappedExtension_field

L83 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedExtension_field
Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
local instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
theorem cyclotomicArithmeticStageMappedExtension_field
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    (cyclotomicArithmeticStageMappedExtension F p hpOdd U e).field =
      cyclotomicArithmeticStageMappedField F p hpOdd U e
theorem

cyclotomicArithmeticStageMappedEquiv_apply

L88 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedEquiv_apply
Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
local instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
theorem cyclotomicArithmeticStageMappedEquiv_apply
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) (x : TopStage) :
    ((cyclotomicArithmeticStageMappedEquiv F p hpOdd U e x :
      cyclotomicArithmeticStageMappedField F p hpOdd U e) : AlgebraicClosure Cyclo) =
        e.symm x
def

cyclotomicArithmeticStageMappedOriginalAlgHom

L95 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedOriginalAlgHom
Documentation

The original arithmetic stage embeds into the mapped compositum.

Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
local instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
def cyclotomicArithmeticStageMappedOriginalAlgHom
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    OriginalStage →ₐ[F] cyclotomicArithmeticStageMappedField F p hpOdd U e
theorem

cyclotomicArithmeticStageMappedOriginalAlgHom_apply

L101 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedOriginalAlgHom_apply
Source context 14 commands

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

noncomputable section
namespace ClassFieldTower.Martinet.Shafarevich
open ClassFieldTower.Martinet ProCGroups
variable (F : Type) [Field F] [NumberField F]
variable (p : ℕ) [Fact p.Prime] (hpOdd : Odd p)
variable (U : OpenNormalSubgroup (MaxEverywhereUnramifiedProPGaloisGroup F p))
local notation "Cyclo" => IdealRadicalCyclotomicBase F p (Fact.out : p.Prime)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local notation "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance mappedCyclotomicBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance mappedCyclotomicSourceFinite : FiniteDimensional Cyclo TopStage :=
  cyclotomicArithmeticStage_finiteDimensional F p hpOdd U
local instance mappedCyclotomicSourceNumber : NumberField TopStage :=
  cyclotomicArithmeticStage_numberField F p hpOdd U
local instance mappedCyclotomicSourceGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
theorem cyclotomicArithmeticStageMappedOriginalAlgHom_apply
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) (x : OriginalStage) :
    ((cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e x :
      cyclotomicArithmeticStageMappedField F p hpOdd U e) : AlgebraicClosure Cyclo) =
        e.symm (x : AlgebraicClosure F)

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