NYLL
Module

CyclotomicArithmeticStage.lean

Nyll.SawinTotallyRealTowers.UnramifiedProPRelationRank.RelationRank.CyclotomicArithmeticStage
14 declarations indexed from sourceView source ↗

Module documentation

The actual cyclotomic base change of an unramified arithmetic stage

Inside the fixed algebraic closure of F, let C = F(μ_p) and let L be the open-normal arithmetic stage. The field below is the actual compositum C L, regarded as an intermediate field over C. Its two generator ranges are proved to generate the top. Restriction therefore gives its p-group Galois group and, by actual ideal-inertia restriction, finite-place unramifiedness. Odd p supplies the infinite-place condition. No unramifiedness of C/F is needed.

All instance choices are local and named. There is one new algebra structure, the inclusion L → C L, and one matching original-base tower; the C → C L tower is the canonical intermediate-field tower.

Imports3
Imported by2

Declarations

def

cyclotomicArithmeticStageField

L42 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageField
Documentation

The actual cyclotomic compositum C L inside the original algebraic closure.

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
def cyclotomicArithmeticStageField : IntermediateField Cyclo (AlgebraicClosure F)
instance

cyclotomicStageBaseFinite

L47 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicStageBaseFinite
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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
Lean source · statement
instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo
instance

cyclotomicStageBaseNumber

L50 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicStageBaseNumber
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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
Lean source · statement
instance cyclotomicStageBaseNumber : NumberField Cyclo
instance

cyclotomicStageFiniteOverOriginalBase

L53 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicStageFiniteOverOriginalBase
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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
Lean source · statement
instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage
theorem

cyclotomicArithmeticStage_numberField

L58 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStage_numberField
Documentation

The compositum is a number field, with the original-base tower fixed.

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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
Lean source · statement
theorem cyclotomicArithmeticStage_numberField : NumberField TopStage
theorem

cyclotomicArithmeticStage_finiteDimensional

L64 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStage_finiteDimensional
Documentation

The actual compositum is finite dimensional over the cyclotomic base.

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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
Lean source · statement
theorem cyclotomicArithmeticStage_finiteDimensional : FiniteDimensional Cyclo TopStage
def

cyclotomicArithmeticStageOriginalAlgHom

L70 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStageOriginalAlgHom
Documentation

The original stage embeds into the actual cyclotomic 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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
Lean source · statement
def cyclotomicArithmeticStageOriginalAlgHom : OriginalStage →ₐ[F] TopStage
instance

cyclotomicStageOriginalAlgebra

L73 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicStageOriginalAlgebra
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 "OriginalStage" => FiniteEverywhereUnramifiedProPExtension.field
  (openNormalArithmeticStage F p hpOdd U)
local notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
Lean source · statement
instance cyclotomicStageOriginalAlgebra : Algebra OriginalStage TopStage
instance

cyclotomicStageOriginalTower

L76 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicStageOriginalTower
Source context 15 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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
local instance cyclotomicStageOriginalAlgebra : Algebra OriginalStage TopStage :=
  (cyclotomicArithmeticStageOriginalAlgHom F p hpOdd U).toAlgebra
Lean source · statement
instance cyclotomicStageOriginalTower : IsScalarTower F OriginalStage TopStage
theorem

cyclotomicArithmeticStage_generatorRanges

L80 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStage_generatorRanges
Documentation

The original stage and the cyclotomic base generate the actual compositum.

Source context 16 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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
local instance cyclotomicStageOriginalAlgebra : Algebra OriginalStage TopStage :=
  (cyclotomicArithmeticStageOriginalAlgHom F p hpOdd U).toAlgebra
local instance cyclotomicStageOriginalTower : IsScalarTower F OriginalStage TopStage :=
  IsScalarTower.of_algebraMap_eq' (by ext; rfl)
