The orientations of the Demushkin normal forms

Each Demushkin normal form whose relator word TauCeti.Topology.Algebra.Group.Profinite.Demushkin.NormalForm.Basic defines carries a marked continuous character to ℤ_pˣ, its standard orientation, with the values that Labute's Theorem 4 tabulates on the normal-form basis:

• q ≠ 2, n even: χ(x₂) = (1 - q)⁻¹ and χ(x_i) = 1 otherwise;
• q = 2, n odd: χ(x₁) = -1, χ(x₃) = (1 - 2^f)⁻¹ and χ(x_i) = 1 otherwise; at f = ∞, where the factor x₂^{2^f} is absent, χ(x₁) = -1 and χ(x_i) = 1 otherwise;
• q = 2, n even: χ(x₂) = -(1 + α)⁻¹, χ(x₄) = (1 - 2^f)⁻¹ and χ(x_i) = 1 otherwise.

These characters exist because the values kill the relator: the commutators die in the commutative group ℤ_pˣ, and the remaining factors are powers of generators sent to 1 or to -1 with even exponent. This file constructs, on the presented pro-p group of each of these normal forms, the continuous characters of this shape with the marked values left as parameters: orientationNeTwo q n u with χ(x₂) = u, orientationTwoOdd f n u with χ(x₁) = -1, χ(x₃) = u, and orientationTwoEven a f n v u with χ(x₂) = v, χ(x₄) = u, each trivial on the other generators; on the rank-two word x₁^{2+α} (x₁, x₂), which has no level, orientationTwoRankTwo a v with χ(x₂) = v and χ(x₁) = 1; and on the odd word at f = ∞, x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n), which has no level and no marked value, orientationTwoOddTop n with χ(x₁) = -1. The standard orientation is the member of the family with the tabulated values, prescribed through the equations they satisfy, u (1 - q) = 1 for q = p^f and v (1 + α) = -1, so that no inverse has to be constructed to state a result. The characters themselves are defined for arbitrary u, v (with u in 1 + pℤ_p for the first family, so that the target of the lift is pro-p); the equations enter only in the image computations.

The image of each character is the closed subgroup of ℤ_pˣ generated by the marked values whose generators exist: 1 < n for the first family and 2 < n for the second, which the classification always provides (n ≥ 2 even, n ≥ 3 odd). In the third family the classification allows every even n ≥ 2, and the two marked generators split it: for 3 < n the image is generated by v and u, while for 1 < n ≤ 3 the generator x₂ exists but x₄ does not and the image is generated by v alone. The bound n ≤ 3 covers two words: in rank two x₃ and x₄ are trivial and the relator is x₁^{2+α} (x₁, x₂), while in rank three the relator is x₁^{2+α} (x₁, x₂) x₃^{2^f}; the character is trivial on x₃, so the two ranks have the same image. Under these rank bounds and the equations on u, v, the images are the closed subgroups computed in TauCeti.NumberTheory.Padics.GeneratedClosedSubgroups: 1 + qℤ_p in the first case, {±1} × U^(f) in the second, and in the third, for 3 < n, {±1} × U^(f) when 2^f ∣ α and the twisted subgroup U^[v₂(α)] otherwise; for 1 < n ≤ 3, {±1} when α = 0 and U^[v₂(α)] otherwise. In rank two, where x₃^{2^f} is absent, these are the f = ∞ endpoint of the table. The odd word at f = ∞ has image {±1} = {±1} × U^(∞), the f = ∞ endpoint of the second row, as soon as 0 < n. The even f = ∞ form of rank at least four, whose relator drops the x₃^{2^f} factor, is not presented here and has no character in this file.

Main definitions

• TauCeti.orientationNeTwo, TauCeti.orientationTwoOdd, TauCeti.orientationTwoEven: the characters of the three normal forms with the shape of the standard orientation and marked values u, resp. -1 and u, resp. v and u; TauCeti.orientationTwoRankTwo: the same on the rank-two word, with marked value v; TauCeti.orientationTwoOddTop: the standard orientation of the odd word at f = ∞, with χ(x₁) = -1.

Main results

