Documentation

TauCeti.NumberTheory.NumberField.Cyclotomic.Compositum

The cyclotomic compositum M = L(μ_m) and its joint restriction isomorphism #

Let L / K be a Galois extension of number fields and let M = L(μ_m) be obtained from L by adjoining the m-th roots of unity. When m is coprime to the discriminant of L, the two restriction maps out of Gal(M/K) — to Gal(L/K), and to (ZMod m)ˣ via the cyclotomic character — are jointly bijective:

Gal(M/K) ≃* Gal(L/K) × (ZMod m)ˣ.

Main results #

The two general prerequisites this rests on are stated where they belong rather than here: the degree identity [M : K] = φ m is IsCyclotomicExtension.finrank_eq_totient in TauCeti.NumberTheory.NumberField.Cyclotomic.Finrank, and the compositum step K(ζ) ⊔ L = ⊤ is TauCeti.IntermediateField.adjoin_sup_fieldRange_eq_top in TauCeti.FieldTheory.IntermediateField.Adjoin.EqTop.

Implementation notes #

The file is split by hypothesis strength, in three steps. restrictNormalHom_prod_autToPow_injective comes first and assumes only [Normal K L]: normality is exactly what defines AlgEquiv.restrictNormalHom L, and the faithfulness argument never separates anything, so requiring IsGalois K L there would be an avoidable hypothesis. Next isGalois_of_isGalois_of_isCyclotomicExtension turns on [IsGalois K L], needing no hypothesis beyond the tower itself (algebraicity and separability of M / K are both derived inside the proof from IsGalois K L and the cyclotomic tower). Both are pure field theory and carry no NumberField instances. Only the results downstream of the degree count, which mention discr L, take number fields.

isGalois_of_isGalois_of_isCyclotomicExtension is a theorem and not an instance because neither L nor m can be recovered from the goal IsGalois K M, so there is no synthesization order for it; call sites introduce it with have.

That M / K is Galois is derived, not assumed: M is the compositum of L with K(ζ), both of which are normal over K, and the engine for a compositum of two normal extensions is Mathlib's IntermediateField.normal_sup. So Gal(M/K) below rests on no hypothesis beyond IsGalois K L and the cyclotomic tower. Separability comes from transitivity along the same tower: L / K is separable because it is Galois, and M / L because a cyclotomic extension is (IsCyclotomicExtension.isSeparable). No characteristic assumption is needed, since a primitive m-th root of unity exists in M only if the characteristic does not divide m.

Faithfulness of the joint restriction is not re-derived here: it is Mathlib's compositum engine IntermediateField.fixingSubgroup_sup (with fixingSubgroup_top), applied to K(ζ) and the image of L inside M. We invoke that shared lemma rather than IntermediateField.restrictRestrictAlgEquivMapHom_injective, which is built from it, because the latter concerns Gal(M/L) →* Gal(K(ζ)/K) whereas the map here is defined on Gal(M/K); using it would first require transporting an element of Gal(M/K) that fixes L into Gal(M/L), which is strictly more work than calling the underlying lemma directly.

Surjectivity does go through a degree count. That is not an oversight: surjectivity onto the (ZMod m)ˣ factor is the assertion that the m-th cyclotomic polynomial stays irreducible over L, which is exactly what the coprimality hypothesis hcop buys. Mathlib's companion restrictRestrictAlgEquivMapHom_surjective needs K(ζ) ⊓ L = ⊥, and the proof of that intersection statement is the same discriminant input, so it would not avoid the arithmetic.

Adapted from the Birkbeck–Brasca Chebotarev density project.

source
theorem IsPrimitiveRoot.autToPow_bijective (L : Type u_1) [Field L] [NumberField L] {M : Type u_2} [Field M] [Algebra L M] {m : ℕ} [NeZero m] [IsCyclotomicExtension {m} L M] {ζ : M} (hζ : IsPrimitiveRoot ζ m) (hcop : (NumberField.discr L).natAbs.Coprime m) :
Function.Bijective ⇑(autToPow L hζ)

The cyclotomic character of the top layer is bijective. For M = L(μ_m) with m coprime to discr L, the character Gal(M/L) → (ZMod m)ˣ is a bijection, so the top layer of the tower realises every prescribed action on the m-th roots of unity.

Stated in IsPrimitiveRoot beside Mathlib's IsPrimitiveRoot.autToPow_injective, and with the same binder shape, so that hζ.autToPow_bijective L reads like its injective counterpart.

Faithfulness of the joint restriction needs only that L / K is normal — enough to define AlgEquiv.restrictNormalHom L — not that it is Galois. Separability of L / K enters only with the compositum-Galois and degree-count results below.

