The unramified character ν_ur : D₀ ⟶ ℤ₂ and the global Demushkin relator

(Stage: Local)

This file equips the profinite Demushkin group D₀ (Boundary/D0.lean) with the two pieces of internal data needed to assemble the marked dyadic Demushkin normalization MarkedDemushkinQ2 (Local/MarkedDemushkin.lean), both proved sorry-free:

• d0_globalRel : d0A ^ 2 * d0S ^ 4 * commutatorW d0S d0Y = 1 — the single defining Demushkin relator, holding globally in D₀ (not merely coordinatewise as in D0_rel). Obtained from D0_rel/D0_ext by pushing the genuine monoid hom θ_X = d0EvalAt X ∘ d0Iso.hom through the word.

• nu_ur : D₀ ⟶ ℤ₂, the unramified character with the full marks ν_ur(a, s, y) = (-2, 1, 0) (manuscript Prop markedDem, eq:markedstandardhyp; here s is the geometric-Frobenius lift ↦ 1, a ↦ -2, y ↦ 0). This is the exact analogue of nu_2 : PiGrp ⟶ ℤ₂ (Boundary/PiGroup.lean) and nu_t : Ttame ⟶ ℤ₂ (Boundary/Ttame.lean): it is built as the map into ℤ₂ = lim_n ZMod(2ⁿ) whose n-th layer projects D₀ through an auxiliary cyclic Demushkin 2-group quotient cyclicD0 n (carrier C2Pow n, marks a = ofAdd(-2), s = ofAdd 1, y = 1). The marks (-2, 1, 0) are exactly consistent with the abelianized relator 2·(-2) + 4·1 = 0, so such a character exists.

Note that this nu_ur is some character realizing the marks; it is not pinned to the genuine unramified character of G_{ℚ₂} (the interface does not require that — see Local/LabuteClassification.lean).

Instance gotcha (inherited from Boundary/D0.lean, Boundary/PiGroup.lean)

Fin n carries the global Fin.instMul, not the transported groupFin. We thread groupFin explicitly (@, letI) through every Fin-level construction so Fin.instMul is never synthesized.

The missing d0SkelHomBetween_key (mirrors piSkelHomBetween_key)

theorem Q2Presentation.d0SkelHomBetween_key {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Nonempty G] [Group H] [Finite H] [Nonempty H] {aG sG yG : G} {hgG : Gen3 aG sG yG} {hrG : D0Relator aG sG yG} {hpG : IsPGroup 2 G} {aH sH yH : H} {hgH : Gen3 aH sH yH} {hrH : D0Relator aH sH yH} {hpH : IsPGroup 2 H} (φ : G →* H) (ha : φ aG = aH) (hs : φ sG = sH) (hy : φ yG = yH) (z : Fin (d0Skeletalize G aG sG yG hgG hrG hpG).n) : (d0SkelEquiv H aH sH yH hgH hrH hpH) ((d0SkelHomBetween φ ha hs hy).toMonoidHom z) = φ ((d0SkelEquiv G aG sG yG hgG hrG hpG) z)

The induced morphism intertwines the transport equivalences with φ. (The D₀ analogue of piSkelHomBetween_key, absent from Boundary/D0.lean.)

The global Demushkin relator in D₀

theorem Q2Presentation.d0_globalRel : d0A ^ 2 * d0S ^ 4 * commutatorW d0S d0Y = 1

The Demushkin relation holds globally in D₀ (manuscript a² s⁴ [s,y] = 1, eq:markedstandardhyp). Strengthens the coordinatewise D0_rel to the genuine group identity in D₀, by pushing the monoid hom θ_X = d0EvalAt X ∘ d0Iso.hom through the relator word and applying X.rel.

The unramified character ν_ur : D₀ ⟶ ℤ₂

The unramified character sends s to the topological generator 1 ∈ ℤ₂, a to -2, and y to 0. It is built as the map into ℤ₂ = lim_n ZMod(2ⁿ) whose n-th layer is the projection of D₀ through the auxiliary cyclic Demushkin 2-group quotient cyclicD0 n (carrier C2Pow n, a = ofAdd(-2), s = ofAdd 1, y = 1).

theorem Q2Presentation.cyclicD0_gen (n : ℕ) : Gen3 (Multiplicative.ofAdd ↑(-2)) (Multiplicative.ofAdd 1) 1

The additive generator ofAdd 1 (the middle mark s) generates the cyclic 2-group C2Pow n.

theorem Q2Presentation.cyclicD0_rel (n : ℕ) : D0Relator (Multiplicative.ofAdd ↑(-2)) (Multiplicative.ofAdd 1) 1

The Demushkin relation holds in C2Pow n with the marks a = ofAdd(-2), s = ofAdd 1, y = 1: additively 2·(-2) + 4·1 = 0, and the commutator is trivial (C2Pow n is abelian).

theorem Q2Presentation.cyclicD0_isTwoGroup (n : ℕ) : IsPGroup 2 (C2Pow n)

C2Pow n is a 2-group.

noncomputable def Q2Presentation.cyclicD0 (n : ℕ) : D0MarkedFinite

The auxiliary cyclic Demushkin 2-group quotient at layer n: carrier C2Pow n, marks a = ofAdd(-2), s = ofAdd 1, y = 1.

Equations

