The tagged fixed fields are cyclotomic

M / K is Galois with Gal(M/K) split by galEquivProd as Gal(L/K) × (ZMod m)ˣ, the second factor being the cyclotomic character on the m-th roots of unity. A tag is a pair (σ, τ) in that product. This file shows that when the tag satisfies orderOf σ ∣ orderOf τ, the field fixed by the cyclic subgroup the tag generates has M as an m-th cyclotomic extension.

Main results

• TauCeti.fixedField_zpowers_isCyclotomicExtension: for a tag (σ, τ) with orderOf σ ∣ orderOf τ, M / fixedField ⟪(σ, τ)⟫ is an m-th cyclotomic extension.
• TauCeti.card_algEquiv_fixedField_zpowers_eq_orderOf: M has orderOf τ automorphisms over that fixed field.

References

The result is due to the Birkbeck--Brasca Chebotarev development, CBirkbeck/chebotarev-density (Apache-2.0), at commit 55a89985d47a3befcf6069aca1da250ff088b5c7. There it is two private declarations in CebotarevDensity/Abelian.lean: compositum_isCyclotomic_over_fixedField, which assumes the meet is trivial, and zpowers_inf_fixingSubgroup_eq_bot_aux, which supplies that hypothesis. The source combines them at their call site rather than stating a single theorem. The hypothesis taken here is orderOf σ ∣ orderOf τ, where the source asks for Nat.card Gal(L/K) ∣ orderOf τ.

theorem TauCeti.fixedField_zpowers_isCyclotomicExtension (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K L] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(L/K)) (τ : (ZMod m)ˣ) (hστ : orderOf σ ∣ orderOf τ) : IsCyclotomicExtension {m} (↥(IntermediateField.fixedField (Subgroup.zpowers ((IsCyclotomicExtension.galEquivProd K L M m hcop hζ).symm (σ, τ))))) M

The tagged fixed field carries the cyclotomic extension. For a tag (σ, τ) in the splitting Gal(M/K) ≃ Gal(L/K) × (ZMod m)ˣ whose first component's order divides the second's, M is an m-th cyclotomic extension of the field fixed by the cyclic subgroup the tag generates.

The divisibility is what makes the tag's cyclic subgroup meet the fixer of K(μ_m) trivially, which is the hypothesis the general criterion needs.

theorem TauCeti.card_algEquiv_fixedField_zpowers_eq_orderOf (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [NumberField K] [Field L] [NumberField L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] [IsGalois K L] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(L/K)) (τ : (ZMod m)ˣ) (hστ : orderOf σ ∣ orderOf τ) : Nat.card Gal(M/↥(IntermediateField.fixedField (Subgroup.zpowers ((IsCyclotomicExtension.galEquivProd K L M m hcop hζ).symm (σ, τ))))) = orderOf τ

The automorphism group of M over the tagged fixed field has order orderOf τ. Under the same divisibility, the cyclic group cut out by the tag has order orderOf τ.

The count depends only on the tag's second component: the first contributes nothing once orderOf σ ∣ orderOf τ.