Labute's normal forms modulo λ_2

Let F = freeProP p (Fin n) be the free pro-p group on n generators x₁, …, x_n, let gr_1(F) = λ_1(F) ⧸ λ_2(F) be the degree-one piece of its lower p-series, and let ρ ∈ gr_1(F) be a class whose degree-one form TauCeti.freeProP.degreeOneForm ρ — the bilinear form on the continuous 𝔽_p-dual of F whose matrix carries the commutator coordinates of ρ off the diagonal and (p choose 2) times its p-power coordinates on it — is nondegenerate. For the class of a relator r this is the form Labute reads off r to describe the cup product on H¹(F ⧸ ⟪r⟫, 𝔽_p) (Labute, Proposition 3); that identification is not made here. This file proves Labute's normal forms for such a class modulo λ_2: a continuous automorphism of F carries ρ to the class of one of the normal-form relator words,

• (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) or x₁^p (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n), and then n is even, when the form is alternating, which is automatic for odd p (TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordNeTwo); at p = 2 only the first word occurs (exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordNeTwo_zero_of_two);
• x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n), which is x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) modulo λ_2, when p = 2, the form is not alternating and n is odd (TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoOdd, and TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoOddTop for the word at f = ∞ itself);
• x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), which is x₁² (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) modulo λ_2, when p = 2, the form is not alternating and n is even (TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoEven).

The route follows Labute. Every basis of the continuous dual is realized by a continuous automorphism of F (TauCeti.freeProP.exists_continuousMulEquiv_continuousZModDualMap_eq), so the normal forms of bilinear forms apply. In the alternating case a symplectic basis, interleaved so that the hyperbolic pairs become the pairs (x_{2a+1}, x_{2a+2}), brings the commutator coordinates into the shape (x₁, x₂)(x₃, x₄) ⋯. The p-power coordinates are invisible to the form for odd p; they define a functional ℓ on the dual, and if ℓ ≠ 0 the symplectic basis is chosen through a hyperbolic pair (θ, e₀) with θ representing ℓ, so that ℓ vanishes on every basis vector but e₀, and the p-power part becomes exactly π ξ₁. When the p-power part is concentrated on the first generator x₁, the same choice with θ representing evaluation at x₁ makes e₀ take the value 1 at x₁ while every other basis vector vanishes at x₁, and the automorphism can then be taken to fix x₁; for a relator with exponent vector q e₁ this keeps the exponent vector, which is what the successive approximation of the relators with q ≠ p needs. In the nonalternating case, which occurs only at p = 2, the form is symmetric and any two nondegenerate symmetric nonalternating forms of the same dimension are equivalent, while at p = 2 the form determines the class; it therefore suffices to check that the forms of the two dyadic normal-form words are nondegenerate and not alternating, which is a direct computation.

Main results

• TauCeti.freeProP.degreeOneBasis_repr_gradedMk_demushkinWordNeTwo_inl: the p-power coordinates of the class of x₁^q (x₁, x₂) ⋯ are q / p at x₁ and 0 elsewhere.
• TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordNeTwo: the alternating case, for every p.
• TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordNeTwo: the degree-one form of the normal-form word x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) is nondegenerate for n even and every q divisible by p (at p = 2 this includes q ≡ 2 mod 4, where the form is not alternating).
• TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordTwoOdd, TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordTwoEven: the degree-one forms of the two dyadic normal-form words are nondegenerate, for n odd, resp. even, for every f ≥ 1 and every even a; under the normal-form bounds f ≥ 2 and 4 ∣ a they are moreover not alternating (TauCeti.freeProP.not_isAlt_degreeOneForm_demushkinWordTwoOdd, TauCeti.freeProP.not_isAlt_degreeOneForm_demushkinWordTwoEven); TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordTwoOddTop and TauCeti.freeProP.not_isAlt_degreeOneForm_demushkinWordTwoOddTop: the same for the odd word at f = ∞, which has the class of the odd word at f = 2.
• TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_of_not_isAlt: at p = 2, two classes with nondegenerate nonalternating degree-one forms are carried to one another by a continuous automorphism.
• TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordNeTwo_zero_of_two: the alternating case at p = 2, where the p-power part vanishes.
• exists_continuousMulEquiv_freeProPGen_zero_eq_gradedMap_eq_gradedMk_demushkinWordNeTwo and exists_continuousMulEquiv_freeProPGen_zero_eq_inv_mul_demushkinWordNeTwo_mem (in TauCeti.freeProP): the alternating case with the p-power part concentrated on x₁, by an automorphism fixing x₁; for a class, and for a relator with exponent vector q e₁.
• TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoOdd, TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoOddTop, TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoEven: the nonalternating case at p = 2, of odd and of even rank.