Lean source · statement
theorem cyclotomicArithmeticStage_generatorRanges :
    (IsScalarTower.toAlgHom F OriginalStage TopStage).fieldRange ⊔
      (IsScalarTower.toAlgHom F Cyclo TopStage).fieldRange = ⊤
theorem

cyclotomicArithmeticStage_isGalois

L91 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStage_isGalois
Documentation

Galoisness survives the actual cyclotomic base change.

Source context 16 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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
local instance cyclotomicStageOriginalAlgebra : Algebra OriginalStage TopStage :=
  (cyclotomicArithmeticStageOriginalAlgHom F p hpOdd U).toAlgebra
local instance cyclotomicStageOriginalTower : IsScalarTower F OriginalStage TopStage :=
  IsScalarTower.of_algebraMap_eq' (by ext; rfl)
Lean source · statement
theorem cyclotomicArithmeticStage_isGalois : IsGalois Cyclo TopStage
instance

cyclotomicStageGalois

L104 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicStageGalois
Source context 16 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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
local instance cyclotomicStageOriginalAlgebra : Algebra OriginalStage TopStage :=
  (cyclotomicArithmeticStageOriginalAlgHom F p hpOdd U).toAlgebra
local instance cyclotomicStageOriginalTower : IsScalarTower F OriginalStage TopStage :=
  IsScalarTower.of_algebraMap_eq' (by ext; rfl)
Lean source · statement
instance cyclotomicStageGalois : IsGalois Cyclo TopStage
theorem

cyclotomicArithmeticStage_isPGroup

L108 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStage_isPGroup
Documentation

The actual base-changed Galois group embeds into the original p-group.

Source context 17 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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
local instance cyclotomicStageOriginalAlgebra : Algebra OriginalStage TopStage :=
  (cyclotomicArithmeticStageOriginalAlgHom F p hpOdd U).toAlgebra
local instance cyclotomicStageOriginalTower : IsScalarTower F OriginalStage TopStage :=
  IsScalarTower.of_algebraMap_eq' (by ext; rfl)
local instance cyclotomicStageGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
theorem cyclotomicArithmeticStage_isPGroup : IsPGroup p Gal(TopStage / Cyclo)
theorem

cyclotomicArithmeticStage_everywhereUnramified

L115 ↗
ClassFieldTower.Martinet.Shafarevich.cyclotomicArithmeticStage_everywhereUnramified
Documentation

The cyclotomic base change is unramified at every finite and infinite place, without any unramifiedness assumption on the cyclotomic extension itself.

Source context 17 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 notation "TopStage" => cyclotomicArithmeticStageField F p hpOdd U
local instance cyclotomicStageBaseFinite : FiniteDimensional F Cyclo :=
  finiteDimensional_idealRadicalCyclotomicBase F p Fact.out
local instance cyclotomicStageBaseNumber : NumberField Cyclo :=
  NumberField.of_module_finite F Cyclo
local instance cyclotomicStageFiniteOverOriginalBase : FiniteDimensional F TopStage := by
  change FiniteDimensional F ↥(Cyclo ⊔ OriginalStage)
  exact IntermediateField.finiteDimensional_sup Cyclo OriginalStage
attribute [local instance] cyclotomicArithmeticStage_numberField
attribute [local instance] cyclotomicArithmeticStage_finiteDimensional
local instance cyclotomicStageOriginalAlgebra : Algebra OriginalStage TopStage :=
  (cyclotomicArithmeticStageOriginalAlgHom F p hpOdd U).toAlgebra
local instance cyclotomicStageOriginalTower : IsScalarTower F OriginalStage TopStage :=
  IsScalarTower.of_algebraMap_eq' (by ext; rfl)
local instance cyclotomicStageGalois : IsGalois Cyclo TopStage :=
  cyclotomicArithmeticStage_isGalois F p hpOdd U
Lean source · statement
theorem cyclotomicArithmeticStage_everywhereUnramified : IsEverywhereUnramified Cyclo TopStage

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