Naturality of the cyclotomic character

Mathlib's cyclotomicCharacter L p : (L ≃+* L) →* ℤ_[p]ˣ records the action of a ring automorphism of a domain L on the roots of unity of p-power order in L, and is the trivial character when L does not contain a primitive pⁱ-th root of unity for every i. This file proves that the character only depends on that action on roots of unity, so that it is natural along injective ring homomorphisms.

Concretely, let f : A →+* B be an injective homomorphism of domains intertwining automorphisms g of A and h of B, that is h (f x) = f (g x). If every primitive pⁱ-th root of unity needed by B already exists in A, then h and g have the same cyclotomic character. This is how the cyclotomic character of an absolute Galois group is compared across different models of the separable or algebraic closure, and across finite extensions of the ground field.

When L has all of these roots of unity, the character is characterized by that action: an automorphism raising every root of unity of p-power order to the c-th power has cyclotomic character c. This is how the character of an automorphism with a known action on roots of unity, such as a Frobenius lift or an element of inertia, is computed.

Main results

• TauCeti.cyclotomicCharacter_eq_one_of_not_forall_isPrimitiveRoot: the cyclotomic character of a domain lacking a primitive pⁱ-th root of unity for some i is trivial.
• TauCeti.cyclotomicCharacter_eq_of_forall_pow_eq_one: two automorphisms that agree on the roots of unity of p-power order have the same cyclotomic character.
• TauCeti.cyclotomicCharacter_eq_of_injective: the cyclotomic character is natural along an injective ring homomorphism intertwining two automorphisms.
• TauCeti.coe_cyclotomicCharacter_eq_natCast: an automorphism raising every root of unity of p-power order to the c-th power has cyclotomic character c.

@[simp]

theorem TauCeti.cyclotomicCharacter_eq_one_of_not_forall_isPrimitiveRoot {A : Type u_1} [CommRing A] [IsDomain A] (p : ℕ) [Fact (Nat.Prime p)] (H : ¬∀ (i : ℕ), ∃ (ζ : A), IsPrimitiveRoot ζ (p ^ i)) (g : A ≃+* A) : (cyclotomicCharacter A p) g = 1

The cyclotomic character is trivial without enough roots of unity: if a domain A lacks a primitive pⁱ-th root of unity for some i, its cyclotomic character is the trivial character.

theorem TauCeti.cyclotomicCharacter_eq_of_forall_pow_eq_one {A : Type u_1} [CommRing A] [IsDomain A] (p : ℕ) [Fact (Nat.Prime p)] {g h : A ≃+* A} (hgh : ∀ (n : ℕ) (t : A), t ^ p ^ n = 1 → g t = h t) : (cyclotomicCharacter A p) g = (cyclotomicCharacter A p) h

The cyclotomic character only depends on the action on roots of unity: two automorphisms of a domain A that agree on every root of unity of p-power order have the same cyclotomic character. In particular an automorphism fixing all these roots of unity has trivial character.

theorem TauCeti.cyclotomicCharacter_eq_of_injective {A : Type u_1} {B : Type u_2} [CommRing A] [IsDomain A] [CommRing B] [IsDomain B] (p : ℕ) [Fact (Nat.Prime p)] {f : A →+* B} (hf : Function.Injective ⇑f) {g : A ≃+* A} {h : B ≃+* B} (hfg : ∀ (x : A), h (f x) = f (g x)) (hroots : (∀ (i : ℕ), ∃ (ζ : B), IsPrimitiveRoot ζ (p ^ i)) → ∀ (i : ℕ), ∃ (ζ : A), IsPrimitiveRoot ζ (p ^ i)) : (cyclotomicCharacter B p) h = (cyclotomicCharacter A p) g

Naturality of the cyclotomic character. Let f : A →+* B be an injective homomorphism of domains with h ∘ f = f ∘ g for automorphisms g of A and h of B. If A has primitive pⁱ-th roots of unity for all i as soon as B does, then g and h have the same cyclotomic character.

theorem TauCeti.coe_cyclotomicCharacter_eq_natCast {A : Type u_1} [CommRing A] [IsDomain A] (p : ℕ) [Fact (Nat.Prime p)] [∀ (i : ℕ), HasEnoughRootsOfUnity A (p ^ i)] {g : A ≃+* A} {c : ℕ} (hc : ∀ (n : ℕ) (t : A), t ^ p ^ n = 1 → g t = t ^ c) : ↑((cyclotomicCharacter A p) g) = ↑c

The cyclotomic character of an automorphism acting by a fixed power. If a domain A contains all roots of unity of p-power order and g raises each of them to the c-th power, then the cyclotomic character of g is c.