Recentering: the algebraic core

Let S be a commutative ring, ι : S →+* S a ring endomorphism (in the application, complex conjugation; it need not be an involution), μ a unit with ι μ = μ⁻¹ and μ ^ n = 1, and B a subring of S stable under ι. Suppose some x = μ^k a ∈ B with ι a = a is a unit of B, and gcd(2k, n) = 1. Then μ ∈ B; if B is generated by elements μ^(d j) a j with ι (a j) = a j, then B is generated by the a j and μ; and when μ − μ⁻¹ is a non-zero-divisor, the ι-fixed part of R[μ] is R for an ι-fixed subring R containing τ = μ + μ⁻¹.

The hypotheses (stability of B, the unit x of B, the non-zero-divisor) are supplied by the caller; integrality, Galois stability and the identities e_j(μT) = μ^j e_j(T) are not formalized here.

Main results

• NotaPuente.Recentering.mu_mem, NotaPuente.Recentering.mu_inv_mem: μ, μ⁻¹ ∈ B.
• NotaPuente.Recentering.B_eq_closure: B = closure (A' ∪ {μ}).
• NotaPuente.Recentering.mem_closure_iff_exists, NotaPuente.Recentering.eq_zero_of_fixed: every element of R[μ] is a + b μ with a, b ∈ R, and a + b μ fixed forces b = 0.
• NotaPuente.Recentering.fixed_iff_of_fixed_subring: (R[μ])^ι = R.
• NotaPuente.Recentering.recentering: the assembled statement.

References

• C. Marín, Non-real orders of character values of GL(n), preprint (2026).
• C. Marín, The ring of character values depends only on the segment: SU(n), Sp(2m) and GL(n) at a torsion element, Zenodo (2026), doi:10.5281/zenodo.22847476.

theorem NotaPuente.Recentering.iota_inv {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) : ι ↑μ⁻¹ = ↑μ

ι μ = μ⁻¹ forces ι μ⁻¹ = μ.

theorem NotaPuente.Recentering.pow_two_mul_eq {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) (k : ℕ) (a y : S) (hιa : ι a = a) (hxy : ↑μ ^ k * a * y = 1) : ↑μ ^ (2 * k) = ↑μ ^ k * a * ι y

Key identity: μ^(2k) = x * ι y when x = μ^k a, ι a = a, x y = 1.

theorem NotaPuente.Recentering.mu_mem {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) (n k : ℕ) (hn : ↑μ ^ n = 1) (hcop : (2 * k).Coprime n) (B : Subring S) (hB : ∀ z ∈ B, ι z ∈ B) (a y : S) (hιa : ι a = a) (hx : ↑μ ^ k * a ∈ B) (hy : y ∈ B) (hxy : ↑μ ^ k * a * y = 1) : ↑μ ∈ B

(1) μ ∈ B'.

theorem NotaPuente.Recentering.mu_inv_mem {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) (B : Subring S) (hB : ∀ z ∈ B, ι z ∈ B) (hμ : ↑μ ∈ B) : ↑μ⁻¹ ∈ B

μ⁻¹ ∈ B' as well (it is ι μ).

theorem NotaPuente.Recentering.B_eq_closure {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) (n : ℕ) (hn : ↑μ ^ n = 1) {J : Type u_2} (d : J → ℕ) (a : J → S) (hιa : ∀ (j : J), ι (a j) = a j) (B : Subring S) (hBdef : B = Subring.closure (Set.range fun (j : J) => ↑μ ^ d j * a j)) (hB : ∀ z ∈ B, ι z ∈ B) (j₀ : J) (hcop : (2 * d j₀).Coprime n) (y : S) (hy : y ∈ B) (hxy : ↑μ ^ d j₀ * a j₀ * y = 1) : B = Subring.closure (Set.range a ∪ {↑μ})

(2) B' = A'[μ]. B = closure {μ^(d j) * a j}, all a j ι-fixed, one generator μ^(d j₀) * a j₀ a unit of B with Coprime (2 d j₀) n. Then B = closure (range a ∪ {μ}).

theorem NotaPuente.Recentering.mem_closure_iff_exists {S : Type u_1} [CommRing S] (μ : Sˣ) (R : Subring S) (hτ : ↑μ + ↑μ⁻¹ ∈ R) (z : S) : z ∈ Subring.closure (↑R ∪ {↑μ}) ↔ ∃ a ∈ R, ∃ b ∈ R, z = a + b * ↑μ

(3a) spanning. If R contains τ = μ + μ⁻¹, every element of R[μ] is a + b μ.

theorem NotaPuente.Recentering.eq_zero_of_fixed {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) (hnzd : ↑μ - ↑μ⁻¹ ∈ nonZeroDivisors S) (a b : S) (hιa : ι a = a) (hιb : ι b = b) (hfix : ι (a + b * ↑μ) = a + b * ↑μ) : b = 0

(3b) directness. a + b μ ι-fixed with a, b ι-fixed and μ - μ⁻¹ a non-zero-divisor ⇒ b = 0.

theorem NotaPuente.Recentering.fixed_iff_of_fixed_subring {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) (hnzd : ↑μ - ↑μ⁻¹ ∈ nonZeroDivisors S) (R : Subring S) (hR : ∀ r ∈ R, ι r = r) (hτ : ↑μ + ↑μ⁻¹ ∈ R) (z : S) : z ∈ Subring.closure (↑R ∪ {↑μ}) ∧ ι z = z ↔ z ∈ R

(4) B'^ι = A'[τ]. With R ι-fixed containing τ, the ι-fixed elements of R[μ] = closure (R ∪ {μ}) are exactly R.

theorem NotaPuente.Recentering.recentering {S : Type u_1} [CommRing S] (ι : S →+* S) (μ : Sˣ) (hιμ : ι ↑μ = ↑μ⁻¹) (n : ℕ) (hn : ↑μ ^ n = 1) {J : Type u_2} (d : J → ℕ) (a : J → S) (hιa : ∀ (j : J), ι (a j) = a j) (B : Subring S) (hBdef : B = Subring.closure (Set.range fun (j : J) => ↑μ ^ d j * a j)) (hB : ∀ z ∈ B, ι z ∈ B) (j₀ : J) (hcop : (2 * d j₀).Coprime n) (y : S) (hy : y ∈ B) (hxy : ↑μ ^ d j₀ * a j₀ * y = 1) (hnzd : ↑μ - ↑μ⁻¹ ∈ nonZeroDivisors S) : have R := Subring.closure (Set.range a ∪ {↑μ + ↑μ⁻¹}); B = Subring.closure (↑R ∪ {↑μ}) ∧ ∀ (z : S), z ∈ B ∧ ι z = z ↔ z ∈ R

Lemma 5.4 assembled. Hypotheses as in B_eq_closure, plus μ - μ⁻¹ a non-zero-divisor. With R := A'[τ] = closure (range a ∪ {τ}): B = R[μ] and B^ι = R.