Rational structure of the tame-frame module

This file identifies the tame-frame module M₀ = R[G]² / R[G]·(σ - a, τ - b) after extension of scalars to a field. The single relation defines a map

R[G] → R[G]², x ↦ x · (σ - a, τ - b).

For elements σ, τ of finite order, natural-number exponents, and a coefficient ring R of characteristic zero without zero divisors (such as ℤ_p), nonzero finite cardinality of the sharp quotient R[G] / (σ - a, τ - b) implies that this map is injective. Over a field k in which #G is nonzero, an injective tame-frame relation map presents one copy of the regular representation k[G]: this is the cancellation theorem TauCeti.nonempty_quotient_span_singleton_linearEquiv_of_injective for the semisimple ring k[G] (Maschke) applied to the defining relation.

The same cancellation applies after a flat base change R → k to a field in which #G is nonzero: the base change M₀ ⊗[R] k of the integral tame-frame module is the base change R[G] ⊗[R] k of the group ring, as a left R[G]-module (TauCeti.nonempty_quotient_span_singleton_tensor_linearEquiv_of_injective). For R = ℤ_p and k = ℚ_p this is the rationalisation M₀ ⊗ ℚ_p ≃ ℚ_p[G] of the tame-frame module of a finite tame layer of local fields, whose sharp exponents are supplied by TauCeti.exists_tameFrame_exponents.

Main results

• TauCeti.tameFrameRelationMap_injective_of_card_ne_zero: sharp finite quotient implies injectivity, for instance over ℤ_p with G finite.
• TauCeti.nonempty_tameFrameModule_linearEquiv_of_relationMap_injective: under Maschke's condition, an injective tame-frame relation map presents the regular representation.
• TauCeti.nonempty_tameFrameModule_tensor_linearEquiv_of_relationMap_injective: after a flat base change to a field satisfying Maschke's condition, an injective tame-frame relation map presents the base change of the group ring.
• TauCeti.nonempty_tameFrameModule_tensorRat_linearEquiv: the rationalisation M₀ ⊗[ℤ_p] ℚ_p ≃ ℤ_p[G] ⊗[ℤ_p] ℚ_p of the tame-frame module with sharp exponents.

References

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

theorem TauCeti.tameFrameRelationMap_injective_of_card_ne_zero {G : Type v} [Monoid G] {R : Type u} [CommRing R] [NoZeroDivisors R] [CharZero R] {σ τ : G} (hσ : IsOfFinOrder σ) (hτ : IsOfFinOrder τ) {a b : ℕ} (hcard : Nat.card (MonoidAlgebra R G ⧸ Ideal.span {MonoidAlgebra.single σ 1 - MonoidAlgebra.single 1 ↑a, MonoidAlgebra.single τ 1 - MonoidAlgebra.single 1 ↑b}) ≠ 0) : Function.Injective ⇑(tameFrameRelationMap R G σ τ ↑a ↑b)

Let R be a commutative ring of characteristic zero without zero divisors, and let σ, τ have finite order. For natural numbers a, b, nonzero finite cardinality of the sharp quotient R[G] / (σ - a, τ - b) implies that the tame-frame relation map is injective. For R = ℤ_p and finite G this is the integral injectivity input for the rational tame-frame computation.

theorem TauCeti.nonempty_tameFrameModule_linearEquiv_of_relationMap_injective {G : Type v} {k : Type u} [Field k] [Group G] [Finite G] [NeZero ↑(Nat.card G)] (σ τ : G) (a b : k) (hinj : Function.Injective ⇑(tameFrameRelationMap k G σ τ a b)) : Nonempty (TameFrameModule k G σ τ a b ≃ₗ[MonoidAlgebra k G] MonoidAlgebra k G)

Let G be finite and suppose that its cardinality is nonzero in k. If the tame-frame relation map is injective, then the tame-frame module is linearly equivalent to the regular representation k[G].

theorem TauCeti.nonempty_tameFrameModule_tensor_linearEquiv_of_relationMap_injective {G : Type v} {k : Type u} [Field k] [Group G] [Finite G] {R : Type u_1} [CommRing R] [Algebra R k] [Module.Flat R k] [NeZero ↑(Nat.card G)] (σ τ : G) (a b : R) (hinj : Function.Injective ⇑(tameFrameRelationMap R G σ τ a b)) : Nonempty (TensorProduct R (TameFrameModule R G σ τ a b) k ≃ₗ[MonoidAlgebra R G] TensorProduct R (MonoidAlgebra R G) k)

The base change of the tame-frame module to a field is the regular representation. Let G be finite, R a commutative ring and k a flat R-algebra which is a field in which the order of G is nonzero. If the integral tame-frame relation map is injective, then the base change M₀ ⊗[R] k of the tame-frame module is linearly equivalent, as a left R[G]-module, to the base change R[G] ⊗[R] k of the group ring.

theorem TauCeti.nonempty_tameFrameModule_tensorRat_linearEquiv {G : Type v} {p : ℕ} [Fact (Nat.Prime p)] [Group G] [Finite G] (σ τ : G) (a b : ℕ) (hcard : Nat.card (MonoidAlgebra ℤ_[p] G ⧸ Ideal.span {MonoidAlgebra.single σ 1 - ↑a, MonoidAlgebra.single τ 1 - ↑b}) ≠ 0) : Nonempty (TensorProduct ℤ_[p] (TameFrameModule ℤ_[p] G σ τ ↑a ↑b) ℚ_[p] ≃ₗ[MonoidAlgebra ℤ_[p] G] TensorProduct ℤ_[p] (MonoidAlgebra ℤ_[p] G) ℚ_[p])

The rationalisation of the tame-frame module with sharp exponents. Let G be a finite group, σ, τ : G, and a, b natural numbers for which the quotient ℤ_p[G] / (σ - a, τ - b) is finite, as the sharp exponents of a tame frame provide. Then M₀ ⊗[ℤ_p] ℚ_p ≃ ℤ_p[G] ⊗[ℤ_p] ℚ_p as left ℤ_p[G]-modules: the rationalised tame-frame module is the regular representation ℚ_p[G].