• TauCeti.orientationNeTwo_of and the _presentedProPGen_ lemmas, with their companions for the other families: the values on the generators.
• TauCeti.range_orientationNeTwo, TauCeti.range_orientationTwoOdd, TauCeti.range_orientationTwoEven: for 1 < n, resp. 2 < n, resp. 3 < n, the image is the closed subgroup generated by the marked values; TauCeti.range_orientationTwoOddTop: for 0 < n, the image of the standard orientation of the odd word at f = ∞ is {±1}; TauCeti.range_orientationTwoEven_of_le_three: for 1 < n ≤ 3, the closed subgroup generated by v; TauCeti.range_orientationTwoRankTwo: on the rank-two word, the closed subgroup generated by v.
• TauCeti.range_orientationNeTwo_eq_unitsPrincipal, TauCeti.range_orientationTwoOdd_eq_unitsPlusMinus, TauCeti.range_orientationTwoEven_eq_unitsPlusMinus_of_dvd, TauCeti.exists_range_orientationTwoEven_eq_of_not_dvd: the image table of the standard orientations, under the same rank bounds; TauCeti.range_orientationTwoEven_eq_zpowers_neg_one and TauCeti.exists_range_orientationTwoEven_eq_of_ne_zero: the rows of the table for 1 < n ≤ 3, rank two and rank three alike; TauCeti.range_orientationTwoRankTwo_eq_zpowers_neg_one and TauCeti.exists_range_orientationTwoRankTwo_eq_of_ne_zero: the same rows on the rank-two word.
• TauCeti.exists_range_orientationNeTwo_eq_unitsPrincipal, TauCeti.exists_range_orientationTwoOdd_eq_unitsPlusMinus, TauCeti.exists_range_orientationTwoEven_eq_unitsPlusMinus_of_dvd, TauCeti.exists_units_range_orientationTwoEven_eq_of_not_dvd, TauCeti.exists_range_orientationTwoEven_eq_zpowers_neg_one, TauCeti.exists_unit_range_orientationTwoEven_eq_of_ne_zero, TauCeti.exists_range_orientationTwoRankTwo_eq_zpowers_neg_one, TauCeti.exists_unit_range_orientationTwoRankTwo_eq_of_ne_zero: the standard orientations exist, as the members of the families whose marked values satisfy the equations, with the tabulated images, one theorem per row of the table.

References

• J. P. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), 106–132, Theorem 4 and its corollary.
• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter III, §9.

The q ≠ 2 normal form

noncomputable def TauCeti.orientationNeTwo {p : ℕ} [Fact (Nat.Prime p)] (q n : ℕ) (u : ℤ_[p]ˣ) (hu : u ∈ unitsPrincipal p 1) : presentedProP p (Fin n) {demushkinWordNeTwo q n (freeProPGen p n)} →ₜ* ℤ_[p]ˣ

The orientation of the q ≠ 2 normal form with marked value u: the continuous character of the pro-p group presented on n generators by x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) with χ(x₂) = u and χ(x_i) = 1 otherwise, for a principal unit u. The standard orientation of the classification is the case u = (1 - q)⁻¹.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.orientationNeTwo_of {p : ℕ} [Fact (Nat.Prime p)] (q n : ℕ) (u : ℤ_[p]ˣ) (hu : u ∈ unitsPrincipal p 1) (i : Fin n) : (orientationNeTwo q n u hu) (presentedProP.of p {demushkinWordNeTwo q n (freeProPGen p n)} i) = if ↑i = 1 then u else 1

The value of the orientation of the q ≠ 2 normal form on the generators.

theorem TauCeti.orientationNeTwo_presentedProPGen_one {p : ℕ} [Fact (Nat.Prime p)] (q n : ℕ) (u : ℤ_[p]ˣ) (hu : u ∈ unitsPrincipal p 1) (hn : 1 < n) : (orientationNeTwo q n u hu) (presentedProPGen p n {demushkinWordNeTwo q n (freeProPGen p n)} 1) = u

The orientation of the q ≠ 2 normal form takes x₂ to its marked value u.

@[simp]

