Module

CyclotomicTeichmullerRestriction.lean

Nyll.ValuedFieldTheory.LocalField.Padic.CyclotomicTeichmullerRestriction

2 declarations indexed from sourceView source ↗

Module documentation

Restriction compatibility of finite cyclotomic Teichmüller characters

The two characters on a cyclotomic extension and its base change agree along the actual restriction homomorphism. Normality of the lower cyclotomic extension supplies the restriction; no bijectivity or compatibility of chosen primitive roots is assumed.

Imports2

Imported by2

theorem

primeCyclotomicTeichmullerCharacter_restrictRestrictAlgEquivMapHom

L31 ↗

LocalFieldTheory.DiscreteValuationField.primeCyclotomicTeichmullerCharacter_restrictRestrictAlgEquivMapHom

Documentation

The finite cyclotomic Teichmüller character agrees with the lower character evaluated on the actual restricted automorphism.

Source context 3 commands

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

namespace LocalFieldTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField
variable (F K L E : Type*) [Field F] [Field K] [Field L] [Field E]
  [Algebra F K] [Algebra F L] [Algebra F E] [Algebra K E] [Algebra L E]
  [IsScalarTower F K E] [IsScalarTower F L E] [Normal F K]
  (p : ℕ) [Fact p.Prime]
  [IsCyclotomicExtension {p} F K] [IsCyclotomicExtension {p} L E]

Lean source · statement

theorem primeCyclotomicTeichmullerCharacter_restrictRestrictAlgEquivMapHom
    (σ : E ≃ₐ[L] E) :
    primeCyclotomicTeichmullerCharacter F K p
      (IntermediateField.restrictRestrictAlgEquivMapHom F K L E σ) =
      primeCyclotomicTeichmullerCharacter L E p σ

theorem

primeCyclotomicTeichmullerCharacter_comp_restrictRestrictAlgEquivMapHom

L44 ↗

LocalFieldTheory.DiscreteValuationField.primeCyclotomicTeichmullerCharacter_comp_restrictRestrictAlgEquivMapHom