References

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

Interleaving a symplectic basis

The two alternating normal forms

@[simp]

theorem TauCeti.freeProP.degreeOneBasis_repr_gradedMk_demushkinWordNeTwo_inl {p : ℕ} [Fact (Nat.Prime p)] {n q : ℕ} (hq : p ∣ q) (k : Fin n) : ((degreeOneBasis p (Fin n)).repr (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩)) (Sum.inl k) = if ↑k = 0 then ↑(q / p) else 0

The p-power coordinates of the class of the q ≠ 2 normal-form word x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n), for p ∣ q: the coefficient of π ξ₁ is q / p, and the other p-power coordinates vanish.

theorem TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (ρ : gradedPiece p (freeProP p (Fin n)) 1) (hnd : (degreeOneForm ρ).Nondegenerate) (halt : (degreeOneForm ρ).IsAlt) : Even n ∧ ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), (gradedMap p (↑e).toMonoidHom ⋯ 1) ρ = gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo 0 n (freeProPGen p n), ⋯⟩ ∨ (gradedMap p (↑e).toMonoidHom ⋯ 1) ρ = gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo p n (freeProPGen p n), ⋯⟩

Labute's normal form modulo λ_2, the alternating case. Let F be the free pro-p group on n generators and let ρ ∈ gr_1(F) have nondegenerate alternating degree-one form, which for odd p is every nondegenerate form. Then n is even, and a continuous automorphism of F carries ρ to the class of (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) or to the class of x₁^p (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n). For a relator r with class ρ, this is r ≡ x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) mod λ_2(F) after a change of basis, with q = 0 or q = p; every q with p² ∣ q gives the same class as q = 0.

theorem TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordNeTwo_zero_of_two {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hp : p = 2) (ρ : gradedPiece p (freeProP p (Fin n)) 1) (hnd : (degreeOneForm ρ).Nondegenerate) (halt : (degreeOneForm ρ).IsAlt) : Even n ∧ ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), (gradedMap p (↑e).toMonoidHom ⋯ 1) ρ = gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo 0 n (freeProPGen p n), ⋯⟩

Labute's normal form modulo λ_2, the alternating case at p = 2. At p = 2 the diagonal of the degree-one form consists of the 2-power coordinates, so an alternating form has no 2-power part and only the first alternative occurs: a continuous automorphism carries ρ to the class of (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_freeProPGen_zero_eq_gradedMap_eq_gradedMk_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (ρ : gradedPiece p (freeProP p (Fin n)) 1) (hnd : (degreeOneForm ρ).Nondegenerate) (halt : (degreeOneForm ρ).IsAlt) {q : ℕ} (hq : p ∣ q) (hc : ∀ (k : Fin n), ((degreeOneBasis p (Fin n)).repr ρ) (Sum.inl k) = if ↑k = 0 then ↑(q / p) else 0) : Even n ∧ ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), e (freeProPGen p n 0) = freeProPGen p n 0 ∧ (gradedMap p (↑e).toMonoidHom ⋯ 1) ρ = gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩

Labute's normal form modulo λ_2, the alternating case, fixing the first generator. Let ρ ∈ gr_1(F) have nondegenerate alternating degree-one form and p-power part (q / p) • π ξ₁ concentrated on the first generator, for some q divisible by p. Then n is even, and a continuous automorphism of F fixing x₁ carries ρ to the class of x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_freeProPGen_zero_eq_inv_mul_demushkinWordNeTwo_mem {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (r : ↥(pLowerCentralSeries p (freeProP p (Fin n)) 1)) (hnd : (degreeOneForm (gradedMk p (freeProP p (Fin n)) 1 r)).Nondegenerate) (halt : (degreeOneForm (gradedMk p (freeProP p (Fin n)) 1 r)).IsAlt) {q : ℕ} (hq : p ∣ q) (hv : ∀ (k : Fin n), Multiplicative.toAdd ((exponentSum p (Fin n)) ↑r) k = if ↑k = 0 then ↑q else 0) : Even n ∧ ∃ (e : freeProP p (Fin n) ≃ₜ* freeProP p (Fin n)), e (freeProPGen p n 0) = freeProPGen p n 0 ∧ (e ↑r)⁻¹ * demushkinWordNeTwo q n (freeProPGen p n) ∈ pLowerCentralSeries p (freeProP p (Fin n)) 2