theorem TauCeti.orientationNeTwo_presentedProPGen_of_ne {p : ℕ} [Fact (Nat.Prime p)] (q n : ℕ) (u : ℤ_[p]ˣ) (hu : u ∈ unitsPrincipal p 1) {i : ℕ} (hi : i ≠ 1) : (orientationNeTwo q n u hu) (presentedProPGen p n {demushkinWordNeTwo q n (freeProPGen p n)} i) = 1

The orientation of the q ≠ 2 normal form is trivial on every generator other than x₂.

theorem TauCeti.range_orientationNeTwo {p : ℕ} [Fact (Nat.Prime p)] (q n : ℕ) (u : ℤ_[p]ˣ) (hu : u ∈ unitsPrincipal p 1) (hn : 1 < n) : (orientationNeTwo q n u hu).range = (Subgroup.zpowers u).topologicalClosure

The image of the orientation of the q ≠ 2 normal form is the closed subgroup generated by its marked value u, as soon as the generator x₂ exists.

theorem TauCeti.range_orientationNeTwo_eq_unitsPrincipal {p : ℕ} [Fact (Nat.Prime p)] (q n : ℕ) (u : ℤ_[p]ˣ) (hu : u ∈ unitsPrincipal p 1) (hn : 1 < n) {f : ℕ} (hq : q = p ^ f) (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) (hu' : ↑u * (1 - ↑q) = 1) : (orientationNeTwo q n u hu).range = unitsPrincipal p f

The image of the standard orientation of the q ≠ 2 normal form is 1 + qℤ_p: for 1 < n and q = p^f with f ≥ 1, and f ≥ 2 when p = 2, the character with χ(x₂) = (1 - q)⁻¹ and χ(x_i) = 1 otherwise has image U^(f) = 1 + qℤ_p.

theorem TauCeti.exists_range_orientationNeTwo_eq_unitsPrincipal {p : ℕ} [Fact (Nat.Prime p)] (q n : ℕ) (hn : 1 < n) {f : ℕ} (hq : q = p ^ f) (hf : 0 < f) (hf₂ : p = 2 → 2 ≤ f) : ∃ (u : ℤ_[p]ˣ) (hu : u ∈ unitsPrincipal p 1), ↑u * (1 - ↑q) = 1 ∧ (orientationNeTwo q n u hu).range = unitsPrincipal p f

The standard orientation of the q ≠ 2 normal form exists: for 1 < n and q = p^f with f ≥ 1, and f ≥ 2 when p = 2, there is a principal unit u with u (1 - q) = 1, and the character with χ(x₂) = u and χ(x_i) = 1 otherwise has image U^(f) = 1 + qℤ_p.

The q = 2, n odd normal form

noncomputable def TauCeti.orientationTwoOdd (f n : ℕ) (u : ℤ_[2]ˣ) : presentedProP 2 (Fin n) {demushkinWordTwoOdd f n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ

The orientation of the q = 2, n odd normal form with marked value u: the continuous character of the pro-2 group presented on n generators by x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) with χ(x₁) = -1, χ(x₃) = u and χ(x_i) = 1 otherwise. The standard orientation of the classification is the case u = (1 - 2^f)⁻¹.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.orientationTwoOdd_of (f n : ℕ) (u : ℤ_[2]ˣ) (i : Fin n) : (orientationTwoOdd f n u) (presentedProP.of 2 {demushkinWordTwoOdd f n (freeProPGen 2 n)} i) = if ↑i = 0 then -1 else if ↑i = 2 then u else 1

The value of the orientation of the q = 2, n odd normal form on the generators.

theorem TauCeti.orientationTwoOdd_presentedProPGen_zero (f n : ℕ) (u : ℤ_[2]ˣ) (hn : 0 < n) : (orientationTwoOdd f n u) (presentedProPGen 2 n {demushkinWordTwoOdd f n (freeProPGen 2 n)} 0) = -1

The orientation of the q = 2, n odd normal form takes x₁ to -1.

theorem TauCeti.orientationTwoOdd_presentedProPGen_two (f n : ℕ) (u : ℤ_[2]ˣ) (hn : 2 < n) : (orientationTwoOdd f n u) (presentedProPGen 2 n {demushkinWordTwoOdd f n (freeProPGen 2 n)} 2) = u

The orientation of the q = 2, n odd normal form takes x₃ to its marked value u.

@[simp]

theorem TauCeti.orientationTwoOdd_presentedProPGen_of_ne (f n : ℕ) (u : ℤ_[2]ˣ) {i : ℕ} (hi₀ : i ≠ 0) (hi₂ : i ≠ 2) : (orientationTwoOdd f n u) (presentedProPGen 2 n {demushkinWordTwoOdd f n (freeProPGen 2 n)} i) = 1

The orientation of the q = 2, n odd normal form is trivial on every generator other than x₁ and x₃.

theorem TauCeti.range_orientationTwoOdd (f n : ℕ) (u : ℤ_[2]ˣ) (hn : 2 < n) : (orientationTwoOdd f n u).range = (Subgroup.zpowers (-1) ⊔ Subgroup.zpowers u).topologicalClosure

The image of the orientation of the q = 2, n odd normal form is the closed subgroup generated by -1 and its marked value u, as soon as the generator x₃ exists.

theorem TauCeti.range_orientationTwoOdd_eq_unitsPlusMinus (f n : ℕ) (u : ℤ_[2]ˣ) (hn : 2 < n) (hf : 2 ≤ f) (hu : ↑u * (1 - 2 ^ f) = 1) : (orientationTwoOdd f n u).range = unitsPlusMinus f

The image of the standard orientation of the q = 2, n odd normal form is {±1} × U^(f): for 2 < n and f ≥ 2, the character with χ(x₁) = -1, χ(x₃) = (1 - 2^f)⁻¹ and χ(x_i) = 1 otherwise has image V^(f).

theorem TauCeti.exists_range_orientationTwoOdd_eq_unitsPlusMinus (f n : ℕ) (hn : 2 < n) (hf : 2 ≤ f) : ∃ (u : ℤ_[2]ˣ), ↑u * (1 - 2 ^ f) = 1 ∧ (orientationTwoOdd f n u).range = unitsPlusMinus f

The standard orientation of the q = 2, n odd normal form exists: for 2 < n and f ≥ 2, there is a unit u with u (1 - 2^f) = 1, and the character with χ(x₁) = -1, χ(x₃) = u and χ(x_i) = 1 otherwise has image V^(f) = {±1} × U^(f).

The q = 2, n odd normal form at level f = ∞

noncomputable def TauCeti.orientationTwoOddTop (n : ℕ) : presentedProP 2 (Fin n) {demushkinWordTwoOddTop n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ

The standard orientation of the q = 2, n odd normal form at level f = ∞: the continuous character of the pro-2 group presented on n generators by x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) with χ(x₁) = -1 and χ(x_i) = 1 otherwise. The word carries no level, so the character carries no marked value.

Equations

• TauCeti.orientationTwoOddTop n = TauCeti.presentedProP.lift (TauCeti.freeProP.lift TauCeti.isProP_units_padicInt_two fun (i : Fin n) => if ↑i = 0 then -1 else 1) ⋯

@[simp]

theorem TauCeti.orientationTwoOddTop_of (n : ℕ) (i : Fin n) : (orientationTwoOddTop n) (presentedProP.of 2 {demushkinWordTwoOddTop n (freeProPGen 2 n)} i) = if ↑i = 0 then -1 else 1

The value of the standard orientation of the odd normal form at f = ∞ on the generators.

theorem TauCeti.orientationTwoOddTop_presentedProPGen_zero (n : ℕ) (hn : 0 < n) : (orientationTwoOddTop n) (presentedProPGen 2 n {demushkinWordTwoOddTop n (freeProPGen 2 n)} 0) = -1

The standard orientation of the odd normal form at f = ∞ takes x₁ to -1.

@[simp]

theorem TauCeti.orientationTwoOddTop_presentedProPGen_of_ne (n : ℕ) {i : ℕ} (hi₀ : i ≠ 0) : (orientationTwoOddTop n) (presentedProPGen 2 n {demushkinWordTwoOddTop n (freeProPGen 2 n)} i) = 1

The standard orientation of the odd normal form at f = ∞ is trivial on every generator other than x₁.

theorem TauCeti.range_orientationTwoOddTop (n : ℕ) (hn : 0 < n) : (orientationTwoOddTop n).range = Subgroup.zpowers (-1)

The image of the standard orientation of the odd normal form at f = ∞ is {±1}, as soon as the generator x₁ exists: it is {±1} × U^(∞), the f = ∞ endpoint of the image table of the odd normal forms.

The q = 2, n even normal form

noncomputable def TauCeti.orientationTwoEven (a f n : ℕ) (v u : ℤ_[2]ˣ) : presentedProP 2 (Fin n) {demushkinWordTwoEven a f n (freeProPGen 2 n)} →ₜ* ℤ_[2]ˣ

The orientation of the q = 2, n even normal form with marked values v, u: the continuous character of the pro-2 group presented on n generators by x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) with χ(x₂) = v, χ(x₄) = u and χ(x_i) = 1 otherwise. The standard orientation of the classification is the case v = -(1 + a)⁻¹, u = (1 - 2^f)⁻¹.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.orientationTwoEven_of (a f n : ℕ) (v u : ℤ_[2]ˣ) (i : Fin n) : (orientationTwoEven a f n v u) (presentedProP.of 2 {demushkinWordTwoEven a f n (freeProPGen 2 n)} i) = if ↑i = 1 then v else if ↑i = 3 then u else 1

