Proposition 1.1 infrastructure: ℤ₂ is pro-2, and ν_ur descends

Proposition 1.1 (GQ2.SectionThree.prop_1_1) reads the unramified coordinates ν_ur(a,s,y) = (−2,1,0) of the marked generators through arbitrary lifts to G_{ℚ₂}. For that reading to be well-defined the coordinate ν_ur ∘ toAb : G_{ℚ₂} → ℤ₂ must be constant on the fibres of the maximal pro-2 quotient maxProPMk 2 G_{ℚ₂} — i.e. it must factor through G_{ℚ₂}(2).

This file supplies that descent. Its engine is:

• isProP_two_multPadicInt : IsProP 2 (Multiplicative ℤ₂) — the target of ν_ur is a pro-2 group. Proof: every open subgroup of ℤ₂ contains 2ⁿℤ₂ = span{2ⁿ} for some n (the span{2ⁿ} are a 0-neighbourhood basis, PadicInt.norm_le_pow_iff_mem_span_pow), so 2ⁿ uniformly annihilates every finite quotient — a 2-group.
• nu_ur_descends : ν_ur ∘ toAb factors through maxProPMk 2 G_{ℚ₂}, via the universal property of the maximal pro-2 quotient (proPKernel_le_ker for the pro-2 target above).

The full proposition is assembled in GQ2/PropOneOneAssembly.lean from this descent, Lemma 3.5's marked abelianization, and Proposition 3.8's automorphism lift. Keeping the descent isolated here also makes its dependence on the maximal pro-2 universal property explicit.

theorem GQ2.PropOneOne.exists_span_pow_subset {S : Set ℤ_[2]} (hopen : IsOpen S) (hmem : 0 ∈ S) : ∃ (n : ℕ), ↑(Ideal.span {2 ^ n}) ⊆ S

The span{2ⁿ} are a neighbourhood basis of 0 in ℤ₂: every open set containing 0 contains span{2ⁿ} for some n.

theorem GQ2.PropOneOne.isProP_two_multPadicInt : IsProP 2 (Multiplicative ℤ_[2])

ℤ₂ is a pro-2 group (multiplicatively): every finite continuous quotient of Multiplicative ℤ₂ is a 2-group.

The ν_ur-descent through the maximal pro-2 quotient

noncomputable def GQ2.PropOneOne.nuUrComp (R : LocalReciprocity) : AbsGalQ2 →ₜ* Multiplicative ℤ_[2]

ν_ur ∘ toAb : G_{ℚ₂} → ℤ₂ as a continuous homomorphism.

Equations

• GQ2.PropOneOne.nuUrComp R = { toFun := fun (g : GQ2.AbsGalQ2) => R.nu_ur (GQ2.toAb g), map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

noncomputable def GQ2.PropOneOne.nuUrBar (R : LocalReciprocity) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] : ↑(maxProPQuotient 2 AbsGalQ2).toProfinite.toTop →ₜ* Multiplicative ℤ_[2]

ν_ur descends through the maximal pro-2 quotient. Since ℤ₂ is pro-2 (isProP_two_multPadicInt), the continuous hom ν_ur ∘ toAb : G_{ℚ₂} → ℤ₂ factors through G_{ℚ₂}(2) = maxProPQuotient 2 G_{ℚ₂} (universal property maxProPHomEquiv): there is a continuous ν̄ with ν̄ (maxProPMk g) = ν_ur (toAb g). This is the well-definedness Prop. 1.1's ν_ur-rows require (they read ν_ur(toAb g) off maxProPMk g).

Equations

• GQ2.PropOneOne.nuUrBar R = (GQ2.maxProPHomEquiv GQ2.PropOneOne.isProP_two_multPadicInt).symm (GQ2.PropOneOne.nuUrComp R)

@[simp]

theorem GQ2.PropOneOne.nuUrBar_maxProPMk (R : LocalReciprocity) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (g : AbsGalQ2) : (nuUrBar R) ((maxProPMk 2 AbsGalQ2) g) = R.nu_ur (toAb g)

theorem GQ2.PropOneOne.nu_ur_toAb_eq_of_maxProPMk_eq (R : LocalReciprocity) [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] {g₁ g₂ : AbsGalQ2} (h : (maxProPMk 2 AbsGalQ2) g₁ = (maxProPMk 2 AbsGalQ2) g₂) : R.nu_ur (toAb g₁) = R.nu_ur (toAb g₂)

ν_ur ∘ toAb is constant on the fibres of maxProPMk — the exact fact Prop. 1.1's ν_ur-rows consume (all lifts g of a fixed maxProP-class have the same ν_ur(toAb g)).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Lemma 3.5 = ⟦lem-markedinitialform⟧
• Prop 1.1 = ⟦prop-markedDem⟧
• Prop 3.8 = ⟦prop-orientationlift⟧ (= proposition 3.9 in current tex)