Labute's normal form modulo λ_2 for a relator with exponent vector q e₁, fixing the first generator. Let r ∈ λ_1(F) have nondegenerate alternating degree-one form and exponent sums q at x₁ and 0 at the other generators, for some q divisible by p. Then n is even, and a continuous automorphism of F fixing x₁ carries r to x₁^q (x₁, x₂)(x₃, x₄) ⋯ (x_{n-1}, x_n) modulo λ_2(F). The image of r has the same exponent sums as r, so this is the first step of the successive approximation of a relator with q ≠ p, whose later steps must keep the exponent sums fixed.

The normal form x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) is nondegenerate

theorem TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordNeTwo {p : ℕ} [Fact (Nat.Prime p)] {n : ℕ} (hn : Even n) {q : ℕ} (hq : p ∣ q) : (degreeOneForm (gradedMk p (freeProP p (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen p n), ⋯⟩)).Nondegenerate

The degree-one form of x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) is nondegenerate for n even and p ∣ q: pairing with the j-th coordinate character reads off the value of a character at the partner x_{j±1} of x_j in the commutator pairs, up to the p-power term, which involves only the value at x₁ and is read off first. This covers q = 0, and at p = 2 also q ≡ 2 mod 4, where the form is not alternating.

The dyadic nonalternating normal forms

theorem TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_of_not_isAlt {n : ℕ} (ρ T : gradedPiece 2 (freeProP 2 (Fin n)) 1) (hnd : (degreeOneForm ρ).Nondegenerate) (hnalt : ¬(degreeOneForm ρ).IsAlt) (hTnd : (degreeOneForm T).Nondegenerate) (hTnalt : ¬(degreeOneForm T).IsAlt) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), (gradedMap 2 (↑e).toMonoidHom ⋯ 1) ρ = T

At p = 2 the classes with nondegenerate nonalternating degree-one form form a single orbit: two such classes are carried to one another by a continuous automorphism of F. Such forms are symmetric, any two of them on spaces of the same dimension are equivalent, and at p = 2 the form determines the class.

@[simp]

theorem TauCeti.freeProP.degreeOneBasis_repr_gradedMk_demushkinWordTwoOdd_inl {n f : ℕ} (hf : 0 < f) (k : Fin n) : ((degreeOneBasis 2 (Fin n)).repr (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOdd f n (freeProPGen 2 n), ⋯⟩)) (Sum.inl k) = (if ↑k = 0 then 1 else 0) + 2 ^ (f - 1) • if ↑k = 1 then 1 else 0

The 2-power coordinates of the class of the q = 2, n odd normal-form word x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n), for f ≥ 1: the coefficient of π ξ₁ is 1, that of π ξ₂ is 2^{f-1}, and the other 2-power coordinates vanish.

theorem TauCeti.freeProP.degreeOneBasis_repr_gradedMk_demushkinWordTwoOdd_inl_eq_zero_iff {n f : ℕ} (hf : 2 ≤ f) (k : Fin n) : ((degreeOneBasis 2 (Fin n)).repr (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOdd f n (freeProPGen 2 n), ⋯⟩)) (Sum.inl k) = 0 ↔ ↑k ≠ 0

The vanishing 2-power coordinates of the odd dyadic normal-form word, for f ≥ 2: all coordinates except that of x₁ vanish.

theorem TauCeti.freeProP.not_isAlt_degreeOneForm_demushkinWordTwoOdd {n : ℕ} (hn : 0 < n) {f : ℕ} (hf : 0 < f) : ¬(degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOdd f n (freeProPGen 2 n), ⋯⟩)).IsAlt

The degree-one form of x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) is not alternating, for n ≥ 1 and f ≥ 1: its value on the first coordinate character twice is 1.

