Theorems · Theorem · number theory

IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply

∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] {m : ℕ} [inst_3 : NeZero m] (F : Type u_2) [inst_4 : Field F]
  [inst_5 : NumberField F] [hF : IsCyclotomicExtension {m} ℚ F] [inst_6 : Algebra F K] [inst_7 : IsGalois ℚ F]
  (h : m ∣ n) (σ : Gal(K/ℚ)),
  (IsCyclotomicExtension.Rat.galEquivZMod m F) (σ.restrictNormal F) =
    (ZMod.unitsMap h) ((IsCyclotomicExtension.Rat.galEquivZMod n K) σ)

Let m ∣ n. Then, the following diagram commutes: Gal(ℚ(ζₙ)/ℚ) → (ℤ/nℤ)ˣ ↓ ↓ Gal(ℚ(ζₘ)/ℚ) → (ℤ/mℤ)ˣ where the horizontal maps are galEquivZMod, the left map is the restriction map and the right map is the natural map.

Defined in

Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Cited by

1 results in Mathlib

Foundations

Depth 218 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NeZeroFieldNumberFieldIsCyclotomicExtensionNeZeroFieldNumberFieldIsCyclotomicExtensionAlgebraIsGalois