Module

CyclotomicCompositumCommutation.lean

Nyll.ValuedFieldTheory.Valuation.DiscreteValuationField.CyclotomicCompositumCommutation

1 declaration indexed from sourceView source ↗

Module documentation

Commuting automorphisms in a cyclotomic compositum

An automorphism fixing the lower cyclotomic field commutes with an automorphism fixing the other normal field. A primitive root in the lower field generates the upper cyclotomic extension, so their commutation on the two fields determines their commutation everywhere.

Imports3

Mathlib.Algebra.Algebra.Subalgebra.Lattice
Mathlib.FieldTheory.Normal.Defs
Mathlib.NumberTheory.Cyclotomic.Basic

Imported by2

theorem

cyclotomic_compositum_aut_commute

L28 ↗

ValuationTheory.DiscreteValuationField.cyclotomic_compositum_aut_commute

Documentation

The two relative automorphism groups commute in the actual cyclotomic compositum; its generation is supplied by a primitive root in L.

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 cyclotomic_compositum_aut_commute
    (n : ℕ) [NeZero n]
    [IsCyclotomicExtension {n} F L] [IsCyclotomicExtension {n} K E]
    (τ : E ≃ₐ[L] E) (δ : E ≃ₐ[K] E) :
    Commute τ.toRingEquiv δ.toRingEquiv

Module documentation

Commuting automorphisms in a cyclotomic compositum

Declarations

cyclotomic_compositum_aut_commute