Torsion of the tame-frame module

Let G be a finite group generated by σ, τ, let a, b be scalars of a commutative ring R, and let J = R[G]·(σ - a) + R[G]·(τ - b) be the left ideal of the two eigenvalue relations. This file computes the p-power torsion of the tame-frame module

M₀ = R[G]² / R[G]·(σ - a, τ - b)

when the relation map x ↦ x · (σ - a, τ - b) is injective, multiplication by p is injective on R, and the scalars in J are exactly the multiples of p ^ k: the torsion is R[G] ⧸ J, as a left R[G]-module.

Modulo J every group element g is a scalar c(g), and c is multiplicative modulo p ^ k. The twisted norm x = ∑_g c(g) g⁻¹ then satisfies x (σ - a) ≡ 0 and x (τ - b) ≡ 0 modulo p ^ k, so x · (σ - a, τ - b) = p ^ k y₀ for some y₀ ∈ R[G]². The class t₀ of y₀ is killed by p ^ k, its annihilator is exactly J, and every p-power torsion element of M₀ is a scalar multiple of t₀. The last point rests on the fact that, since σ, τ generate G, a w with w (σ - a) and w (τ - b) divisible by p ^ n has w J divisible by p ^ n.

For R = ℤ_p and natural-number exponents, finiteness of ℤ_p[G] ⧸ J is enough: the scalars in J then form a nonzero ideal of ℤ_p, a power of (p). With the sharp exponents of a tame frame on a layer L/K (TauCeti.exists_tameFrame_exponents), ℤ_p[G] ⧸ J is the p-power torsion of the p-adic completion A(L) of Lˣ, that is μ_{p^∞}(L) with its Galois action. So the tame-frame module has the same p-power torsion as A(L), the arithmetic input of the comparison of the Tate module of the layer with M₀ ⊕ ℤ_p[G]^N in the proof of NSW (7.4.1).

Main results

• TauCeti.nonempty_tameFrameModule_torsion_linearEquiv_of_relationMap_injective: the p-power torsion of M₀ is R[G] ⧸ J, for an injective relation map and an ideal J whose scalars are the multiples of p ^ k.
• TauCeti.nonempty_tameFrameModule_torsion_linearEquiv: the same over ℤ_p, when ℤ_p[G] ⧸ J is finite.
• TauCeti.tameFrameModule_torsion_linearEquiv: for supplied sharp exponents of a tame frame, the p-power torsion of M₀ is that of A(L).
• TauCeti.exists_tameFrameModule_torsion_linearEquiv: for a tame frame of L/K, there are sharp exponents for which the p-power torsion of M₀ is that of A(L).

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, proof of (7.4.1).

theorem TauCeti.nonempty_tameFrameModule_torsion_linearEquiv_of_relationMap_injective {R : Type u} [CommRing R] {G : Type v} [Group G] {σ τ : G} {a b : R} [Finite G] {p k : ℕ} (hgen : Subgroup.closure {σ, τ} = ⊤) (hp : IsSMulRegular R p) (hinj : Function.Injective ⇑(tameFrameRelationMap R G σ τ a b)) (hJ : Ideal.comap (algebraMap R (MonoidAlgebra R G)) (Ideal.span {MonoidAlgebra.single σ 1 - MonoidAlgebra.single 1 a, MonoidAlgebra.single τ 1 - MonoidAlgebra.single 1 b}) = Ideal.span {↑p ^ k}) : Nonempty (↥(pPowerTorsion p (MonoidAlgebra R G) (TameFrameModule R G σ τ a b)) ≃ₗ[MonoidAlgebra R G] MonoidAlgebra R G ⧸ Ideal.span {MonoidAlgebra.single σ 1 - MonoidAlgebra.single 1 a, MonoidAlgebra.single τ 1 - MonoidAlgebra.single 1 b})

The torsion of the tame-frame module. Let G be a finite group generated by σ, τ, and let R be a commutative ring on which multiplication by p is injective, such as ℤ_p. Suppose that the tame-frame relation x ↦ x · (σ - a, τ - b) is injective and that the scalars in the left ideal J = (σ - a, τ - b) of R[G] are exactly the multiples of p ^ k. Then the p-power torsion of the tame-frame module M₀ = R[G]² / R[G]·(σ - a, τ - b) is isomorphic to R[G] ⧸ J as a left R[G]-module.

theorem TauCeti.nonempty_tameFrameModule_torsion_linearEquiv {G : Type v} [Group G] {p : ℕ} [Fact (Nat.Prime p)] [Finite G] {σ τ : G} (hgen : Subgroup.closure {σ, τ} = ⊤) (a b : ℕ) (hcard : Nat.card (MonoidAlgebra ℤ_[p] G ⧸ Ideal.span {MonoidAlgebra.single σ 1 - ↑a, MonoidAlgebra.single τ 1 - ↑b}) ≠ 0) : Nonempty (↥(pPowerTorsion p (MonoidAlgebra ℤ_[p] G) (TameFrameModule ℤ_[p] G σ τ ↑a ↑b)) ≃ₗ[MonoidAlgebra ℤ_[p] G] MonoidAlgebra ℤ_[p] G ⧸ Ideal.span {MonoidAlgebra.single σ 1 - ↑a, MonoidAlgebra.single τ 1 - ↑b})

