Documentation

Q2Presentation.Boundary.D0PiIso

The profinite Nielsen comparison D₀ ≅ Π (Stage C, work order C4) #

This file assembles the genuine profinite Nielsen isomorphism D₀ ≅ Π (manuscript reference/q2_manuscript.tex, Corollary 3.12 cor:relativeDemushkin, building on Proposition 3.11 prop:abstractDemushkin, l.~998–1035) from the finite-quotient category equivalence D0_Pi_index_equiv : D0MarkedFinite ≌ PiMarkedFinite (Boundary/Nielsen.lean) together with limit-invariance under an equivalence of the (cofiltered) index categories.

Method #

The Nielsen functor D0_to_Pi : D0MarkedFinite ⥤ PiMarkedFinite remarks the same underlying finite group: (D0_to_Pi.obj X).n = X.n definitionally (the obj-map copies n, groupFin, … and only permutes the marking), and the morphism map is the same underlying homomorphism Fin X.n →* Fin Y.n. Since both d0Diagram and piDiagram send their index object to ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Fin ·.n)) and a morphism to ProfiniteGrp.ofFiniteGrpHom (FiniteGrp.ofHom ·.toMonoidHom), the two inverse systems agree on the nose along the Nielsen functor: D0_to_Pi ⋙ piDiagram ≅ d0Diagram (the natural iso d0CompIso, with identity components).

Limit-invariance under the index equivalence (HasLimit.isoOfEquivalence applied to D0_Pi_index_equiv) then gives the profinite isomorphism D₀ = limit d0Diagram ≅ limit piDiagram = Π.

source
noncomputable def Q2Presentation.d0CompIso :
D0_to_Pi.comp piDiagram ≅ d0Diagram

The Nielsen comparison of inverse systems D0_to_Pi ⋙ piDiagram ≅ d0Diagram.

The Nielsen functor D0_to_Pi relabels each finite Demushkin quotient by the same underlying skeletal group Fin X.n (only the marking is permuted), and its morphism map is the same underlying homomorphism. Hence the composite diagram D0_to_Pi ⋙ piDiagram and d0Diagram are object- and morphism-wise equal, so the natural iso has identity components.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Q2Presentation.D0_iso_PiGrp :
    D0 ≅ PiGrp

    The profinite Nielsen comparison D₀ ≅ Π (manuscript Corollary 3.12, cor:relativeDemushkin).

    The Nielsen transform's category equivalence D0_Pi_index_equiv : D0MarkedFinite ≌ PiMarkedFinite carries the Demushkin inverse system d0Diagram to the pro-2 boundary system piDiagram (via the natural iso d0CompIso); limit-invariance under that equivalence of cofiltered index categories (HasLimit.isoOfEquivalence) yields the profinite isomorphism D₀ = limit d0Diagram ≅ limit piDiagram = Π.

    Equations
    Instances For

      The Nielsen comparison preserves the unramified markings #

      The genuine profinite Nielsen isomorphism D₀ ≅ Π intertwines the two unramified characters ν_ur : D₀ ↠ ℤ₂ (Local/NuUr.lean, marks (a,s,y) ↦ (-2,1,0)) and ν₂ : Π ↠ ℤ₂ (Boundary/PiGroup.lean, marks (σ,x₀,x₁) ↦ (1,0,0)): ν_ur = D0_iso_PiGrp.hom ≫ ν₂. This is the marking half of manuscript Cor. 3.12 / Prop compatiblemarking (l.1085–1110): the Nielsen change of generators σ = s, x₁ = y, x₀ = s⁻²a⁻¹ (equivalently a = x₀⁻¹σ⁻²) carries the marks compatibly — ν₂(x₀⁻¹σ⁻²) = -2·1 = ν_ur(a), ν₂(σ) = 1 = ν_ur(s), ν₂(x₁) = 0 = ν_ur(y).

      The proof works through the inverse limits: HasLimit.isoOfEquivalence_inv_π identifies the D₀-coordinate of D0_iso_PiGrp.inv p at a Demushkin quotient j with the Π-coordinate of p at the Nielsen-relabelled quotient D0_to_Pi.obj j (the comparison natural iso d0CompIso has identity components). Evaluating the unramified layers at the auxiliary cyclic quotient cyclicD0 n then reduces the character identity to the three generator marks, computed by cyclicD0Equiv_*.

      source
      theorem Q2Presentation.d0iso_inv_proj (j : D0MarkedFinite) (p : ↑PiGrp.toProfinite.toTop) :
      (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram j)) ((ProfiniteGrp.Hom.hom D0_iso_PiGrp.inv) p) = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram (D0_to_Pi.obj j))) p

      Coordinate transport of the inverse Nielsen isomorphism. Projecting D0_iso_PiGrp.inv p to the Demushkin quotient j equals projecting p to the Nielsen-relabelled pro-2 quotient D0_to_Pi.obj j (since the comparison natural iso d0CompIso has identity components).

      source
      theorem Q2Presentation.d0LayerHom_inv (n : ℕ) (p : ↑PiGrp.toProfinite.toTop) :
      (d0LayerHom n) ((ProfiniteGrp.Hom.hom D0_iso_PiGrp.inv) p) = (cyclicD0Equiv n) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram (D0_to_Pi.obj (cyclicD0 n)))) p)

      The n-th unramified layer of ν_ur ∘ D0_iso_PiGrp.inv, read off the Nielsen-relabelled cyclic quotient D0_to_Pi.obj (cyclicD0 n).

      source
      theorem Q2Presentation.nu_ur_inv_piSigma :
      (ProfiniteGrp.Hom.hom nu_ur) ((ProfiniteGrp.Hom.hom D0_iso_PiGrp.inv) piSigma) = z2One

      ν_ur(D0_iso_PiGrp.inv σ) = 1 (σ ↦ s ↦ 1).

      source
      theorem Q2Presentation.nu_ur_inv_piX0 :
      (ProfiniteGrp.Hom.hom nu_ur) ((ProfiniteGrp.Hom.hom D0_iso_PiGrp.inv) piX0) = z2Zero

      ν_ur(D0_iso_PiGrp.inv x₀) = 0 (x₀ ↦ s⁻²a⁻¹, marks -2·1 - (-2) = 0).

      source
      theorem Q2Presentation.nu_ur_inv_piX1 :
      (ProfiniteGrp.Hom.hom nu_ur) ((ProfiniteGrp.Hom.hom D0_iso_PiGrp.inv) piX1) = z2Zero

      ν_ur(D0_iso_PiGrp.inv x₁) = 0 (x₁ ↦ y ↦ 0).

      source
      theorem Q2Presentation.nu_ur_inv_comp :
      CategoryTheory.CategoryStruct.comp D0_iso_PiGrp.inv nu_ur = nu_2

      The inverse Nielsen isomorphism intertwines ν₂ and ν_ur: D0_iso_PiGrp.inv ≫ ν_ur = ν₂. Both are continuous characters Π ↠ ℤ₂; they agree on the topological generators σ, x₀, x₁ (the three lemmas above versus nu_2_piSigma/piX0/piX1), hence on the dense generated subgroup, hence everywhere (Continuous.ext_on).

      source
      theorem Q2Presentation.nu_ur_eq_hom_comp_nu_2 :
      nu_ur = CategoryTheory.CategoryStruct.comp D0_iso_PiGrp.hom nu_2

      The profinite Nielsen comparison preserves the unramified marking (manuscript Cor. 3.12 / Prop compatiblemarking): ν_ur = D0_iso_PiGrp.hom ≫ ν₂. Derived from nu_ur_inv_comp by composing with D0_iso_PiGrp.hom.

      Acceptance checks #