NYLL
Module

CyclotomicArithmeticStageRestriction.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.CyclotomicArithmeticStageRestriction
5 declarations indexed from sourceView source ↗

Module documentation

Restriction from the synchronized cyclotomic stage

The actual embedding of the original stage in the mapped compositum defines restriction of automorphisms. Its evaluation law is expressed in the same closure equivalence used to form the mapped field, supplying the finite part of the absolute-restriction comparison diagram.

Only the original-stage algebra and its matching F-tower are introduced locally; the cyclotomic tower is inherited from the mapped intermediate field, and no alternative algebra on that tower is installed.

Imports1
Imported by2

Declarations

instance

mappedCyclotomicOriginalAlgebra

L36 ↗
ClassFieldTower.Martinet.Shafarevich.mappedCyclotomicOriginalAlgebra
Source context 8 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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
Lean source · statement
instance mappedCyclotomicOriginalAlgebra
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    Algebra OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e)
instance

mappedCyclotomicOriginalTower

L41 ↗
ClassFieldTower.Martinet.Shafarevich.mappedCyclotomicOriginalTower
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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicOriginalAlgebra
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    Algebra OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e) :=
  (cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e).toAlgebra
Lean source · statement
instance mappedCyclotomicOriginalTower
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    IsScalarTower F OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e)
def

cyclotomicArithmeticStageMappedRestriction

L51 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedRestriction
Documentation

Actual restriction of automorphisms from the mapped cyclotomic stage to the original arithmetic stage.

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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicOriginalAlgebra
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    Algebra OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e) :=
  (cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e).toAlgebra
local instance mappedCyclotomicOriginalTower
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    IsScalarTower F OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e) :=
  IsScalarTower.of_algebraMap_eq' (by
    apply RingHom.ext
    intro x
    exact ((cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e).commutes x).symm)
Lean source · statement
def cyclotomicArithmeticStageMappedRestriction
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    Gal(cyclotomicArithmeticStageMappedField F p hpOdd U e / Cyclo) →* Gal(OriginalStage / F)
theorem

cyclotomicArithmeticStageMappedRestriction_commutes

L58 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedRestriction_commutes
Documentation

Restriction commutes with the actual original-stage embedding.

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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicOriginalAlgebra
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    Algebra OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e) :=
  (cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e).toAlgebra
local instance mappedCyclotomicOriginalTower
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    IsScalarTower F OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e) :=
  IsScalarTower.of_algebraMap_eq' (by
    apply RingHom.ext
    intro x
    exact ((cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e).commutes x).symm)
Lean source · statement
theorem cyclotomicArithmeticStageMappedRestriction_commutes
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F)
    (σ : Gal(cyclotomicArithmeticStageMappedField F p hpOdd U e/Cyclo))
    (x : OriginalStage) :
    cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e
        (cyclotomicArithmeticStageMappedRestriction F p hpOdd U e σ x) =
      σ (cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e x)
theorem

cyclotomicArithmeticStageMappedRestriction_apply

L69 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageMappedRestriction_apply
Documentation

Pointwise compatibility of finite restriction with the synchronized algebraic-closure equivalence.

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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local instance mappedCyclotomicOriginalAlgebra
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    Algebra OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e) :=
  (cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e).toAlgebra
local instance mappedCyclotomicOriginalTower
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F) :
    IsScalarTower F OriginalStage (cyclotomicArithmeticStageMappedField F p hpOdd U e) :=
  IsScalarTower.of_algebraMap_eq' (by
    apply RingHom.ext
    intro x
    exact ((cyclotomicArithmeticStageMappedOriginalAlgHom F p hpOdd U e).commutes x).symm)
Lean source · statement
theorem cyclotomicArithmeticStageMappedRestriction_apply
    (e : AlgebraicClosure Cyclo ≃ₐ[Cyclo] AlgebraicClosure F)
    (σ : Gal(cyclotomicArithmeticStageMappedField F p hpOdd U e/Cyclo))
    (x : OriginalStage) :
    e.symm (cyclotomicArithmeticStageMappedRestriction F p hpOdd U e σ x : AlgebraicClosure F) =
      (σ (cyclotomicArithmeticStageMappedOriginalAlgHom
        F p hpOdd U e x) : AlgebraicClosure Cyclo)

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