The Kummer character of a group of automorphisms

Let L / F be a field extension in which F is integrally closed (for fields: algebraically closed in L, as the constants of a function field are), G a monoid acting on L by F-algebra automorphisms, and α a unit of L whose n-th power no element of G moves. Then each σ ∈ G moves α by an n-th root of unity, which lies in F because F and L have the same n-th roots of unity (TauCeti.rootsOfUnityMulEquiv), and σ ↦ σ α / α is a homomorphism G →* rootsOfUnity n F: the Kummer character of α, with values in the constants. It is multiplicative in α, and trivial exactly when G fixes α.

Mathlib's autEquivRootsOfUnity is the Kummer isomorphism of a splitting field of Xⁿ - a over a base containing the n-th roots of unity; here the base is the constant field and the acting monoid is arbitrary.

Main definitions

• MonoidHom.kummerCharacter: for ρ : G →* (L ≃ₐ[F] L), the character σ ↦ ρ σ α / α of G with values in rootsOfUnity n F, written ρ.kummerCharacter n α hα.

Main results

• TauCeti.apply_div_pow_eq_one: if σ fixes αⁿ, then σ α / α is an n-th root of unity.
• MonoidHom.algebraMap_kummerCharacter: its value at σ, read in L, is σ α / α.
• MonoidHom.apply_eq_algebraMap_kummerCharacter_mul: σ moves α by its value.
• MonoidHom.kummerCharacter_mul: it is multiplicative in α.
• MonoidHom.kummerCharacter_algebraMap_mul: it is unchanged by a constant factor.
• MonoidHom.kummerCharacter_eq_one_iff: it is trivial exactly when G fixes α.

References

• J. Silverman, The Arithmetic of Elliptic Curves, III.8.1, where the Weil pairing is this character for the translation action of E[n].

theorem TauCeti.apply_div_pow_eq_one {M : Type u_1} {S : Type u_2} [CommGroupWithZero M] [FunLike S M M] [MonoidHomClass S M M] {σ : S} {α : M} {n : ℕ} (hα : α ≠ 0) (h : σ (α ^ n) = α ^ n) : (σ α / α) ^ n = 1

If σ fixes α ^ n for a nonzero α, then σ α / α is an n-th root of unity.

noncomputable def MonoidHom.kummerCharacter {F : Type u_1} {L : Type u_2} {G : Type u_3} [Field F] [Field L] [Algebra F L] [IsIntegrallyClosedIn F L] [Monoid G] (ρ : G →* L ≃ₐ[F] L) (n : ℕ) [NeZero n] (α : Lˣ) (hα : ∀ (σ : G), (ρ σ) (↑α ^ n) = ↑α ^ n) : G →* ↥(rootsOfUnity n F)

The Kummer character of α: σ ↦ σ α / α, which lies in the n-th roots of unity of F as soon as no element of G moves αⁿ.

Equations

• ρ.kummerCharacter n α hα = { toFun := fun (σ : G) => (TauCeti.rootsOfUnityMulEquiv F L n).symm (MonoidHom.ratio✝ ρ n hα σ), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem MonoidHom.algebraMap_kummerCharacter {F : Type u_1} {L : Type u_2} {G : Type u_3} [Field F] [Field L] [Algebra F L] [IsIntegrallyClosedIn F L] [Monoid G] {ρ : G →* L ≃ₐ[F] L} {n : ℕ} [NeZero n] {α : Lˣ} (hα : ∀ (σ : G), (ρ σ) (↑α ^ n) = ↑α ^ n) (σ : G) : (algebraMap F L) ↑↑((ρ.kummerCharacter n α hα) σ) = (ρ σ) ↑α / ↑α

The value of the Kummer character, read in L: χ(σ) = σ α / α.

theorem MonoidHom.apply_eq_algebraMap_kummerCharacter_mul {F : Type u_1} {L : Type u_2} {G : Type u_3} [Field F] [Field L] [Algebra F L] [IsIntegrallyClosedIn F L] [Monoid G] {ρ : G →* L ≃ₐ[F] L} {n : ℕ} [NeZero n] {α : Lˣ} (hα : ∀ (σ : G), (ρ σ) (↑α ^ n) = ↑α ^ n) (σ : G) : (ρ σ) ↑α = (algebraMap F L) ↑↑((ρ.kummerCharacter n α hα) σ) * ↑α

The Kummer character moves α by its value: σ α = χ(σ) α.

theorem MonoidHom.kummerCharacter_mul {F : Type u_1} {L : Type u_2} {G : Type u_3} [Field F] [Field L] [Algebra F L] [IsIntegrallyClosedIn F L] [Monoid G] {ρ : G →* L ≃ₐ[F] L} {n : ℕ} [NeZero n] {α β : Lˣ} (hα : ∀ (σ : G), (ρ σ) (↑α ^ n) = ↑α ^ n) (hβ : ∀ (σ : G), (ρ σ) (↑β ^ n) = ↑β ^ n) : ρ.kummerCharacter n (α * β) ⋯ = ρ.kummerCharacter n α hα * ρ.kummerCharacter n β hβ

The Kummer character is multiplicative in α; G fixes (α β)ⁿ = αⁿ βⁿ because it fixes both factors.

theorem MonoidHom.kummerCharacter_algebraMap_mul {F : Type u_1} {L : Type u_2} {G : Type u_3} [Field F] [Field L] [Algebra F L] [IsIntegrallyClosedIn F L] [Monoid G] {ρ : G →* L ≃ₐ[F] L} {n : ℕ} [NeZero n] {α : Lˣ} (c : Fˣ) (hα : ∀ (σ : G), (ρ σ) (↑α ^ n) = ↑α ^ n) : ρ.kummerCharacter n ((Units.map ↑(algebraMap F L)) c * α) ⋯ = ρ.kummerCharacter n α hα

The Kummer character is unchanged by a constant factor: G fixes the constant c, so it moves c α and α by the same roots of unity.

theorem MonoidHom.kummerCharacter_eq_one_iff {F : Type u_1} {L : Type u_2} {G : Type u_3} [Field F] [Field L] [Algebra F L] [IsIntegrallyClosedIn F L] [Monoid G] {ρ : G →* L ≃ₐ[F] L} {n : ℕ} [NeZero n] {α : Lˣ} (hα : ∀ (σ : G), (ρ σ) (↑α ^ n) = ↑α ^ n) : ρ.kummerCharacter n α hα = 1 ↔ ∀ (σ : G), (ρ σ) ↑α = ↑α

The Kummer character is trivial exactly when G fixes α.