Documentation

GQ2.AnabelianBridge.Construction

Construction of the anabelian bridge and lifting automorphisms #

The topological-generation toolkit, presentation lifts, automorphisms, rows, and shear lifts.

See GQ2.AnabelianBridge for the paper-facing overview, source citations, and deviations.

ẑ-power helpers #

source
theorem GQ2.zpowHat_inv {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (x : G) (γ : ↑Zhat.toProfinite.toTop) :
zpowHat x⁻¹ γ = (zpowHat x γ)⁻¹

ẑ-powers of inverses: (x⁻¹) ^ᶻ γ = (x ^ᶻ γ)⁻¹.

source
theorem GQ2.zpowHat_zpow {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (x : G) (γ : ↑Zhat.toProfinite.toTop) (n : ℤ) :
zpowHat x γ ^ n = zpowHat (x ^ n) γ

ẑ-powers commute with integer powers: (x ^ᶻ γ) ^ n = (x ^ n) ^ᶻ γ.

source
theorem GQ2.zpowHat_conjP {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x c : G) (γ : ↑Zhat.toProfinite.toTop) :
zpowHat (conjP x c) γ = conjP (zpowHat x γ) c

ẑ-powers commute with conjugation: (x ^ c) ^ᶻ γ = (x ^ᶻ γ) ^ c (conjP x c = c⁻¹xc).

ω₂ acts as the identity on pro-2 groups — the hι_proj/hι_one compatibility #

source
theorem GQ2.zpowHat_omega2_eq_self {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) (x : P) :
zpowHat x omega2 = x

On a pro-2 group, the profinite-exponentiation API idempotent ω₂ ∈ ℤ̂ powers every element to itself: x ^ᶻ ω₂ = x. (ω₂ ≡ 1 on the pro-2 part; every finite quotient of a pro-2 group is a 2-group, where powOmega2 is the identity.)

source
theorem GQ2.zpowHat_iota {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (R : PeripheralCyclotomicAction) (hP : IsProP 2 P) (x : P) (u : ℤ_[2]ˣ) :
zpowHat x (R.ι u) = zpowZtwo hP x ↑u

On a pro-2 group, B8's ι-powers are the 2-adic powers: x ^ᶻ ι u = zpowZtwo x u (via the hι_proj pinning and the ℤ₂-powering development's zpowHat_eq_zpowZtwo).

Pinned topological generation #

source
theorem GQ2.freeProfiniteGroup_pinned_generation (X : Type) :
(Subgroup.closure (Set.range FreeProfiniteGroup.of)).topologicalClosure = ⊤

The free generators of a free profinite group pinned-topologically-generate it (the generator-pinned refinement of isTopologicallyFinGen_freeProfiniteGroup; no finiteness of X needed).

source
theorem GQ2.pinned_generation_map {G : Type u_1} {Q : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] (f : G →* Q) (hf : Continuous ⇑f) (hfs : Function.Surjective ⇑f) {S : Set G} (hS : (Subgroup.closure S).topologicalClosure = ⊤) :
(Subgroup.closure (⇑f '' S)).topologicalClosure = ⊤

Pinned topological generation pushes forward along a continuous surjection.

source
theorem GQ2.topClosure_closure_le_ker {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] [T2Space H] (q : G →ₜ* H) {S : Set G} (h : ∀ x ∈ S, q x = 1) :
(Subgroup.closure S).topologicalClosure ≤ q.ker

A continuous hom into a Hausdorff group vanishing on a pinned generating family's members kills the whole closed generated subgroup.

source
theorem GQ2.topClosure_closure_le_comap {G : Type u_1} {H : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group H] [TopologicalSpace H] (f : G →ₜ* H) {S : Set G} {M : Subgroup H} (hM : IsClosed ↑M) (h : ∀ x ∈ S, f x ∈ M) :
(Subgroup.closure S).topologicalClosure ≤ Subgroup.comap f.toMonoidHom M

A continuous hom sending a pinned generating family into a closed subgroup sends the whole closed generated subgroup into it.

conjP algebra #

source
theorem GQ2.demushkin_relator_iff {G : Type u_1} [Group G] (α σ ψ : G) :
α ^ 2 * σ ^ 4 * commP σ ψ = 1 ↔ conjP σ ψ = (σ ^ 3)⁻¹ * (α ^ 2)⁻¹

The Demushkin relator in HNN form: α²σ⁴[σ,ψ] = 1 ↔ ψ⁻¹σψ = σ⁻³α⁻² (paper (16)).

Presentation lifts: maps out of Δ and D₀ into pro-2 targets #

source
noncomputable def GQ2.deltaLift {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] (hH : IsProP 2 H) (m : Fin 2 → H) :
↑Delta.toProfinite.toTop →ₜ* H

Universal property of Δ (free pro-2 on two generators): a pair of elements of a pro-2 group classifies a continuous hom Δ → H.

Equations
Instances For
    source
    noncomputable def GQ2.d0Lift {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H] (hH : IsProP 2 H) (m : Fin 3 → H) (hrel : m 0 ^ 2 * m 1 ^ 4 * commP (m 1) (m 2) = 1) :
    ↑D0.toProfinite.toTop →ₜ* H

    Universal property of D₀: a triple of elements of a pro-2 group satisfying the Demushkin relation classifies a continuous hom D₀ → H.

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

      Pinned generation of Δ and D₀, and their topological finite generation #

      source
      theorem GQ2.isProP_d0 :
      IsProP 2 ↑D0.toProfinite.toTop

      D₀ is pro-2.

      source
      theorem GQ2.delta_pinned :
      (Subgroup.closure {deltaP, deltaT}).topologicalClosure = ⊤

      {P, T} pinned-topologically-generate Δ.

      source
      theorem GQ2.d0_pinned :
      (Subgroup.closure {d0A, d0S, d0Y}).topologicalClosure = ⊤

      {A, S, Y} pinned-topologically-generate D₀.

      source
      theorem GQ2.d0_topologicallyFinGen :
      ∃ (s : Finset ↑D0.toProfinite.toTop), (Subgroup.closure ↑s).topologicalClosure = ⊤

      D₀ is topologically finitely generated (the ∃ s : Finset _ form profinite_hopfian consumes).

      The index-2 quotient toolkit #

      source
      theorem GQ2.discreteTopology_quotient_openNormal {K : Type} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] (U : OpenNormalSubgroup K) :
      DiscreteTopology (K ⧸ ↑U.toOpenSubgroup)

      Quotients by open normal subgroups are discrete.

      source
      theorem GQ2.zpowZtwo_eq_self_of_sq_eq_one {P : Type} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [T2Space P] [TotallyDisconnectedSpace P] (hP : IsProP 2 P) {x : P} (hx : x ^ 2 = 1) (u : ℤ_[2]ˣ) :
      zpowZtwo hP x ↑u = x

      Pro-2 powering fixes square-one elements: x² = 1 ⇒ x^u = x for u ∈ ℤ₂ˣ (odd exponents act trivially on exponent-2 elements).

      source
      theorem GQ2.quotient_mul_comm {K : Type} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {M : OpenNormalSubgroup K} (hM : (↑M.toOpenSubgroup).index = 2) (z w : K ⧸ ↑M.toOpenSubgroup) :
      z * w = w * z

      The index-2 quotient is commutative.

      source
      theorem GQ2.quotient_sq_eq_one {K : Type} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {M : OpenNormalSubgroup K} (hM : (↑M.toOpenSubgroup).index = 2) (z : K ⧸ ↑M.toOpenSubgroup) :
      z ^ 2 = 1

      Squares die in the index-2 quotient.

      source
      theorem GQ2.quotient_map_conjP {K : Type} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] {M : OpenNormalSubgroup K} (hM : (↑M.toOpenSubgroup).index = 2) (x c : K) :
      (QuotientGroup.mk' ↑M.toOpenSubgroup) (conjP x c) = (QuotientGroup.mk' ↑M.toOpenSubgroup) x

      Conjugation dies in the index-2 quotient.

      source
      theorem GQ2.quotient_map_zpowHat_iota {K : Type} [Group K] [TopologicalSpace K] [IsTopologicalGroup K] [CompactSpace K] [TotallyDisconnectedSpace K] {M : OpenNormalSubgroup K} (hM : (↑M.toOpenSubgroup).index = 2) (R : PeripheralCyclotomicAction) (x : K) (u : ℤ_[2]ˣ) :
      (QuotientGroup.mk' ↑M.toOpenSubgroup) (zpowHat x (R.ι u)) = (QuotientGroup.mk' ↑M.toOpenSubgroup) x

      B8's ι-powers die in index-2 quotients: q(x ^ᶻ ι u) = q(x) (u is odd).

      The peripheral identity and its push to D₀ #

      source
      theorem GQ2.peripheral_identity (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
      (conjP (zpowHat deltaP (R.ι u)) (R.cP u) * conjP (zpowHat deltaT (R.ι u)) (R.cT u))⁻¹ = conjP (zpowHat (deltaP * deltaT)⁻¹ (R.ι u)) (R.cC u)

      The combined B8 identity (*): the three conjugation rows of Lemma 3.6 are tied together by φ_u being a homomorphism and P·T·C = 1.

      source
      noncomputable def GQ2.lambdaHom :
      ↑Delta.toProfinite.toTop →ₜ* ↑D0.toProfinite.toTop

      The transport hom λ : Δ → D₀, P ↦ s³, T ↦ s⁻³a⁻² (the paper's "view the words in E□ ⊆ D₀ via P, T" — the composite of its Tietze identifications, inlined).

      Equations
      Instances For
        source
        theorem GQ2.d0_relation_hnn :
        conjP d0S d0Y = (d0S ^ 3)⁻¹ * (d0A ^ 2)⁻¹

        The Demushkin relation in HNN form (paper (16)): y⁻¹sy = s⁻³a⁻² in D₀.

        source
        theorem GQ2.pushed_identity (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
        conjP (zpowHat ((d0S ^ 3)⁻¹ * (d0A ^ 2)⁻¹) (R.ι u)) (lambdaHom (R.cT u)) = conjP (zpowHat (d0S ^ 3)⁻¹ (R.ι u)) (lambdaHom (R.cP u)) * conjP (zpowHat (d0A ^ 2)⁻¹ (R.ι u)) (lambdaHom (R.cC u))

        The pushed identity: transporting (*) along λ produces the conjugation identity that the Ψ_u-relator check consumes.

        Ψ_u : construction, surjectivity, automorphism #

        source
        theorem GQ2.zpowHat_pow {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] (x : G) (γ : ↑Zhat.toProfinite.toTop) (n : ℕ) :
        zpowHat x γ ^ n = zpowHat (x ^ n) γ

        ẑ-powers commute with natural-number powers.

        source
        theorem GQ2.psi_relator (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
        conjP (zpowHat d0A (R.ι u)) (lambdaHom (R.cC u)) ^ 2 * conjP (zpowHat d0S (R.ι u)) (lambdaHom (R.cP u)) ^ 4 * commP (conjP (zpowHat d0S (R.ι u)) (lambdaHom (R.cP u))) ((lambdaHom (R.cP u))⁻¹ * d0Y * lambdaHom (R.cT u)) = 1

        The Ψ_u-marking respects the Demushkin relator (via the HNN form (16) and the pushed peripheral identity).

        source
        noncomputable def GQ2.psiHom (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
        ↑D0.toProfinite.toTop →ₜ* ↑D0.toProfinite.toTop

        Ψ_u as a continuous endomorphism of D₀: A ↦ (A^u)^{κ_C}, S ↦ (S^u)^{κ_P}, Y ↦ κ_P⁻¹ Y κ_T (paper, proof of Lemma 3.7).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem GQ2.lambdaHom_mem_closure (γ : ↑Delta.toProfinite.toTop) :
          lambdaHom γ ∈ (Subgroup.closure {d0S, d0A}).topologicalClosure

          λ lands in the closed subgroup generated by s, a.

          source
          theorem GQ2.psiHom_surjective (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
          Function.Surjective ⇑(psiHom R u)

          Ψ_u is surjective (the pro-2 Frattini criterion: in every index-2 quotient the u-powers and the conjugators are invisible, so Ψ_u moves the generators by elements the generators already reach).

          source
          noncomputable def GQ2.psiEquiv (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
          ↑D0.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop

          Ψ_u is a continuous automorphism of D₀ (surjectivity + Hopficity).

          Equations
          Instances For

            The abelianized rows (paper (15)) and Lemma 3.7 #

            source
            theorem GQ2.zpowZtwo_multPadicInt (c u : ℤ_[2]) :
            zpowZtwo PropOneOne.isProP_two_multPadicInt (Multiplicative.ofAdd c) u = Multiplicative.ofAdd (c * u)

            2-adic powering on Multiplicative ℤ₂ is multiplication of exponents.

            source
            theorem GQ2.zpowHat_iota_multProd (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) (c₀ : ZMod 2) (c₁ c₂ : ℤ_[2]) :
            zpowHat (Multiplicative.ofAdd (c₀, c₁, c₂)) (R.ι u) = Multiplicative.ofAdd (c₀, ↑u * c₁, ↑u * c₂)

            ι u-powering on the coordinate group acts trivially on the ℤ/2-component and by u-multiplication on the ℤ₂-components.

            source
            noncomputable def GQ2.bCoordHom (B : SectionThree.BDecomposition) :
            ↑D0.toProfinite.toTop →ₜ* Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2])

            The coordinate hom φ = B.e ∘ abMk : D₀ → ℤ/2 × ℤ₂ × ℤ₂ of eq. (11).

            Equations
            Instances For
              source
              theorem GQ2.bCoord_psiHom_A (B : SectionThree.BDecomposition) (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
              (bCoordHom B) ((psiHom R u) d0A) = Multiplicative.ofAdd (1, -2 * ↑u, 0)

              The Ā-row of Ψ_u (paper (15)): Ā = (1,−2,0) ↦ (1,−2u,0).

              source
              theorem GQ2.bCoord_psiHom_S (B : SectionThree.BDecomposition) (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
              (bCoordHom B) ((psiHom R u) d0S) = Multiplicative.ofAdd (0, ↑u, 0)

              The S̄-row of Ψ_u (paper (15)): S̄ = (0,1,0) ↦ (0,u,0).

              source
              theorem GQ2.SectionThree.lemma_3_7 (B : BDecomposition) (u : ℤ_[2]ˣ) :
              ∃ (Ψ : ↑D0.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop), B.e (abMk (Ψ d0A)) = Multiplicative.ofAdd (1, -2 * ↑u, 0) ∧ B.e (abMk (Ψ d0S)) = Multiplicative.ofAdd (0, ↑u, 0)

              Lemma 3.7 (paper (15)): for every u ∈ ℤ₂ˣ there is a continuous automorphism Ψ_u of D₀ acting on B-coordinates by Ā = (1,−2,0) ↦ (1,−2u,0), S̄ = (0,1,0) ↦ (0,u,0). Consumes axiom B8 (peripheralCyclotomicAction). Declared here (not in GQ2/SectionThree.lean) because the proof needs this file's bridge; same namespace, per the Prop. 3.2 precedent (GQ2/Prop32.lean).

              Proposition 3.8, lifting half: the shear Θ_b (paper (19)) and the composite #

              source
              noncomputable def GQ2.sPow (b : ℤ_[2]) :
              ↑D0.toProfinite.toTop

              S^b for a 2-adic exponent b.

              Equations
              Instances For
                source
                theorem GQ2.commute_pow_sPow (n : ℕ) (b : ℤ_[2]) :
                Commute (d0S ^ n) (sPow b)

                Ordinary S-powers commute with S^b.

                source
                theorem GQ2.conjP_conjP {G : Type u_1} [Group G] (x c d : G) :
                conjP (conjP x c) d = conjP x (c * d)

                Composing conjugations multiplies the conjugators.

                source
                theorem GQ2.theta_relator (b : ℤ_[2]) :
                conjP d0A (sPow b) ^ 2 * d0S ^ 4 * commP d0S (d0Y * sPow b) = 1

                The shear marking respects the Demushkin relator (paper (19)): Θ_b(A) = A^{S^b}, Θ_b(S) = S, Θ_b(Y) = Y·S^b.

                source
                noncomputable def GQ2.thetaHom (b : ℤ_[2]) :
                ↑D0.toProfinite.toTop →ₜ* ↑D0.toProfinite.toTop

                The shear Θ_b (paper (19)) as a continuous endomorphism of D₀.

                Equations
                Instances For
                  source
                  theorem GQ2.d0Hom_ext {H : Type u_1} [Group H] [TopologicalSpace H] [T2Space H] {f g : ↑D0.toProfinite.toTop →ₜ* H} (hA : f d0A = g d0A) (hS : f d0S = g d0S) (hY : f d0Y = g d0Y) :
                  f = g

                  Extensionality on D₀: continuous homs agreeing on the three marked generators agree.

                  source
                  theorem GQ2.thetaHom_sPow (b c : ℤ_[2]) :
                  (thetaHom b) (sPow c) = sPow c

                  Θ_b fixes every S-power.

                  source
                  theorem GQ2.thetaHom_comp_neg (b : ℤ_[2]) (x : ↑D0.toProfinite.toTop) :
                  (thetaHom b) ((thetaHom (-b)) x) = x

                  Θ_b ∘ Θ_{−b} = id on points.

                  source
                  noncomputable def GQ2.thetaEquiv (b : ℤ_[2]) :
                  ↑D0.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop

                  Θ_b is a continuous automorphism (inverse Θ_{−b}).

                  Equations
                  Instances For

                    The Ȳ-row of Ψ_u, and Proposition 3.8 (lifting half) #

                    source
                    noncomputable def GQ2.bcoordMiddle :
                    Subgroup (Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2]))

                    The coordinate subgroup {(0, ∗, 0)}-shaped constraint: trivial ℤ/2- and Ȳ-components.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      theorem GQ2.bCoord_lambda_mem (B : SectionThree.BDecomposition) (γ : ↑Delta.toProfinite.toTop) :
                      (bCoordHom B) (lambdaHom γ) ∈ bcoordMiddle

                      The conjugator words land in the (0, ∗, 0)-coordinate constraint: λ's generators s³ and s⁻³a⁻² have trivial ℤ/2- and Ȳ-coordinates (−2Ā kills the torsion coordinate).

                      source
                      theorem GQ2.bcoord_ext {z w : Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2])} (h1 : (Multiplicative.toAdd z).1 = (Multiplicative.toAdd w).1) (h2 : (Multiplicative.toAdd z).2.1 = (Multiplicative.toAdd w).2.1) (h3 : (Multiplicative.toAdd z).2.2 = (Multiplicative.toAdd w).2.2) :
                      z = w

                      Componentwise extensionality on the coordinate group.

                      source
                      theorem GQ2.bCoord_psiHom_Y (B : SectionThree.BDecomposition) (R : PeripheralCyclotomicAction) (u : ℤ_[2]ˣ) :
                      ∃ (c : ℤ_[2]), (bCoordHom B) ((psiHom R u) d0Y) = Multiplicative.ofAdd (0, c, 1)

                      The Ȳ-row of Ψ_u has the shape (0, c, 1): the conjugators contribute only in the S̄-coordinate.

                      source
                      theorem GQ2.isProP_two_bcoord (B : SectionThree.BDecomposition) :
                      IsProP 2 (Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2]))

                      The coordinate group is pro-2 (continuous surjective image of D₀^{ab} under B.e).

                      source
                      theorem GQ2.zpowZtwo_bcoord_S (hBc : IsProP 2 (Multiplicative (ZMod 2 × ℤ_[2] × ℤ_[2]))) (v w : ℤ_[2]) :
                      zpowZtwo hBc (Multiplicative.ofAdd (0, v, 0)) w = Multiplicative.ofAdd (0, v * w, 0)

                      Powering the S̄-line of the coordinate group multiplies the S̄-coordinate.

                      source
                      theorem GQ2.SectionThree.prop_3_8_lift (B : BDecomposition) (u : ℤ_[2]ˣ) (b : ℤ_[2]) :
                      ∃ (Ψ : ↑D0.toProfinite.toTop ≃ₜ* ↑D0.toProfinite.toTop), B.e (abMk (Ψ d0A)) = Multiplicative.ofAdd (1, -2 * ↑u, 0) ∧ B.e (abMk (Ψ d0S)) = Multiplicative.ofAdd (0, ↑u, 0) ∧ B.e (abMk (Ψ d0Y)) = Multiplicative.ofAdd (0, b, 1)

                      Proposition 3.8, lifting half (paper (18)/(19)): every α_{u,b} lifts to a continuous automorphism of D₀ — Ψ_u composed with the shear Θ_{b'}, b' = (b − c(u))u⁻¹. Consumes axiom B8. Declared here per the Prop. 3.2 precedent.