The value of the orientation of the q = 2, n even normal form on the generators.

theorem TauCeti.orientationTwoEven_presentedProPGen_one (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 1 < n) : (orientationTwoEven a f n v u) (presentedProPGen 2 n {demushkinWordTwoEven a f n (freeProPGen 2 n)} 1) = v

The orientation of the q = 2, n even normal form takes x₂ to its marked value v.

theorem TauCeti.orientationTwoEven_presentedProPGen_three (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 3 < n) : (orientationTwoEven a f n v u) (presentedProPGen 2 n {demushkinWordTwoEven a f n (freeProPGen 2 n)} 3) = u

The orientation of the q = 2, n even normal form takes x₄ to its marked value u.

@[simp]

theorem TauCeti.orientationTwoEven_presentedProPGen_of_ne (a f n : ℕ) (v u : ℤ_[2]ˣ) {i : ℕ} (hi₁ : i ≠ 1) (hi₃ : i ≠ 3) : (orientationTwoEven a f n v u) (presentedProPGen 2 n {demushkinWordTwoEven a f n (freeProPGen 2 n)} i) = 1

The orientation of the q = 2, n even normal form is trivial on every generator other than x₂ and x₄.

theorem TauCeti.range_orientationTwoEven (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 3 < n) : (orientationTwoEven a f n v u).range = (Subgroup.zpowers v ⊔ Subgroup.zpowers u).topologicalClosure