The torsion of the tame-frame module with sharp exponents. Let G be a finite group generated by σ, τ, and let a, b be natural numbers for which the quotient ℤ_p[G] ⧸ J by the left ideal J = (σ - a, τ - b) is finite, as the sharp exponents of a tame frame provide. Then the p-power torsion of the tame-frame module M₀ = ℤ_p[G]² / ℤ_p[G]·(σ - a, τ - b) is isomorphic to ℤ_p[G] ⧸ J as a left ℤ_p[G]-module.

theorem TauCeti.tameFrameModule_torsion_linearEquiv {p : ℕ} [Fact (Nat.Prime p)] {L : Type u_1} [Field L] {K : Type u_2} [Field K] [Algebra K L] [Finite Gal(L/K)] (h : Finite ↥(pPowerRootsOfUnity p L)) (σ τ : Gal(L/K)) (hgen : Subgroup.closure {σ, τ} = ⊤) (a b : ℕ) (ha : ∀ ζ ∈ pPowerRootsOfUnity p L, (Units.map ↑σ) ζ = ζ ^ a) (hb : ∀ ζ ∈ pPowerRootsOfUnity p L, (Units.map ↑τ) ζ = ζ ^ b) (hcard : Nat.card (MonoidAlgebra ℤ_[p] Gal(L/K) ⧸ Ideal.span {MonoidAlgebra.single σ 1 - ↑a, MonoidAlgebra.single τ 1 - ↑b}) = localRootOfUnityOrder p L h) : Nonempty (↥(pPowerTorsion p (MonoidAlgebra ℤ_[p] Gal(L/K)) (TameFrameModule ℤ_[p] Gal(L/K) σ τ ↑a ↑b)) ≃ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] ↥(pPowerTorsion p (MonoidAlgebra ℤ_[p] Gal(L/K)) (Additive ↥(padicCompletionUnits p L))))

The torsion of the tame-frame module for supplied sharp exponents. Let σ, τ generate the finite automorphism group of L/K. If a, b describe their action on the p-power roots of unity and the quotient ℤ_p[G] ⧸ (σ - a, τ - b) has the sharp cardinality q(L), then the p-power torsion of the tame-frame module is isomorphic to that of the p-adic completion A(L) as a left ℤ_p[G]-module.

theorem TauCeti.exists_tameFrameModule_torsion_linearEquiv {p : ℕ} [Fact (Nat.Prime p)] {L : Type u_1} [Field L] {K : Type u_2} [Field K] [Algebra K L] [Finite Gal(L/K)] (h : Finite ↥(pPowerRootsOfUnity p L)) (σ τ : Gal(L/K)) (hgen : Subgroup.closure {σ, τ} = ⊤) (hτ : ¬p ∣ orderOf τ) : ∃ (a : ℕ) (b : ℕ), (∀ ζ ∈ pPowerRootsOfUnity p L, (Units.map ↑σ) ζ = ζ ^ a) ∧ (∀ ζ ∈ pPowerRootsOfUnity p L, (Units.map ↑τ) ζ = ζ ^ b) ∧ Nat.card (MonoidAlgebra ℤ_[p] Gal(L/K) ⧸ Ideal.span {MonoidAlgebra.single σ 1 - ↑a, MonoidAlgebra.single τ 1 - ↑b}) = localRootOfUnityOrder p L h ∧ Nonempty (↥(pPowerTorsion p (MonoidAlgebra ℤ_[p] Gal(L/K)) (TameFrameModule ℤ_[p] Gal(L/K) σ τ ↑a ↑b)) ≃ₗ[MonoidAlgebra ℤ_[p] Gal(L/K)] ↥(pPowerTorsion p (MonoidAlgebra ℤ_[p] Gal(L/K)) (Additive ↥(padicCompletionUnits p L))))

The torsion of the tame-frame module of a tame frame is μ_{p^∞}(L). Let σ, τ generate the finite automorphism group G of L/K, with τ of order prime to p, and suppose L has finitely many p-power roots of unity. Then there are natural numbers a, b through which σ, τ act on μ_{p^∞}(L) such that the quotient ℤ_p[G] ⧸ (σ - a, τ - b) has order q(L) = #μ_{p^∞}(L), and the p-power torsion of the tame-frame module M₀ = ℤ_p[G]² / ℤ_p[G]·(σ - a, τ - b) is isomorphic as a left ℤ_p[G]-module to the p-power torsion of the p-adic completion A(L) of Lˣ, which is μ_{p^∞}(L) with its Galois action. For the same exponents, nonempty_tameFrameModule_tensorRat_linearEquiv identifies M₀ ⊗[ℤ_p] ℚ_p with ℤ_p[G] ⊗[ℤ_p] ℚ_p.