• Q2Presentation.cyclicD0 n = Q2Presentation.d0Skeletalize (Q2Presentation.C2Pow n) (Multiplicative.ofAdd ↑(-2)) (Multiplicative.ofAdd 1) 1 ⋯ ⋯ ⋯

noncomputable def Q2Presentation.cyclicD0Equiv (n : ℕ) : Fin (cyclicD0 n).n ≃* C2Pow n

The transport equivalence Fin (cyclicD0 n).n ≃* C2Pow n.

Equations

• Q2Presentation.cyclicD0Equiv n = Q2Presentation.d0SkelEquiv (Q2Presentation.C2Pow n) (Multiplicative.ofAdd ↑(-2)) (Multiplicative.ofAdd 1) 1 ⋯ ⋯ ⋯

@[simp]

theorem Q2Presentation.cyclicD0Equiv_a (n : ℕ) : (cyclicD0Equiv n) (cyclicD0 n).a = Multiplicative.ofAdd ↑(-2)

@[simp]

theorem Q2Presentation.cyclicD0Equiv_s (n : ℕ) : (cyclicD0Equiv n) (cyclicD0 n).s = Multiplicative.ofAdd 1

@[simp]

theorem Q2Presentation.cyclicD0Equiv_y (n : ℕ) : (cyclicD0Equiv n) (cyclicD0 n).y = 1

theorem Q2Presentation.castCMH_ofAddOne {a b : ℕ} (h : 2 ^ a ∣ 2 ^ b) : (castCMH h) (Multiplicative.ofAdd 1) = Multiplicative.ofAdd 1

Reduction maps fix the additive generator ofAdd 1 (the s-mark).

theorem Q2Presentation.castCMH_ofAdd_intCast {a b : ℕ} (k : ℤ) (h : 2 ^ a ∣ 2 ^ b) : (castCMH h) (Multiplicative.ofAdd ↑k) = Multiplicative.ofAdd ↑k

Reduction maps commute with the ℤ-cast marks (here the a-mark ofAdd(-2)).

noncomputable def Q2Presentation.d0LayerHom (n : ℕ) : ↑D0.toProfinite.toTop →* C2Pow n

The n-th unramified layer hom D₀ →* C2Pow n: project to the auxiliary cyclic quotient cyclicD0 n and read off the additive coordinate.

Equations

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

theorem Q2Presentation.d0Layer_continuous (n : ℕ) : Continuous ⇑(d0LayerHom n)

noncomputable def Q2Presentation.redHomD0 (n m : ℕ) (hmn : m ≤ n) : cyclicD0 n ⟶ cyclicD0 m

The reduction D₀ morphism cyclicD0 n ⟶ cyclicD0 m for m ≤ n, underlying the ℤ₂-layer maps ZMod(2ⁿ) → ZMod(2ᵐ).

Equations

• Q2Presentation.redHomD0 n m hmn = Q2Presentation.d0SkelHomBetween (Q2Presentation.castCMH ⋯).toMonoidHom ⋯ ⋯ ⋯

theorem Q2Presentation.redHomD0_key (n m : ℕ) (hmn : m ≤ n) (z : Fin (cyclicD0 n).n) : (cyclicD0Equiv m) ((redHomD0 n m hmn).toMonoidHom z) = (castCMH ⋯) ((cyclicD0Equiv n) z)

The reduction morphism intertwines the transport equivalences with the ℤ₂-layer reduction.

theorem Q2Presentation.d0Layer_compat (n m : ℕ) (hmn : m ≤ n) (x : ↑D0.toProfinite.toTop) : (castCMH ⋯) ((d0LayerHom n) x) = (d0LayerHom m) x

Layer compatibility: reducing the n-th layer to the m-th agrees with the m-th layer (m ≤ n). Uses the inverse-limit compatibility of D₀ through redHomD0.

noncomputable def Q2Presentation.nu_ur : D0 ⟶ ProfiniteZ2

The unramified character ν_ur : D₀ ⟶ ℤ₂, a ↦ -2, s ↦ 1, y ↦ 0. Built as the map into ℤ₂ = lim_n ZMod(2ⁿ) whose n-th coordinate is d0LayerHom n.

Equations

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

ν_ur realizes the marks (a, s, y) ↦ (-2, 1, 0)

theorem Q2Presentation.d0LayerHom_d0A (n : ℕ) : (d0LayerHom n) d0A = Multiplicative.ofAdd ↑(-2)

theorem Q2Presentation.d0LayerHom_d0S (n : ℕ) : (d0LayerHom n) d0S = Multiplicative.ofAdd 1

theorem Q2Presentation.d0LayerHom_d0Y (n : ℕ) : (d0LayerHom n) d0Y = 1

theorem Q2Presentation.nu_ur_d0A : (ProfiniteGrp.Hom.hom nu_ur) d0A = z2NegTwo

ν_ur sends a to -2 ∈ ℤ₂.

theorem Q2Presentation.nu_ur_d0S : (ProfiniteGrp.Hom.hom nu_ur) d0S = z2One

ν_ur sends s to the topological generator 1 ∈ ℤ₂ (the unramified Frobenius coordinate).

theorem Q2Presentation.nu_ur_d0Y : (ProfiniteGrp.Hom.hom nu_ur) d0Y = z2Zero

ν_ur sends y to 0 ∈ ℤ₂.