The image of the orientation of the q = 2, n even normal form is the closed subgroup generated by its marked values v and u, as soon as the generator x₄ exists.

theorem TauCeti.range_orientationTwoEven_eq_unitsPlusMinus_of_dvd (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 3 < n) (hf : 2 ≤ f) (hv : ↑v * (1 + ↑a) = -1) (hu : ↑u * (1 - 2 ^ f) = 1) (ha : 2 ^ f ∣ ↑a) : (orientationTwoEven a f n v u).range = unitsPlusMinus f

The image of the standard orientation of the q = 2, n even normal form when 2^f ∣ α is {±1} × U^(f): for 3 < n and f ≥ 2, the character with χ(x₂) = -(1 + a)⁻¹, χ(x₄) = (1 - 2^f)⁻¹ and χ(x_i) = 1 otherwise has image V^(f). This includes a = 0.

theorem TauCeti.exists_range_orientationTwoEven_eq_unitsPlusMinus_of_dvd (a f n : ℕ) (hn : 3 < n) (hf : 2 ≤ f) (ha : 2 ^ f ∣ ↑a) : ∃ (v : ℤ_[2]ˣ) (u : ℤ_[2]ˣ), ↑v * (1 + ↑a) = -1 ∧ ↑u * (1 - 2 ^ f) = 1 ∧ (orientationTwoEven a f n v u).range = unitsPlusMinus f