theorem TauCeti.freeProP.degreeOneForm_gradedMk_demushkinWordTwoOdd_dualBasis_zero {n : ℕ} (hn : 0 < n) {f : ℕ} (hf : 0 < f) (χ : continuousZModDual 2 (freeProP 2 (Fin n))) : ((degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOdd f n (freeProPGen 2 n), ⋯⟩)) χ) ((dualBasis 2 (Fin n)) ⟨0, hn⟩) = Multiplicative.toAdd ((Additive.toMul χ) (freeProPGen 2 n 0))

The first coordinate character splits off the degree-one form of x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n), for n ≥ 1 and f ≥ 1: pairing any character χ with the first coordinate character reads off χ(x₁), because x₁ occurs in no commutator of the word. In particular the first coordinate character is orthogonal to all the others.

theorem TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordTwoOdd {n : ℕ} (hn : Odd n) {f : ℕ} (hf : 0 < f) : (degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOdd f n (freeProPGen 2 n), ⋯⟩)).Nondegenerate

The degree-one form of x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n) is nondegenerate for n odd and f ≥ 1: pairing with the j-th coordinate character reads off the value of a character at x₁ for j = 1, and at the partner x_{j±1} of x_j in the commutator pairs otherwise (for j = 2 up to the diagonal term 2^{f-1} • χ(x₂), which vanishes once the value at x₂ is read off from j = 3).

@[simp]

theorem TauCeti.freeProP.degreeOneBasis_repr_gradedMk_demushkinWordTwoEven_inl {n a f : ℕ} (ha : 2 ∣ a) (hf : 0 < f) (k : Fin n) : ((degreeOneBasis 2 (Fin n)).repr (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven a f n (freeProPGen 2 n), ⋯⟩)) (Sum.inl k) = ((1 + a / 2) • if ↑k = 0 then 1 else 0) + 2 ^ (f - 1) • if ↑k = 2 then 1 else 0

The 2-power coordinates of the class of the q = 2, n even normal-form word x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), for a even and f ≥ 1: the coefficient of π ξ₁ is 1 + a/2, that of π ξ₃ is 2^{f-1}, and the other 2-power coordinates vanish.

theorem TauCeti.freeProP.not_isAlt_degreeOneForm_demushkinWordTwoEven {n : ℕ} (hn : 0 < n) {a f : ℕ} (ha : 4 ∣ a) (hf : 2 ≤ f) : ¬(degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven a f n (freeProPGen 2 n), ⋯⟩)).IsAlt

The degree-one form of x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) is not alternating, for n ≥ 1, 4 ∣ a and f ≥ 2: its value on the first coordinate character twice is 1. (For a ≡ 2 mod 4 and f ≥ 2 the form is alternating.)

theorem TauCeti.freeProP.not_isAlt_degreeOneForm_demushkinWordNeTwo {n : ℕ} (hn : 0 < n) {q : ℕ} (hq : q % 4 = 2) : ¬(degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordNeTwo q n (freeProPGen 2 n), ⋯⟩)).IsAlt

The degree-one form of x₁^q (x₁, x₂) ⋯ (x_{n-1}, x_n) is not alternating at p = 2, for n ≥ 1 and q ≡ 2 mod 4: its value on the first coordinate character twice is q / 2 ≡ 1. This covers the relators x₁^{2 + 2^f} (x₁, x₂) ⋯ with f ≥ 2 and x₁² (x₁, x₂) ⋯.

theorem TauCeti.freeProP.degreeOneForm_gradedMk_demushkinWordTwoEven_dualBasis_one {n : ℕ} (hn : 1 < n) {a f : ℕ} (ha : 2 ∣ a) (hf : 0 < f) (χ : continuousZModDual 2 (freeProP 2 (Fin n))) : ((degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven a f n (freeProPGen 2 n), ⋯⟩)) χ) ((dualBasis 2 (Fin n)) ⟨1, hn⟩) = Multiplicative.toAdd ((Additive.toMul χ) (freeProPGen 2 n 0))

The second coordinate character pairs only with the first under the degree-one form of x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), for n ≥ 2, a even and f ≥ 1: pairing any character χ with the second coordinate character reads off χ(x₁), because x₂ occurs only in the commutator (x₁, x₂). In particular the second coordinate character is orthogonal to every coordinate character other than the first.

