The tame-frame module

For two elements σ, τ of a monoid G and two coefficients a, b in a ring R, the tame-frame module is the left R[G]-module with two generators and one relation,

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

In the computation of the generator rank of the absolute Galois group of a p-adic field (NSW (7.4.1)), R = ℤ_p, σ, τ are the images in a finite Galois group of the two tame generators of the absolute Galois group, and a, b are exponents through which they act on the p-power roots of unity. The module is a quotient of R[G]², which is where the 2 in the generator count [K : ℚ_p] + 2 comes from.

The module is presented by Mathlib's Module.Relations: tameFrameRelations has generator type Fin 2 and a single relation, and TameFrameModule is its Module.Relations.Quotient. The class of Finsupp.single i 1 under Module.Relations.toQuotient is the generator eᵢ, and Module.Relations.toQuotient_relation says that the generators satisfy the relation. A left R[G]-linear map out of M₀ is a pair of elements x, y of the target with (σ - a) x + (τ - b) y = 0: tameFrameSolution packages such a pair as a Module.Relations.Solution, whose Module.Relations.Solution.fromQuotient is the map, and Module.Relations.Quotient.linearMap_ext says that a map out of M₀ is determined by the images of e₀, e₁.

Main definitions

• TauCeti.tameFrameRelations: two generators subject to the relation (σ - a) e₀ + (τ - b) e₁ = 0.
• TauCeti.TameFrameModule: the module R[G]² / R[G]·(σ - a, τ - b) it presents.
• TauCeti.tameFrameRelationMap: the map from R[G] into R[G]² generated by the relation.
• TauCeti.tameFrameSolution: the solution of the relation in a module M given by x, y ∈ M with (σ - a) x + (τ - b) y = 0.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.tameFrameRelations (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) : Module.Relations (MonoidAlgebra R G)

The relations of the tame-frame module of two elements σ, τ of G and two coefficients a, b of R: two generators e₀, e₁ subject to the single relation (σ - a) e₀ + (τ - b) e₁ = 0.

@[reducible, inline]

abbrev TauCeti.TameFrameModule (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) : Type (max u v)

The tame-frame module M₀ = R[G]² / R[G]·(σ - a, τ - b) of two elements σ, τ of G and two coefficients a, b of R: the left R[G]-module presented by tameFrameRelations.

noncomputable def TauCeti.tameFrameRelationMap (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) : MonoidAlgebra R G →ₗ[MonoidAlgebra R G] Fin 2 →₀ MonoidAlgebra R G

The left R[G]-linear map whose range is the relation submodule defining the tame-frame module. It sends x to x · (σ - a, τ - b).

theorem TauCeti.tameFrameRelationMap_def (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) : tameFrameRelationMap R G σ τ a b = LinearMap.toSpanSingleton (MonoidAlgebra R G) (Fin 2 →₀ MonoidAlgebra R G) ((tameFrameRelations R G σ τ a b).relation ())

The tame-frame relation map is LinearMap.toSpanSingleton of the defining relation (σ - a, τ - b).

theorem TauCeti.tameFrameRelationMap_apply (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) (x : MonoidAlgebra R G) : (tameFrameRelationMap R G σ τ a b) x = x • (tameFrameRelations R G σ τ a b).relation ()

The tame-frame relation map sends x to x times the defining relation (σ - a, τ - b).

@[simp]

theorem TauCeti.tameFrameRelationMap_apply_zero (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) (x : MonoidAlgebra R G) : ((tameFrameRelationMap R G σ τ a b) x) 0 = x * (MonoidAlgebra.single σ 1 - MonoidAlgebra.single 1 a)

The zeroth coordinate of the tame-frame relation map is right multiplication by σ - a.

@[simp]

theorem TauCeti.tameFrameRelationMap_apply_one (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) (x : MonoidAlgebra R G) : ((tameFrameRelationMap R G σ τ a b) x) 1 = x * (MonoidAlgebra.single τ 1 - MonoidAlgebra.single 1 b)

The first coordinate of the tame-frame relation map is right multiplication by τ - b.

theorem TauCeti.range_tameFrameRelationMap (R : Type u) [Ring R] (G : Type v) [Monoid G] (σ τ : G) (a b : R) : (tameFrameRelationMap R G σ τ a b).range = Submodule.span (MonoidAlgebra R G) (Set.range (tameFrameRelations R G σ τ a b).relation)

The range of the tame-frame relation map is the relation submodule by which TameFrameModule is defined as a quotient.

noncomputable def TauCeti.tameFrameSolution {R : Type u} [Ring R] {G : Type v} [Monoid G] {σ τ : G} {a b : R} {M : Type u_1} [AddCommGroup M] [Module (MonoidAlgebra R G) M] (x y : M) (h : (MonoidAlgebra.single σ 1 - MonoidAlgebra.single 1 a) • x + (MonoidAlgebra.single τ 1 - MonoidAlgebra.single 1 b) • y = 0) : (tameFrameRelations R G σ τ a b).Solution M

The solution of tameFrameRelations in M sending the generators e₀, e₁ to x, y, for x, y satisfying the relation (σ - a) x + (τ - b) y = 0. Its Module.Relations.Solution.fromQuotient is the left R[G]-linear map out of the tame-frame module sending e₀, e₁ to x, y.

@[simp]

theorem TauCeti.tameFrameSolution_var_zero {R : Type u} [Ring R] {G : Type v} [Monoid G] {σ τ : G} {a b : R} {M : Type u_1} [AddCommGroup M] [Module (MonoidAlgebra R G) M] (x y : M) (h : (MonoidAlgebra.single σ 1 - MonoidAlgebra.single 1 a) • x + (MonoidAlgebra.single τ 1 - MonoidAlgebra.single 1 b) • y = 0) : (tameFrameSolution x y h).var 0 = x

The solution tameFrameSolution x y h sends the generator e₀ to x.

@[simp]

theorem TauCeti.tameFrameSolution_var_one {R : Type u} [Ring R] {G : Type v} [Monoid G] {σ τ : G} {a b : R} {M : Type u_1} [AddCommGroup M] [Module (MonoidAlgebra R G) M] (x y : M) (h : (MonoidAlgebra.single σ 1 - MonoidAlgebra.single 1 a) • x + (MonoidAlgebra.single τ 1 - MonoidAlgebra.single 1 b) • y = 0) : (tameFrameSolution x y h).var 1 = y

The solution tameFrameSolution x y h sends the generator e₁ to y.