The standard orientation of the q = 2, n even normal form exists when 2^f ∣ α: for 3 < n and f ≥ 2, there are units v, u with v (1 + a) = -1 and u (1 - 2^f) = 1, and the character with χ(x₂) = v, χ(x₄) = u and χ(x_i) = 1 otherwise has image V^(f) = {±1} × U^(f).

theorem TauCeti.exists_range_orientationTwoEven_eq_of_not_dvd (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 3 < n) (hv : ↑v * (1 + ↑a) = -1) (hu : ↑u * (1 - 2 ^ f) = 1) (ha₄ : 4 ∣ ↑a) (ha : ¬2 ^ f ∣ ↑a) : ∃ (g : ℕ) (w : ℤ_[2]ˣ), 2 ≤ g ∧ g < f ∧ 2 ^ g ∣ ↑a ∧ ¬2 ^ (g + 1) ∣ ↑a ∧ ↑w = -1 + 2 ^ g ∧ (orientationTwoEven a f n v u).range = (Subgroup.zpowers w).topologicalClosure

The image of the standard orientation of the q = 2, n even normal form when 4 ∣ α but 2^f ∤ α is the twisted subgroup U^[g] generated by -1 + 2^g, where g = v₂(α) satisfies 2 ≤ g < f, for 3 < n.

theorem TauCeti.exists_units_range_orientationTwoEven_eq_of_not_dvd (a f n : ℕ) (hn : 3 < n) (ha₄ : 4 ∣ ↑a) (ha : ¬2 ^ f ∣ ↑a) : ∃ (v : ℤ_[2]ˣ) (u : ℤ_[2]ˣ) (g : ℕ) (w : ℤ_[2]ˣ), ↑v * (1 + ↑a) = -1 ∧ ↑u * (1 - 2 ^ f) = 1 ∧ 2 ≤ g ∧ g < f ∧ 2 ^ g ∣ ↑a ∧ ¬2 ^ (g + 1) ∣ ↑a ∧ ↑w = -1 + 2 ^ g ∧ (orientationTwoEven a f n v u).range = (Subgroup.zpowers w).topologicalClosure

The standard orientation of the q = 2, n even normal form exists when 4 ∣ α but 2^f ∤ α: for 3 < n, there are units v, u with v (1 + a) = -1 and u (1 - 2^f) = 1, and the character with χ(x₂) = v, χ(x₄) = u and χ(x_i) = 1 otherwise has image the twisted subgroup U^[g] generated by -1 + 2^g, where g = v₂(α) satisfies 2 ≤ g < f.

