Module

CyclotomicAutToPowRestriction.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.CyclotomicAutToPowRestriction

2 declarations indexed from sourceView source ↗

Module documentation

Cyclotomic exponents under restriction

Restricting an automorphism along two field towers preserves its exponent on primitive roots. The primitive roots in the two fields may be chosen independently; neither bijectivity of restriction nor a compositum hypothesis is needed.

Imports2

Mathlib.FieldTheory.Galois.Basic
Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots

Imported by2

theorem

restrictRestrict_algebraMap

L25 ↗

ValuationTheory.DiscreteValuationField.restrictRestrict_algebraMap

Source context 2 commands

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

namespace 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]

Lean source · statement

theorem restrictRestrict_algebraMap (σ : E ≃ₐ[L] E) (x : K) :
    algebraMap K E (IntermediateField.restrictRestrictAlgEquivMapHom F K L E σ x) =
      σ (algebraMap K E x)

theorem

autToPow_restrictRestrictAlgEquivMapHom

L32 ↗

ValuationTheory.DiscreteValuationField.autToPow_restrictRestrictAlgEquivMapHom

Documentation

The actual restriction homomorphism preserves the cyclotomic exponent, independently of the primitive roots chosen in the two fields.