Root-of-unity orders in field extensions

The p-power root group of a field embeds in that of every extension, so its finite order divides the order in the extension. A field isomorphism preserves the order exactly. These facts compare the invariant localRootOfUnityOrder through towers of local fields.

theorem TauCeti.localRootOfUnityOrder_dvd_of_injective (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K →* L) (hf : Function.Injective ⇑f) (hK : Finite ↥(pPowerRootsOfUnity p K)) (hL : Finite ↥(pPowerRootsOfUnity p L)) : localRootOfUnityOrder p K hK ∣ localRootOfUnityOrder p L hL

An injective monoid map preserves the order of each root, so the finite root-group order of its source divides the order in its target.

theorem TauCeti.localRootOfUnityOrder_dvd_of_fieldHom (p : ℕ) {F : Type u_3} {E : Type u_4} [Field F] [Field E] (f : F →+* E) (hF : Finite ↥(pPowerRootsOfUnity p F)) (hE : Finite ↥(pPowerRootsOfUnity p E)) : localRootOfUnityOrder p F hF ∣ localRootOfUnityOrder p E hE

The p-power root order of a field divides that of every extension field.

theorem TauCeti.localRootOfUnityOrder_eq_of_mulEquiv (p : ℕ) {K : Type u_1} {L : Type u_2} [CommMonoid K] [CommMonoid L] (f : K ≃* L) (hK : Finite ↥(pPowerRootsOfUnity p K)) (hL : Finite ↥(pPowerRootsOfUnity p L)) : localRootOfUnityOrder p K hK = localRootOfUnityOrder p L hL

A multiplicative isomorphism preserves the order of the finite p-power root group.

theorem TauCeti.localRootOfUnityOrder_eq_of_ringEquiv (p : ℕ) {F : Type u_3} {E : Type u_4} [Field F] [Field E] (f : F ≃+* E) (hF : Finite ↥(pPowerRootsOfUnity p F)) (hE : Finite ↥(pPowerRootsOfUnity p E)) : localRootOfUnityOrder p F hF = localRootOfUnityOrder p E hE

A field isomorphism preserves the order of the finite p-power root group.