theorem TauCeti.range_orientationTwoEven_of_le_three (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 1 < n) (hn' : n ≤ 3) : (orientationTwoEven a f n v u).range = (Subgroup.zpowers v).topologicalClosure

The image of the orientation of the q = 2, n even normal form for 1 < n ≤ 3 is the closed subgroup generated by its marked value v: the generator x₂ exists but x₄ does not. In rank two the relator is x₁^{2+a} (x₁, x₂), in rank three it is x₁^{2+a} (x₁, x₂) x₃^{2^f}, and the character is trivial on x₃ either way.

theorem TauCeti.range_orientationTwoEven_eq_zpowers_neg_one (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 1 < n) (hn' : n ≤ 3) (hv : ↑v * (1 + ↑a) = -1) (ha : a = 0) : (orientationTwoEven a f n v u).range = Subgroup.zpowers (-1)

The image of the standard orientation of the q = 2 normal form with α = 0 on at most three generators is {±1}: for 1 < n ≤ 3, the character with χ(x₂) = -1 and χ(x_i) = 1 otherwise has image {±1}. In rank two, with relator x₁² (x₁, x₂), this is the f = ∞ endpoint V^(∞) of the image table; in rank three the relator is x₁² (x₁, x₂) x₃^{2^f} and the image is the same.

theorem TauCeti.exists_range_orientationTwoEven_eq_zpowers_neg_one (a f n : ℕ) (u : ℤ_[2]ˣ) (hn : 1 < n) (hn' : n ≤ 3) (ha : a = 0) : ∃ (v : ℤ_[2]ˣ), ↑v * (1 + ↑a) = -1 ∧ (orientationTwoEven a f n v u).range = Subgroup.zpowers (-1)

The standard orientation of the q = 2 normal form with α = 0 on at most three generators exists: for 1 < n ≤ 3, in rank two and in rank three alike, there is a unit v with v (1 + a) = -1, and the character with χ(x₂) = v and χ(x_i) = 1 otherwise has image {±1}, whatever the unused marked value u.

theorem TauCeti.exists_range_orientationTwoEven_eq_of_ne_zero (a f n : ℕ) (v u : ℤ_[2]ˣ) (hn : 1 < n) (hn' : n ≤ 3) (hv : ↑v * (1 + ↑a) = -1) (ha₄ : 4 ∣ ↑a) (ha : a ≠ 0) : ∃ (g : ℕ) (w : ℤ_[2]ˣ), 2 ≤ g ∧ 2 ^ g ∣ ↑a ∧ ¬2 ^ (g + 1) ∣ ↑a ∧ ↑w = -1 + 2 ^ g ∧ (orientationTwoEven a f n v u).range = (Subgroup.zpowers w).topologicalClosure

The image of the standard orientation of the q = 2 normal form with 4 ∣ α ≠ 0 on at most three generators is the twisted subgroup U^[g] generated by -1 + 2^g, where g = v₂(α) ≥ 2: for 1 < n ≤ 3, the character with χ(x₂) = -(1 + a)⁻¹ and χ(x_i) = 1 otherwise. The rank-two relator x₁^{2+a} (x₁, x₂) and the rank-three relator x₁^{2+a} (x₁, x₂) x₃^{2^f} give the same image, as the character is trivial on x₃.

theorem TauCeti.exists_unit_range_orientationTwoEven_eq_of_ne_zero (a f n : ℕ) (u : ℤ_[2]ˣ) (hn : 1 < n) (hn' : n ≤ 3) (ha₄ : 4 ∣ ↑a) (ha : a ≠ 0) : ∃ (v : ℤ_[2]ˣ) (g : ℕ) (w : ℤ_[2]ˣ), ↑v * (1 + ↑a) = -1 ∧ 2 ≤ g ∧ 2 ^ g ∣ ↑a ∧ ¬2 ^ (g + 1) ∣ ↑a ∧ ↑w = -1 + 2 ^ g ∧ (orientationTwoEven a f n v u).range = (Subgroup.zpowers w).topologicalClosure

The standard orientation of the q = 2 normal form with 4 ∣ α ≠ 0 on at most three generators exists: for 1 < n ≤ 3, in rank two and in rank three alike, there is a unit v with v (1 + a) = -1, and the character with χ(x₂) = v and χ(x_i) = 1 otherwise has image the twisted subgroup U^[g] generated by -1 + 2^g, where g = v₂(α) ≥ 2, whatever the unused marked value u.

The q = 2 normal form of rank two

noncomputable def TauCeti.orientationTwoRankTwo (a : ℕ) (v : ℤ_[2]ˣ) : presentedProP 2 (Fin 2) {demushkinWordTwoRankTwo a (freeProPGen 2 2)} →ₜ* ℤ_[2]ˣ

The orientation of the rank-two q = 2 normal form with marked value v: the continuous character of the pro-2 group presented on two generators by x₁^{2+a} (x₁, x₂) with χ(x₁) = 1 and χ(x₂) = v. The standard orientation of the classification is the case v = -(1 + a)⁻¹.

Equations

• TauCeti.orientationTwoRankTwo a v = TauCeti.presentedProP.lift (TauCeti.freeProP.lift TauCeti.isProP_units_padicInt_two fun (i : Fin 2) => if ↑i = 1 then v else 1) ⋯

@[simp]

theorem TauCeti.orientationTwoRankTwo_of (a : ℕ) (v : ℤ_[2]ˣ) (i : Fin 2) : (orientationTwoRankTwo a v) (presentedProP.of 2 {demushkinWordTwoRankTwo a (freeProPGen 2 2)} i) = if ↑i = 1 then v else 1

The value of the orientation of the rank-two q = 2 normal form on the generators.

theorem TauCeti.orientationTwoRankTwo_presentedProPGen_zero (a : ℕ) (v : ℤ_[2]ˣ) : (orientationTwoRankTwo a v) (presentedProPGen 2 2 {demushkinWordTwoRankTwo a (freeProPGen 2 2)} 0) = 1

The orientation of the rank-two q = 2 normal form is trivial on x₁.

theorem TauCeti.orientationTwoRankTwo_presentedProPGen_one (a : ℕ) (v : ℤ_[2]ˣ) : (orientationTwoRankTwo a v) (presentedProPGen 2 2 {demushkinWordTwoRankTwo a (freeProPGen 2 2)} 1) = v

The orientation of the rank-two q = 2 normal form takes x₂ to its marked value v.

theorem TauCeti.range_orientationTwoRankTwo (a : ℕ) (v : ℤ_[2]ˣ) : (orientationTwoRankTwo a v).range = (Subgroup.zpowers v).topologicalClosure

The image of the orientation of the rank-two q = 2 normal form is the closed subgroup generated by its marked value v.

theorem TauCeti.range_orientationTwoRankTwo_eq_zpowers_neg_one (a : ℕ) (v : ℤ_[2]ˣ) (hv : ↑v * (1 + ↑a) = -1) (ha : a = 0) : (orientationTwoRankTwo a v).range = Subgroup.zpowers (-1)

The image of the standard orientation of the rank-two q = 2 normal form with α = 0 is {±1}: the character of the group presented by x₁² (x₁, x₂) with χ(x₁) = 1 and χ(x₂) = -1 has image {±1}, the f = ∞ endpoint V^(∞) of the image table.

theorem TauCeti.exists_range_orientationTwoRankTwo_eq_zpowers_neg_one (a : ℕ) (ha : a = 0) : ∃ (v : ℤ_[2]ˣ), ↑v * (1 + ↑a) = -1 ∧ (orientationTwoRankTwo a v).range = Subgroup.zpowers (-1)

The standard orientation of the rank-two q = 2 normal form with α = 0 exists: there is a unit v with v (1 + a) = -1, and the character with χ(x₁) = 1 and χ(x₂) = v has image {±1}.

theorem TauCeti.exists_range_orientationTwoRankTwo_eq_of_ne_zero (a : ℕ) (v : ℤ_[2]ˣ) (hv : ↑v * (1 + ↑a) = -1) (ha₄ : 4 ∣ ↑a) (ha : a ≠ 0) : ∃ (g : ℕ) (w : ℤ_[2]ˣ), 2 ≤ g ∧ 2 ^ g ∣ ↑a ∧ ¬2 ^ (g + 1) ∣ ↑a ∧ ↑w = -1 + 2 ^ g ∧ (orientationTwoRankTwo a v).range = (Subgroup.zpowers w).topologicalClosure

The image of the standard orientation of the rank-two q = 2 normal form with 4 ∣ α ≠ 0 is the twisted subgroup U^[g] generated by -1 + 2^g, where g = v₂(α) ≥ 2: the character of the group presented by x₁^{2+a} (x₁, x₂) with χ(x₁) = 1 and χ(x₂) = -(1 + a)⁻¹.

theorem TauCeti.exists_unit_range_orientationTwoRankTwo_eq_of_ne_zero (a : ℕ) (ha₄ : 4 ∣ ↑a) (ha : a ≠ 0) : ∃ (v : ℤ_[2]ˣ) (g : ℕ) (w : ℤ_[2]ˣ), ↑v * (1 + ↑a) = -1 ∧ 2 ≤ g ∧ 2 ^ g ∣ ↑a ∧ ¬2 ^ (g + 1) ∣ ↑a ∧ ↑w = -1 + 2 ^ g ∧ (orientationTwoRankTwo a v).range = (Subgroup.zpowers w).topologicalClosure

The standard orientation of the rank-two q = 2 normal form with 4 ∣ α ≠ 0 exists: there is a unit v with v (1 + a) = -1, and the character with χ(x₁) = 1 and χ(x₂) = v has image the twisted subgroup U^[g] generated by -1 + 2^g, where g = v₂(α) ≥ 2.