source
theorem IsCyclotomicExtension.restrictNormalHom_prod_autToPow_injective (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [Normal K L] {ζ : M} (hζ : IsPrimitiveRoot ζ m) :
Function.Injective ⇑((AlgEquiv.restrictNormalHom L).prod (IsPrimitiveRoot.autToPow K hζ))

The joint restriction is faithful. An automorphism of M = L(μ_m) over K that is trivial on L and trivial on the m-th roots of unity is the identity. No arithmetic hypothesis is needed, only normality of L / K.

source
theorem IsCyclotomicExtension.isGalois_of_isGalois_of_isCyclotomicExtension (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [IsGalois K L] :
IsGalois K M

The cyclotomic compositum of a Galois extension is Galois. If L / K is Galois and M = L(μ_m), then M / K is Galois, so Gal(M/K) is available without a further hypothesis.

Both tower hypotheses are needed, which is what the name records: the cyclotomic extension is M / L, and L / K is Galois. Mathlib's IsCyclotomicExtension.isGalois is the one-step statement, for a cyclotomic extension of the base itself. Call sites introduce this with have; see the module Implementation notes.

The remaining results are arithmetic: they need the discriminant of L, hence number fields rather than bare characteristic-zero fields. Only the base fields K and L carry NumberField; M does not, because a cyclotomic extension of a number field is finite over it and so is a number field already — the instances it needs are installed locally where used.

source
noncomputable def IsCyclotomicExtension.galEquivProd (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [IsGalois K L] [NumberField K] [NumberField L] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) :
Gal(M/K) ≃* Gal(L/K) × (ZMod m)ˣ

The joint restriction Gal(M/K) ≃* Gal(L/K) × (ZMod m)ˣ, packaged as a MulEquiv.

Instances For
    source
    @[simp]
    theorem IsCyclotomicExtension.galEquivProd_apply (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [IsGalois K L] [NumberField K] [NumberField L] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (σ : Gal(M/K)) :
    (galEquivProd K L M m hcop hζ) σ = (σ.restrictNormal L, (IsPrimitiveRoot.autToPow K hζ) σ)

    Both components of galEquivProd: it sends σ to its restriction to L paired with its cyclotomic character. Consumers should compute with this rather than unfolding the MulEquiv.ofBijective that packages it.

    source
    @[simp]
    theorem IsCyclotomicExtension.restrictNormal_galEquivProd_symm (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [IsGalois K L] [NumberField K] [NumberField L] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (x : Gal(L/K) × (ZMod m)ˣ) :
    ((galEquivProd K L M m hcop hζ).symm x).restrictNormal L = x.1

    Elimination for the inverse of galEquivProd, first component: the automorphism it produces restricts on L to the prescribed element of Gal(L/K). Together with autToPow_galEquivProd_symm this characterises (galEquivProd ...).symm, so consumers never need the MulEquiv.ofBijective that packages it.

    source
    @[simp]
    theorem IsCyclotomicExtension.autToPow_galEquivProd_symm (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [IsGalois K L] [NumberField K] [NumberField L] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) (x : Gal(L/K) × (ZMod m)ˣ) :
    (IsPrimitiveRoot.autToPow K hζ) ((galEquivProd K L M m hcop hζ).symm x) = x.2

    Elimination for the inverse of galEquivProd, second component: the automorphism it produces has the prescribed cyclotomic character.

    source
    theorem IsCyclotomicExtension.ker_autToPow_eq_comap_galEquivProd (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [IsGalois K L] [NumberField K] [NumberField L] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) :
    (IsPrimitiveRoot.autToPow K hζ).ker = Subgroup.comap (galEquivProd K L M m hcop hζ).toMonoidHom (⊤.prod ⊥)

    The cyclotomic character's kernel is the first factor of the joint restriction. The automorphisms of M acting trivially on the m-th roots of unity are exactly those that galEquivProd sends into Gal(L/K) × 1; equivalently, the kernel of the cyclotomic character is the part of Gal(M/K) that the equivalence reads off as pure Gal(L/K).

    This is the subgroup-level companion to galEquivProd_apply: that lemma computes the equivalence on elements, this one transports a distinguished subgroup across it.

    Source: the identification of Gal(M/K(μ_m)) with the Gal(L/K) × 1 factor is credited to CBirkbeck/chebotarev-density (Apache-2.0, Birkbeck--Brasca) at commit 55a89985d47a3befcf6069aca1da250ff088b5c7, which states it in the docstring of the private autToPow_eq_one_of_fixes (CebotarevDensity/Abelian.lean:659) and performs the step inline; isolating it as a lemma over galEquivProd is not the source's.

    source
    theorem IsCyclotomicExtension.ker_restrictNormalHom_eq_comap_galEquivProd (K : Type u_1) (L : Type u_2) (M : Type u_3) [Field K] [Field L] [Field M] [Algebra K L] [Algebra K M] [Algebra L M] [IsScalarTower K L M] (m : ℕ) [NeZero m] [IsCyclotomicExtension {m} L M] [IsGalois K L] [NumberField K] [NumberField L] (hcop : (NumberField.discr L).natAbs.Coprime m) {ζ : M} (hζ : IsPrimitiveRoot ζ m) :
    (AlgEquiv.restrictNormalHom L).ker = Subgroup.comap (galEquivProd K L M m hcop hζ).toMonoidHom (⊥.prod ⊤)

    The restriction's kernel is the second factor of the joint restriction. The automorphisms of M acting trivially on L are exactly those that galEquivProd sends into 1 × (ZMod m)ˣ.

    This is the mirror of ker_autToPow_eq_comap_galEquivProd: between them the two components of the equivalence are each characterised on subgroups, so a consumer holding either Gal(M/L) or Gal(M/K(μ_m)) can transport it without unfolding galEquivProd.

    Source: as for ker_autToPow_eq_comap_galEquivProd.