theorem TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordTwoEven {n : ℕ} (hn : Even n) {a f : ℕ} (ha : 2 ∣ a) (hf : 0 < f) : (degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven a f n (freeProPGen 2 n), ⋯⟩)).Nondegenerate

The degree-one form of x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n) is nondegenerate for n even, a even and f ≥ 1: pairing with the second coordinate character reads off the value of a character at x₁, pairing with the first one then reads off its value at x₂, and the remaining coordinate characters read off the values at the partners in the commutator pairs (for j = 3 up to the diagonal term 2^{f-1} • χ(x₃), which vanishes once the value at x₃ is read off from j = 4).

theorem TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoOdd {n : ℕ} (ρ : gradedPiece 2 (freeProP 2 (Fin n)) 1) (hnd : (degreeOneForm ρ).Nondegenerate) (hnalt : ¬(degreeOneForm ρ).IsAlt) (hn : Odd n) {f : ℕ} (hf : 2 ≤ f) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), (gradedMap 2 (↑e).toMonoidHom ⋯ 1) ρ = gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOdd f n (freeProPGen 2 n), ⋯⟩

Labute's normal form modulo λ_2, the nonalternating case of odd rank. Let F be the free pro-2 group on n generators, n odd, and let ρ ∈ gr_1(F) have nondegenerate degree-one form that is not alternating. Then for every f ≥ 2 a continuous automorphism of F carries ρ to the class of x₁² x₂^{2^f} (x₂, x₃) ⋯ (x_{n-1}, x_n), which is the class of x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.not_isAlt_degreeOneForm_demushkinWordTwoOddTop {n : ℕ} (hn : 0 < n) : ¬(degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOddTop n (freeProPGen 2 n), ⋯⟩)).IsAlt

The degree-one form of x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) is not alternating, for n ≥ 1: the word has the class of x₁² x₂⁴ (x₂, x₃) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.nondegenerate_degreeOneForm_demushkinWordTwoOddTop {n : ℕ} (hn : Odd n) : (degreeOneForm (gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOddTop n (freeProPGen 2 n), ⋯⟩)).Nondegenerate

The degree-one form of x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n) is nondegenerate for n odd: the word has the class of x₁² x₂⁴ (x₂, x₃) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoOddTop {n : ℕ} (ρ : gradedPiece 2 (freeProP 2 (Fin n)) 1) (hnd : (degreeOneForm ρ).Nondegenerate) (hnalt : ¬(degreeOneForm ρ).IsAlt) (hn : Odd n) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), (gradedMap 2 (↑e).toMonoidHom ⋯ 1) ρ = gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoOddTop n (freeProPGen 2 n), ⋯⟩

Labute's normal form modulo λ_2, the nonalternating case of odd rank, at level f = ∞. Let F be the free pro-2 group on n generators, n odd, and let ρ ∈ gr_1(F) have nondegenerate degree-one form that is not alternating. Then a continuous automorphism of F carries ρ to the class of x₁² (x₂, x₃) ⋯ (x_{n-1}, x_n).

theorem TauCeti.freeProP.exists_continuousMulEquiv_gradedMap_eq_gradedMk_demushkinWordTwoEven {n : ℕ} (ρ : gradedPiece 2 (freeProP 2 (Fin n)) 1) (hnd : (degreeOneForm ρ).Nondegenerate) (hnalt : ¬(degreeOneForm ρ).IsAlt) (hn : Even n) {a f : ℕ} (ha : 4 ∣ a) (hf : 2 ≤ f) : ∃ (e : freeProP 2 (Fin n) ≃ₜ* freeProP 2 (Fin n)), (gradedMap 2 (↑e).toMonoidHom ⋯ 1) ρ = gradedMk 2 (freeProP 2 (Fin n)) 1 ⟨demushkinWordTwoEven a f n (freeProPGen 2 n), ⋯⟩

Labute's normal form modulo λ_2, the nonalternating case of even rank. Let F be the free pro-2 group on n generators, n even, and let ρ ∈ gr_1(F) have nondegenerate degree-one form that is not alternating. Then for every a divisible by 4 and every f ≥ 2 a continuous automorphism of F carries ρ to the class of x₁^{2+a} (x₁, x₂) x₃^{2^f} (x₃, x₄) ⋯ (x_{n-1}, x_n), which is the class of x₁² (x₁, x₂) (x₃, x₄) ⋯ (x_{n-1}, x_n).