4. The tame and maximal pro-2 quotients🔗

Lemma4.1

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Proposition 4.2

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 4

Reverse dependency previews

Preview

Proposition 4.2

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Lemma 3.1 of the paper (Finite tame quotients).

In every finite quotient generated by s,t with t^s=t^2, the element t has odd order, and the quotient has the form

C_e\rtimes C_n, \qquad e\text{ odd}, \qquad s^{-1}ts=t^2.

Every normal 2-subgroup of such a quotient is central and lies in the unramified cyclic direction.

Lean code for Lemma4.1●2 theorems

theoremdefined in GQ2/Tame.lean

complete

theorem GQ2.Tame.tame_odd_order.{u_1} {G : Type u_1} [Group G] {s t : G}
  (hs : orderOf s ≠ 0) (h : s⁻¹ * t * s = t ^ 2) : Odd (orderOf t)

theorem GQ2.Tame.tame_odd_order.{u_1}
  {G : Type u_1} [Group G] {s t : G}
  (hs : orderOf s ≠ 0)
  (h : s⁻¹ * t * s = t ^ 2) :
  Odd (orderOf t)

**Lemma 3.1 (first assertion).** If a finite group is generated by `s, t` with the tame
relation `s⁻¹ t s = t²` (so in particular `s` has finite order), then `t` has odd order.

theoremdefined in GQ2/Tame.lean

complete

theorem GQ2.Tame.tame_normal_two_subgroup_central.{u_1} {G : Type u_1} [Group G]
  {s t : G} [Finite G] (hgen : Subgroup.closure {s, t} = ⊤)
  (h : s⁻¹ * t * s = t ^ 2) (N : Subgroup G) [hNnorm : N.Normal]
  (hN : IsPGroup 2 ↥N) : N ≤ Subgroup.center G

theorem GQ2.Tame.tame_normal_two_subgroup_central.{u_1}
  {G : Type u_1} [Group G] {s t : G}
  [Finite G]
  (hgen : Subgroup.closure {s, t} = ⊤)
  (h : s⁻¹ * t * s = t ^ 2)
  (N : Subgroup G) [hNnorm : N.Normal]
  (hN : IsPGroup 2 ↥N) :
  N ≤ Subgroup.center G

**Lemma 3.1 (normal 2-subgroups are central).** Every normal 2-subgroup `N` of a finite tame
quotient `⟨s,t | s⁻¹ t s = t²⟩` is central.

Key idea: `N ⊓ ⟨t⟩ = ⊥` (coprime orders), so for `n ∈ N` the commutator `⁅n,s⁆` lies in `N`
(normality) *and* in `⟨t⟩` (the quotient `G/⟨t⟩` is cyclic, hence abelian), whence `⁅n,s⁆ = 1`;
together with `⁅n,t⁆ = 1` this puts `n` in the centralizer of the generators `{s,t}`, i.e. the
centre.

Proposition4.2

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 2

Reverse dependency previews

Preview

Proposition 4.9

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Proposition 3.2 of the paper (Common tame quotient).

There are canonical isomorphisms

\GA/\WA\cong \TA\cong \GQ/\WF,

where \WF is wild inertia.

Lean code for Proposition4.2●3 declarations

theoremdefined in GQ2/Prop32.lean

complete

theorem GQ2.SectionThree.prop_3_2_gammaA :
  ∃ e,
    e ↑GQ2.SectionThree.gammaSigma = GQ2.tameSigma ∧
      e ↑GQ2.SectionThree.gammaTau = GQ2.tameTau

theorem GQ2.SectionThree.prop_3_2_gammaA :
  ∃ e,
    e ↑GQ2.SectionThree.gammaSigma =
        GQ2.tameSigma ∧
      e ↑GQ2.SectionThree.gammaTau =
        GQ2.tameTau

**Prop. 3.2, `Γ_A` side**: the quotient of `Γ_A` by `W_A` is `T_tame`,
matching the marked generators.

theoremdefined in GQ2/Prop32.lean

complete

theorem GQ2.SectionThree.prop_3_2_local [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] :
  Nonempty GQ2.SectionThree.LocalTameQuotient

theorem GQ2.SectionThree.prop_3_2_local
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace
      GQ2.AbsGalQ2] :
  Nonempty
    GQ2.SectionThree.LocalTameQuotient

**Prop. 3.2, local side** (`Ax = B10`): the tame quotient of
`G_{ℚ₂}` is `T_tame`, by the *maximal* closed normal pro-2 subgroup.  Existence is axiom B10
(oriented form B10′ since the marked pro-2 isomorphisms; only the underlying `TameQuotientData` is used here);
maximality is Lemma 3.3 (`tameData_maximal`).

structure(extends 1, 6 fields)defined in GQ2/SectionThree.lean

complete

structure GQ2.SectionThree.LocalTameQuotient : Type

structure GQ2.SectionThree.LocalTameQuotient : Type

**Prop. 3.2, local side + Lemma 3.3's characterization, bundled.**  Extends the B10
bundle `TameQuotientData` (`GQ2/TameQuotient.lean`: `W` closed normal pro-2 with
`G_{ℚ₂}/W ≅ T_tame` — the paper's wild inertia, encoded intrinsically since Mathlib has no
ramification theory; **deviation, flagged there**) by Lemma 3.3's **maximality**, which pins
`W` uniquely (the "canonical" of Prop. 3.2 on the local side).  Maximality is deliberately
*not* part of axiom B10 — it is the paper's own proved content.

Extends

GQ2.TameQuotientData

Fields

W : Subgroup GQ2.AbsGalQ2

Inherited from

GQ2.TameQuotientData

normal : self.W.Normal

Inherited from

GQ2.TameQuotientData

isClosed : IsClosed ↑self.W

Inherited from

GQ2.TameQuotientData

isProP : GQ2.IsProP 2 ↥self.W

Inherited from

GQ2.TameQuotientData

equiv : GQ2.AbsGalQ2 ⧸ self.W ≃ₜ* ↑GQ2.Ttame.toProfinite.toTop

Inherited from

GQ2.TameQuotientData

maximal : ∀ (N : Subgroup GQ2.AbsGalQ2), N.Normal → IsClosed ↑N → GQ2.IsProP 2 ↥N → N ≤ self.W

`W_F` is the **maximal** closed normal pro-2 subgroup — Lemma 3.3's `O₂(G_{ℚ₂}) = W_F`.

Proof for Proposition 4.2

Proof uses 4

Proof dependency previews

Preview

Proposition 1.2

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §3 of the paper. Ingredients: Proposition 1.2 Proposition 1.7 Lemma 4.3 Lemma 4.1.

Lemma4.3

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1!L∃∀N

Lemma 3.3 of the paper (The wild subgroup is the characteristic 2-core).

The tame group \TA has no nontrivial closed normal pro-2 subgroup. Consequently

O_2(\GA)=\WA, \qquad O_2(\GQ)=\WF.

In particular, the marked wild subgroups of the two sources are characteristic.

Lean code for Lemma4.3●4 declarations, 2 missing

GQ2.SectionThree.qMk_mem_of_two_imagesmissing declaration

declaration not found (name was not present during directive/code-block registration)

GQ2.SectionThree.eq_one_of_mem_inertiaPartmissing declaration

declaration not found (name was not present during directive/code-block registration)

theoremdefined in GQ2/Prop32.lean

complete

theorem GQ2.SectionThree.eq_bot_of_normal_two_images
  (M : Subgroup ↑GQ2.Ttame.toProfinite.toTop) [hMn : M.Normal]
  (h2 :
    ∀ (G : Type) [inst : Group G] [inst_1 : TopologicalSpace G]
      [DiscreteTopology G] [Finite G]
      (f : ↑GQ2.Ttame.toProfinite.toTop →* G),
      Continuous ⇑f → IsPGroup 2 ↥(Subgroup.map f M)) :
  M = ⊥

theorem GQ2.SectionThree.eq_bot_of_normal_two_images
  (M :
    Subgroup ↑GQ2.Ttame.toProfinite.toTop)
  [hMn : M.Normal]
  (h2 :
    ∀ (G : Type) [inst : Group G]
      [inst_1 : TopologicalSpace G]
      [DiscreteTopology G] [Finite G]
      (f :
        ↑GQ2.Ttame.toProfinite.toTop →*
          G),
      Continuous ⇑f →
        IsPGroup 2 ↥(Subgroup.map f M)) :
  M = ⊥

**Lemma 3.3 (core)**: a normal subgroup of `T_tame` all of whose finite continuous images
are 2-groups is trivial.  Paper argument: through each Fermat level `G_m` the image is a
central 2-subgroup of a center-free group, hence trivial, so the `Q`-coordinate dies in every
`C_{2^m}`; the cyclic level-comparison then kills the `Q`-image entirely, and the remaining
inertia part has both odd and 2-power order levelwise.

theoremdefined in GQ2/Prop32.lean

complete

theorem GQ2.SectionThree.tameData_maximal [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (T' : GQ2.TameQuotientData)
  (N : Subgroup GQ2.AbsGalQ2) :
  N.Normal → IsClosed ↑N → GQ2.IsProP 2 ↥N → N ≤ T'.W

theorem GQ2.SectionThree.tameData_maximal
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (T' : GQ2.TameQuotientData)
  (N : Subgroup GQ2.AbsGalQ2) :
  N.Normal →
    IsClosed ↑N →
      GQ2.IsProP 2 ↥N → N ≤ T'.W

**Lemma 3.3's maximality, for any B10 datum** (extracted from `prop_3_2_local`'s proof
so the marked pro-2 isomorphisms oriented witness can reuse it): every closed normal pro-2 subgroup lies in `T.W`
(`eq_bot_of_normal_two_images` applied to the image of the competitor `N` in `T_tame`).

Lemma4.4

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma 3.5 of the paper (Marked abelianization, orientation, and initial form).

Use arithmetic local reciprocity \rec, normalized so that \rec(2) is arithmetic Frobenius, and normalize \nu_{\mathrm{ur}} geometrically. Put

\bar s=\rec(2)^{-1}=\rec(1/2),\qquad \bar\epsilon=\rec(-1),\qquad \bar y=\rec(-3),\qquad \bar a=\bar\epsilon\bar s^{-2}=\rec(-4).

Then the pro-2 abelianization of D_{\mathrm{loc}}=G_{\Qtwo}(2) is identified with B_{\mathrm{ab}} by

\bar A\longmapsto\bar a, \qquad \bar S\longmapsto\bar s, \qquad \bar Y\longmapsto\bar y.

Under this identification,

\nu_{\mathrm{ur}}(\bar a,\bar s,\bar y)=(-2,1,0), \qquad \chi_{\mathrm{loc}}(\bar a,\bar s,\bar y)=(-1,1,(-3)^{-1}),

where \chi_{\mathrm{loc}} is the canonical Demushkin orientation. In the basis of H^1(D_{\mathrm{loc}},\F_2) dual to (\bar a,\bar s,\bar y), the Demushkin quadratic initial form is

\alpha^2+\beta\gamma+\gamma\beta.

Consequently a Demushkin relator for lifts of these classes has the same quadratic initial form as

r_0=A^2S^4[S,Y],

namely A^2+[S,Y] in degree two. Moreover the pair

(\nu_{\mathrm{ur}},\chi_{\mathrm{loc}}):B_{\mathrm{ab}}\longrightarrow \mathbb{Z}_2\times\mathbb{Z}_2^\times

is injective.

Lean code for Lemma4.4●3 theorems

theoremdefined in GQ2/SectionThree.lean

complete

theorem GQ2.SectionThree.lemma_3_5_injective
  (ν :
    GQ2.topAbelianization ↑GQ2.D0.toProfinite.toTop →*
      Multiplicative ℤ_[2])
  (hν : Continuous ⇑ν)
  (χ : GQ2.topAbelianization ↑GQ2.D0.toProfinite.toTop →* ℤ_[2]ˣ)
  (hχ : Continuous ⇑χ)
  (hνA : ν (GQ2.SectionThree.abMk GQ2.d0A) = Multiplicative.ofAdd ↑(-2))
  (hνS : ν (GQ2.SectionThree.abMk GQ2.d0S) = Multiplicative.ofAdd ↑1)
  (hνY : ν (GQ2.SectionThree.abMk GQ2.d0Y) = Multiplicative.ofAdd ↑0)
  (hχA : χ (GQ2.SectionThree.abMk GQ2.d0A) = -1)
  (hχS : χ (GQ2.SectionThree.abMk GQ2.d0S) = 1)
  (hχY :
    ∀ (y : ℤ_[2]ˣ), ↑y = -3 → χ (GQ2.SectionThree.abMk GQ2.d0Y) = y⁻¹)
  (x y : GQ2.topAbelianization ↑GQ2.D0.toProfinite.toTop) :
  ν x = ν y → χ x = χ y → x = y

theorem GQ2.SectionThree.lemma_3_5_injective
  (ν :
    GQ2.topAbelianization
        ↑GQ2.D0.toProfinite.toTop →*
      Multiplicative ℤ_[2])
  (hν : Continuous ⇑ν)
  (χ :
    GQ2.topAbelianization
        ↑GQ2.D0.toProfinite.toTop →*
      ℤ_[2]ˣ)
  (hχ : Continuous ⇑χ)
  (hνA :
    ν (GQ2.SectionThree.abMk GQ2.d0A) =
      Multiplicative.ofAdd ↑(-2))
  (hνS :
    ν (GQ2.SectionThree.abMk GQ2.d0S) =
      Multiplicative.ofAdd ↑1)
  (hνY :
    ν (GQ2.SectionThree.abMk GQ2.d0Y) =
      Multiplicative.ofAdd ↑0)
  (hχA :
    χ (GQ2.SectionThree.abMk GQ2.d0A) =
      -1)
  (hχS :
    χ (GQ2.SectionThree.abMk GQ2.d0S) = 1)
  (hχY :
    ∀ (y : ℤ_[2]ˣ),
      ↑y = -3 →
        χ
            (GQ2.SectionThree.abMk
              GQ2.d0Y) =
          y⁻¹)
  (x y :
    GQ2.topAbelianization
      ↑GQ2.D0.toProfinite.toTop) :
  ν x = ν y → χ x = χ y → x = y

**Lemma 3.5, injectivity clause**: the pair `(ν_ur, χ_D) : B → ℤ₂ × ℤ₂ˣ` is injective.
Stated intrinsically on `B = D₀^{ab}`: any continuous pair with the eq. (13) rows on the
marked generator classes separates points.  (The rows pin `ν, χ` on a dense subgroup, hence
everywhere, so this *is* the paper's clause.)  Proof the Lemmas 3.4–3.5 proof — from `b_decomposition`
plus `v₂(η − 1) = 2` (`η = (−3)⁻¹` topologically generates `1 + 4ℤ₂`).

theoremdefined in GQ2/SectionThree.lean

complete

theorem GQ2.SectionThree.lemma_3_5_marked_abelianization
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (R : GQ2.LocalReciprocity) :
  ∃ e,
    (∀ (g : GQ2.AbsGalQ2),
        GQ2.toAb g = R.recip GQ2.SectionThree.unitNeg4 →
          e (GQ2.SectionThree.abMk GQ2.d0A) =
            GQ2.SectionThree.abMk ((GQ2.maxProPMk 2 GQ2.AbsGalQ2) g)) ∧
      (∀ (g : GQ2.AbsGalQ2),
          GQ2.toAb g = (R.recip GQ2.uniformizer)⁻¹ →
            e (GQ2.SectionThree.abMk GQ2.d0S) =
              GQ2.SectionThree.abMk
                ((GQ2.maxProPMk 2 GQ2.AbsGalQ2) g)) ∧
        ∀ (g : GQ2.AbsGalQ2),
          GQ2.toAb g = R.recip GQ2.SectionThree.unitNeg3 →
            e (GQ2.SectionThree.abMk GQ2.d0Y) =
              GQ2.SectionThree.abMk ((GQ2.maxProPMk 2 GQ2.AbsGalQ2) g)

theorem GQ2.SectionThree.lemma_3_5_marked_abelianization
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (R : GQ2.LocalReciprocity) :
  ∃ e,
    (∀ (g : GQ2.AbsGalQ2),
        GQ2.toAb g =
            R.recip
              GQ2.SectionThree.unitNeg4 →
          e
              (GQ2.SectionThree.abMk
                GQ2.d0A) =
            GQ2.SectionThree.abMk
              ((GQ2.maxProPMk 2
                  GQ2.AbsGalQ2)
                g)) ∧
      (∀ (g : GQ2.AbsGalQ2),
          GQ2.toAb g =
              (R.recip
                  GQ2.uniformizer)⁻¹ →
            e
                (GQ2.SectionThree.abMk
                  GQ2.d0S) =
              GQ2.SectionThree.abMk
                ((GQ2.maxProPMk 2
                    GQ2.AbsGalQ2)
                  g)) ∧
        ∀ (g : GQ2.AbsGalQ2),
          GQ2.toAb g =
              R.recip
                GQ2.SectionThree.unitNeg3 →
            e
                (GQ2.SectionThree.abMk
                  GQ2.d0Y) =
              GQ2.SectionThree.abMk
                ((GQ2.maxProPMk 2
                    GQ2.AbsGalQ2)
                  g)

**Lemma 3.5, marked-abelianization clause**: the pro-2 abelianization of `D = G_{ℚ₂}(2)`
is identified with `B = D₀^{ab}` by `Ā ↦ ā = rec(−4)`, `S̄ ↦ s̄ = rec(2)⁻¹ = rec(1/2)`,
`Ȳ ↦ ȳ = rec(−3)`.  The `rec`-classes live in `G^{ab}` (`R.recip`); the matching is quantified
over lifts `g ∈ G_{ℚ₂}` (all lifts agree via `markedPi`, an abelian descent).  The proof uses
`markedHom_bijective` and B5.

theoremdefined in GQ2/SectionThree.lean

complete

theorem GQ2.SectionThree.lemma_3_5_hilbert_ledger :
  GQ2.HilbertSymbol.hilbertSymbol (GQ2.HilbertSymbol.unitCoe (-1))
        (GQ2.HilbertSymbol.unitCoe (-1)) =
      -1 ∧
    (∀ (y : ℤ_[2]ˣ),
        ↑y = -3 →
          GQ2.HilbertSymbol.hilbertSymbol GQ2.HilbertSymbol.unit2
              (GQ2.HilbertSymbol.unitCoe y) =
            -1) ∧
      GQ2.HilbertSymbol.hilbertSymbol (GQ2.HilbertSymbol.unitCoe (-1))
            GQ2.HilbertSymbol.unit2 =
          1 ∧
        (∀ (y : ℤ_[2]ˣ),
            ↑y = -3 →
              GQ2.HilbertSymbol.hilbertSymbol
                  (GQ2.HilbertSymbol.unitCoe (-1))
                  (GQ2.HilbertSymbol.unitCoe y) =
                1) ∧
          GQ2.HilbertSymbol.hilbertSymbol GQ2.HilbertSymbol.unit2
                GQ2.HilbertSymbol.unit2 =
              1 ∧
            ∀ (y : ℤ_[2]ˣ),
              ↑y = -3 →
                GQ2.HilbertSymbol.hilbertSymbol
                    (GQ2.HilbertSymbol.unitCoe y)
                    (GQ2.HilbertSymbol.unitCoe y) =
                  1

theorem GQ2.SectionThree.lemma_3_5_hilbert_ledger :
  GQ2.HilbertSymbol.hilbertSymbol
        (GQ2.HilbertSymbol.unitCoe (-1))
        (GQ2.HilbertSymbol.unitCoe (-1)) =
      -1 ∧
    (∀ (y : ℤ_[2]ˣ),
        ↑y = -3 →
          GQ2.HilbertSymbol.hilbertSymbol
              GQ2.HilbertSymbol.unit2
              (GQ2.HilbertSymbol.unitCoe
                y) =
            -1) ∧
      GQ2.HilbertSymbol.hilbertSymbol
            (GQ2.HilbertSymbol.unitCoe
              (-1))
            GQ2.HilbertSymbol.unit2 =
          1 ∧
        (∀ (y : ℤ_[2]ˣ),
            ↑y = -3 →
              GQ2.HilbertSymbol.hilbertSymbol
                  (GQ2.HilbertSymbol.unitCoe
                    (-1))
                  (GQ2.HilbertSymbol.unitCoe
                    y) =
                1) ∧
          GQ2.HilbertSymbol.hilbertSymbol
                GQ2.HilbertSymbol.unit2
                GQ2.HilbertSymbol.unit2 =
              1 ∧
            ∀ (y : ℤ_[2]ˣ),
              ↑y = -3 →
                GQ2.HilbertSymbol.hilbertSymbol
                    (GQ2.HilbertSymbol.unitCoe
                      y)
                    (GQ2.HilbertSymbol.unitCoe
                      y) =
                  1

**Lemma 3.5, Hilbert-symbol ledger** (the "initial form" clause in symbol vocabulary):
on the square-class basis `(−1, 2, −3)` of Lemma 3.5, the dyadic Hilbert symbol takes the
values `(−1,−1)₂ = −1`, `(2,−3)₂ = −1`, and `+1` on every other (unordered) pair.  In the
dual basis `(α, β, γ)` of `H¹(D, 𝔽₂)` this is exactly the quadratic initial form
`α² + βγ + γβ` — the degree-two initial form of `r₀ = A²S⁴[S,Y]` (design note §3.5 for the
dictionary; the Kummer-cocycle cup reading enters at §6).  The proof consists of six evaluations
of `hilbertSymbol_dyadic`.

Proof for Lemma 4.4

uses 1

Proved in §3 of the paper. Ingredients: Proposition 1.7.

Proposition4.5

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Remark 3.6 of the paper (Why the orientation cannot be omitted).

An un-oriented marked-relator normalization with only the abelianized relation and quadratic initial form is false. Let F=\langle A,S,Y\rangle_{\mathrm{pro}-2} and define

\psi(A)=AY^{-4}, \qquad \psi(S)=SY^2, \qquad \psi(Y)=Y.

This is an automorphism, with inverse A\mapsto AY^4, S\mapsto SY^{-2}, Y\mapsto Y. For r_0=A^2S^4[S,Y], put r=\psi^{-1}(r_0). On the free abelianization,

\psi_{\mathrm{ab}}(2\bar A+4\bar S) =2(\bar A-4\bar Y)+4(\bar S+2\bar Y) =2\bar A+4\bar S.

Moreover

r=(AY^4)^2(SY^{-2})^4[SY^{-2},Y],

so, modulo the third Zassenhaus term, its initial form is A^2+[S,Y]. Thus r has the same abelianized relation and quadratic initial form as r_0, and its quotient is abstractly D_0. However, under the isomorphism induced by \psi, the transported canonical orientation takes S to \eta^2\ne1. Therefore no isomorphism from this quotient to D_0 which is the identity on B_{\mathrm{ab}} can exist. The orientation-preserving lifting statement Proposition 3.9, rather than the false un-oriented normalization, is the exact structural input needed below.

Lean code for Proposition4.5●1 definition

structure(11 fields)defined in GQ2/PeripheralAction.lean

complete

structure GQ2.PeripheralCyclotomicAction : Type

structure GQ2.PeripheralCyclotomicAction : Type

**Lemma 3.6 (B8), bundled.**  The cyclotomic action on the peripheral generators of
`Δ = maxPro2(F₂)`: a 2-adic cyclotomic exponent embedding `ι` and, for each `u ∈ ℤ₂ˣ`, a continuous
automorphism `aut u` of `Δ` sending each peripheral generator to the corresponding cyclotomic
conjugate.  See the module docstring for the faithfulness deviation (no `π₁`) and the pinning of
`ι`.  Conjugation convention `x ^ c = c⁻¹ x c` (`GQ2.conjP`, matching `GQ2/Words.lean`).

Fields

ι : ℤ_[2]ˣ → ↑GQ2.Zhat.toProfinite.toTop

The 2-adic cyclotomic exponent embedding `ℤ₂ˣ → ℤ̂` (`ι(u) ≡ u` on the pro-2 part, `≡ 0` on
the odd part).

hι_cont : Continuous self.ι

`ι` is continuous.

hι_one : self.ι 1 = GQ2.omega2

`ι(1) = ω₂`: the `u = 1` cyclotomic exponent is the idempotent of the profinite-exponentiation API (so `P ^ᶻ ι 1 = P` on
the pro-2 group `Δ`).

hι_proj : ∀ (u : ℤ_[2]ˣ), GQ2.zhatProjTwo (self.ι u) = Multiplicative.ofAdd ↑u

**`ι(u) ≡ u` on the pro-2 part** (see the module docstring): the canonical
projection `ℤ̂ → ℤ₂` sends `ι u` to `u`.  This is what makes `x ^ᶻ ι u` the `u`-th 2-adic power
on every pro-2 group (`zpowHat_eq_zpowZtwo`).

aut : ℤ_[2]ˣ → ↑GQ2.Delta.toProfinite.toTop ≃ₜ* ↑GQ2.Delta.toProfinite.toTop

The continuous automorphism `φ_u` of `Δ` induced by `u ∈ ℤ₂ˣ`.

cP : ℤ_[2]ˣ → ↑GQ2.Delta.toProfinite.toTop

The conjugator `c_P(u)` for the generator `P`.

cT : ℤ_[2]ˣ → ↑GQ2.Delta.toProfinite.toTop

The conjugator `c_T(u)` for the generator `T`.

cC : ℤ_[2]ˣ → ↑GQ2.Delta.toProfinite.toTop

The conjugator `c_C(u)` for the generator `C`.

hP : ∀ (u : ℤ_[2]ˣ), (self.aut u) GQ2.deltaP = GQ2.conjP (GQ2.zpowHat GQ2.deltaP (self.ι u)) (self.cP u)

`φ_u(P) = c_P⁻¹ · P^u · c_P`.

hT : ∀ (u : ℤ_[2]ˣ), (self.aut u) GQ2.deltaT = GQ2.conjP (GQ2.zpowHat GQ2.deltaT (self.ι u)) (self.cT u)

`φ_u(T) = c_T⁻¹ · T^u · c_T`.

hC : ∀ (u : ℤ_[2]ˣ), (self.aut u) GQ2.deltaC = GQ2.conjP (GQ2.zpowHat GQ2.deltaC (self.ι u)) (self.cC u)

`φ_u(C) = c_C⁻¹ · C^u · c_C`.

Lemma4.6

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma 3.7 of the paper (Cyclotomic powering of the three peripheral classes).

Let

\Delta=\langle P,T\rangle_{\mathrm{pro}-2}, \qquad C=(PT)^{-1}.

For every u\in\mathbb{Z}_2^\times there are an automorphism \varphi_u\in\Aut(\Delta) and elements c_P,c_T,c_C\in\Delta such that

\varphi_u(P)=c_P^{-1}P^u c_P, \qquad \varphi_u(T)=c_T^{-1}T^u c_T, \qquad \varphi_u(C)=c_C^{-1}C^u c_C.

Lean code for Lemma4.6●1 theorem

theoremdefined in GQ2/AnabelianBridge/Construction.lean

complete

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

theorem GQ2.SectionThree.lemma_3_7
  (B : GQ2.SectionThree.BDecomposition)
  (u : ℤ_[2]ˣ) :
  ∃ Ψ,
    B.e
          (GQ2.SectionThree.abMk
            (Ψ GQ2.d0A)) =
        Multiplicative.ofAdd
          (1, -2 * ↑u, 0) ∧
      B.e
          (GQ2.SectionThree.abMk
            (Ψ GQ2.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`).

Proof for Lemma 4.6

Proof uses 2

Proof dependency previews

Preview

Proposition 1.8

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §3 of the paper. Ingredients: Proposition 1.8 Proposition 4.5.

Lemma4.7

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 1✓L∃∀N

Lemma 3.8 of the paper (Square-root and HNN lifting).

For every u\in\mathbb{Z}_2^\times there is an automorphism \Psi_u\in\Aut(D_0) such that, on B_{\mathrm{ab}},

\bar A\longmapsto u\bar A, \qquad \bar S\longmapsto u\bar S.

Lean code for Lemma4.7●2 theorems

theoremdefined in GQ2/AnabelianBridge/Classification.lean

complete

theorem GQ2.SectionThree.prop_3_8_classification
  (B : GQ2.SectionThree.BDecomposition)
  (ξ :
    GQ2.topAbelianization ↑GQ2.D0.toProfinite.toTop ≃ₜ*
      GQ2.topAbelianization ↑GQ2.D0.toProfinite.toTop)
  (χ : GQ2.topAbelianization ↑GQ2.D0.toProfinite.toTop →* ℤ_[2]ˣ)
  (hχ : Continuous ⇑χ) (hχA : χ (GQ2.SectionThree.abMk GQ2.d0A) = -1)
  (hχS : χ (GQ2.SectionThree.abMk GQ2.d0S) = 1)
  (hχY :
    ∀ (y : ℤ_[2]ˣ), ↑y = -3 → χ (GQ2.SectionThree.abMk GQ2.d0Y) = y⁻¹)
  (hpres :
    ∀ (x : GQ2.topAbelianization ↑GQ2.D0.toProfinite.toTop),
      χ (ξ x) = χ x) :
  ∃! p,
    B.e (ξ (GQ2.SectionThree.abMk GQ2.d0A)) =
        Multiplicative.ofAdd (1, -2 * ↑p.1, 0) ∧
      B.e (ξ (GQ2.SectionThree.abMk GQ2.d0S)) =
          Multiplicative.ofAdd (0, ↑p.1, 0) ∧
        B.e (ξ (GQ2.SectionThree.abMk GQ2.d0Y)) =
          Multiplicative.ofAdd (0, p.2, 1)

theorem GQ2.SectionThree.prop_3_8_classification
  (B : GQ2.SectionThree.BDecomposition)
  (ξ :
    GQ2.topAbelianization
        ↑GQ2.D0.toProfinite.toTop ≃ₜ*
      GQ2.topAbelianization
        ↑GQ2.D0.toProfinite.toTop)
  (χ :
    GQ2.topAbelianization
        ↑GQ2.D0.toProfinite.toTop →*
      ℤ_[2]ˣ)
  (hχ : Continuous ⇑χ)
  (hχA :
    χ (GQ2.SectionThree.abMk GQ2.d0A) =
      -1)
  (hχS :
    χ (GQ2.SectionThree.abMk GQ2.d0S) = 1)
  (hχY :
    ∀ (y : ℤ_[2]ˣ),
      ↑y = -3 →
        χ
            (GQ2.SectionThree.abMk
              GQ2.d0Y) =
          y⁻¹)
  (hpres :
    ∀
      (x :
        GQ2.topAbelianization
          ↑GQ2.D0.toProfinite.toTop),
      χ (ξ x) = χ x) :
  ∃! p,
    B.e
          (ξ
            (GQ2.SectionThree.abMk
              GQ2.d0A)) =
        Multiplicative.ofAdd
          (1, -2 * ↑p.1, 0) ∧
      B.e
            (ξ
              (GQ2.SectionThree.abMk
                GQ2.d0S)) =
          Multiplicative.ofAdd
            (0, ↑p.1, 0) ∧
        B.e
            (ξ
              (GQ2.SectionThree.abMk
                GQ2.d0Y)) =
          Multiplicative.ofAdd (0, p.2, 1)

**Proposition 3.8, classification half** (paper (18); statement moved from
`GQ2/SectionThree.lean`, see the pointer there).  Every continuous `χ₀`-preserving automorphism
`ξ` of `B = D₀^{ab}` is `α_{u,b}` for a **unique** `(u, b) ∈ ℤ₂ˣ × ℤ₂`: in the coordinates of
the `B`-decomposition it sends `S̄ ↦ S̄^u`, `Ȳ ↦ S̄^b Ȳ`, and (forced by preservation of the
torsion element `t = Ā S̄²` and the relation `Ā² S̄⁴ = 1`) `Ā ↦ t S̄^{-2u}`.  The `S̄`-exponent
`u` is a unit because the same row analysis applies to `ξ⁻¹`.  Axiom-free: the abelianized `D₀`
and its coordinate frame are concrete.

theoremdefined in GQ2/AnabelianBridge/Construction.lean

complete

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

theorem GQ2.SectionThree.prop_3_8_lift
  (B : GQ2.SectionThree.BDecomposition)
  (u : ℤ_[2]ˣ) (b : ℤ_[2]) :
  ∃ Ψ,
    B.e
          (GQ2.SectionThree.abMk
            (Ψ GQ2.d0A)) =
        Multiplicative.ofAdd
          (1, -2 * ↑u, 0) ∧
      B.e
            (GQ2.SectionThree.abMk
              (Ψ GQ2.d0S)) =
          Multiplicative.ofAdd
            (0, ↑u, 0) ∧
        B.e
            (GQ2.SectionThree.abMk
              (Ψ GQ2.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.

Proof for Lemma 4.7

uses 1

Proved in §3 of the paper. Ingredients: Lemma 4.6.

Proposition4.8

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0

Used by 2

Reverse dependency previews

Preview

Proposition 4.9

Loading preview

Reverse dependency preview content is loaded from the rendered-fragment cache.

✓L∃∀N

Proposition 3.10 of the paper (Maximal pro-2 quotient).

The maximal pro-2 quotient of \GA is

\Pi= \left\langle \sigma,x_0,x_1\;\middle|\; x_0^{\sigma^2}x_0[x_1,\sigma]=1 \right\rangle_{\mathrm{pro-}2}.

The group \Pi is abstractly isomorphic to G_{\Qtwo}(2). Equipped with

\nu_2:\Pi\twoheadrightarrow\mathbb{Z}_2, \qquad \nu_2(\sigma)=1,\quad \nu_2(x_0)=\nu_2(x_1)=0,

it is isomorphic to the fully unramified marked pair (G_{\Qtwo}(2),\nu_{\mathrm{ur}}).

Lean code for Proposition4.8●4 theorems

theoremdefined in GQ2/BoundaryConstruction.lean

complete

theorem GQ2.SectionThree.prop_3_10_gammaA_proved :
  ∃ e,
    e
          ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
            ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.σ)) =
        GQ2.piSigma ∧
      e
            ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
              ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.τ)) =
          1 ∧
        e
              ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.x₀)) =
            GQ2.piX0 ∧
          e
              ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.x₁)) =
            GQ2.piX1

theorem GQ2.SectionThree.prop_3_10_gammaA_proved :
  ∃ e,
    e
          ((GQ2.maxProPMk 2
              ↑GQ2.GammaA.toProfinite.toTop)
            ((GQ2.quotientMk GQ2.NA)
              GQ2.univMarking.σ)) =
        GQ2.piSigma ∧
      e
            ((GQ2.maxProPMk 2
                ↑GQ2.GammaA.toProfinite.toTop)
              ((GQ2.quotientMk GQ2.NA)
                GQ2.univMarking.τ)) =
          1 ∧
        e
              ((GQ2.maxProPMk 2
                  ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA)
                  GQ2.univMarking.x₀)) =
            GQ2.piX0 ∧
          e
              ((GQ2.maxProPMk 2
                  ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA)
                  GQ2.univMarking.x₁)) =
            GQ2.piX1

**Prop 3.10, `Γ_A` half** (proved): the maximal pro-`2` quotient of `Γ_A` is `Π`, matching
the marked generators.

theoremdefined in GQ2/LocalMarked.lean

complete

theorem GQ2.SectionThree.prop_3_10_local_marked_proved
  [CompactSpace GQ2.AbsGalQ2] [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (R : GQ2.LocalReciprocity) :
  ∃ ι,
    ι GQ2.ztwoOne = Multiplicative.ofAdd ↑1 ∧
      ∃ e,
        ∀ (g : GQ2.AbsGalQ2),
          R.nu_ur (GQ2.toAb g) =
            ι (GQ2.nuTwo (e ((GQ2.maxProPMk 2 GQ2.AbsGalQ2) g)))

theorem GQ2.SectionThree.prop_3_10_local_marked_proved
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (R : GQ2.LocalReciprocity) :
  ∃ ι,
    ι GQ2.ztwoOne =
        Multiplicative.ofAdd ↑1 ∧
      ∃ e,
        ∀ (g : GQ2.AbsGalQ2),
          R.nu_ur (GQ2.toAb g) =
            ι
              (GQ2.nuTwo
                (e
                  ((GQ2.maxProPMk 2
                      GQ2.AbsGalQ2)
                    g)))

**Prop 3.10, local half** (proved): the boundary group `Π` with `ν₂` is the fully unramified
marked pair `(G_{ℚ₂}(2), ν_ur)`.

theoremdefined in GQ2/SectionThreeMarked.lean

complete

theorem GQ2.SectionThree.prop_3_10_gammaA :
  ∃ e,
    e
          ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
            ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.σ)) =
        GQ2.piSigma ∧
      e
            ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
              ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.τ)) =
          1 ∧
        e
              ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.x₀)) =
            GQ2.piX0 ∧
          e
              ((GQ2.maxProPMk 2 ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA) GQ2.univMarking.x₁)) =
            GQ2.piX1

theorem GQ2.SectionThree.prop_3_10_gammaA :
  ∃ e,
    e
          ((GQ2.maxProPMk 2
              ↑GQ2.GammaA.toProfinite.toTop)
            ((GQ2.quotientMk GQ2.NA)
              GQ2.univMarking.σ)) =
        GQ2.piSigma ∧
      e
            ((GQ2.maxProPMk 2
                ↑GQ2.GammaA.toProfinite.toTop)
              ((GQ2.quotientMk GQ2.NA)
                GQ2.univMarking.τ)) =
          1 ∧
        e
              ((GQ2.maxProPMk 2
                  ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA)
                  GQ2.univMarking.x₀)) =
            GQ2.piX0 ∧
          e
              ((GQ2.maxProPMk 2
                  ↑GQ2.GammaA.toProfinite.toTop)
                ((GQ2.quotientMk GQ2.NA)
                  GQ2.univMarking.x₁)) =
            GQ2.piX1

**Prop. 3.10, `Γ_A` half**: the maximal pro-2 quotient of `Γ_A` is `Π`, canonically —
the isomorphism matches the marked generators (`σ ↦ σ`, `x₀ ↦ x₀`, `x₁ ↦ x₁`; `τ` dies).
The proof is the word-collapse computation above, through the profinite-exponentiation API and
the literal `Γ_A` construction.

theoremdefined in GQ2/SectionThreeMarked.lean

complete

theorem GQ2.SectionThree.prop_3_10_local_marked [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (R : GQ2.LocalReciprocity) :
  ∃ ι,
    ι GQ2.ztwoOne = Multiplicative.ofAdd ↑1 ∧
      ∃ e,
        ∀ (g : GQ2.AbsGalQ2),
          R.nu_ur (GQ2.toAb g) =
            ι (GQ2.nuTwo (e ((GQ2.maxProPMk 2 GQ2.AbsGalQ2) g)))

theorem GQ2.SectionThree.prop_3_10_local_marked
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (R : GQ2.LocalReciprocity) :
  ∃ ι,
    ι GQ2.ztwoOne =
        Multiplicative.ofAdd ↑1 ∧
      ∃ e,
        ∀ (g : GQ2.AbsGalQ2),
          R.nu_ur (GQ2.toAb g) =
            ι
              (GQ2.nuTwo
                (e
                  ((GQ2.maxProPMk 2
                      GQ2.AbsGalQ2)
                    g)))

**Prop. 3.10, local half = Cor. 3.12 (fully marked form)**: `(Π, ν₂)` is isomorphic to
the fully unramified marked pair `(G_{ℚ₂}(2), ν_ur)`.  The `ℤ₂`-identification between the
two `ν`-targets (`Ztwo = maxProPQuotient 2 ℤ̂` on the boundary side, `Multiplicative ℤ₂` on
the B5 side) is quantified explicitly as a continuous isomorphism `ι` pinned by
`ι(1) = ofAdd 1`; the `ν_ur`-values are read through arbitrary lifts, as in `prop_1_1`.
The proof combines Prop. 1.1, the Nielsen transform (23)/(24) of Prop. 3.11, and the
`Ztwo ≅ ℤ₂` bridge.

Proof for Proposition 4.8

Proof uses 2

Proof dependency previews

Preview

Proposition 2.1

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §3 of the paper. Ingredients: Lemma 4.1 Proposition 2.1.

Proposition4.9

Group: The tame and maximal pro-2 quotients (8)

Group member previews

Preview

Lemma 4.1

Loading preview

Group member preview content is loaded from the rendered-fragment cache.

uses 0used by 0✓L∃∀N

Proposition 3.14 of the paper (Fully marked tame and pro-2 quotients).

Let

\nu_{\mathrm t}:\TA\twoheadrightarrow\mathbb{Z}_2, \qquad \nu_{\mathrm t}(\sigma)=1, \quad \nu_{\mathrm t}(\tau)=0,

and equip \Pi with (21). For each \Gamma\in\{\GA,\GQ\}, the tame quotient map and the maximal pro-2 quotient map may be chosen so that their composites with \nu_{\mathrm t} and \nu_2 are the same natural unramified character

\nu_{\Gamma}:\Gamma\twoheadrightarrow\mathbb{Z}_2.

The compatibility therefore holds after passage to every finite quotient C_{2^m}, not only modulo 2.

Lean code for Proposition4.9●2 theorems

theoremdefined in GQ2/BoundaryMapsWitness.lean

complete

theorem GQ2.SectionThree.prop_3_14_proved [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] : Nonempty GQ2.BoundaryMaps

theorem GQ2.SectionThree.prop_3_14_proved
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace
      GQ2.AbsGalQ2] :
  Nonempty GQ2.BoundaryMaps

**Prop. 3.14**: the eq. (27) boundary data exists.

theoremdefined in GQ2/SectionThreeMarked.lean

complete

theorem GQ2.SectionThree.prop_3_14 [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] : Nonempty GQ2.BoundaryMaps

theorem GQ2.SectionThree.prop_3_14
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace
      GQ2.AbsGalQ2] :
  Nonempty GQ2.BoundaryMaps

**Prop. 3.14** (with Cor. 3.12 supplying the `G_{ℚ₂}`-side): the eq. (27) boundary data
exists — tame and maximal pro-2 quotient maps for both sources, `ν`-compatible, jointly
surjective onto the fibred boundary, with the `Γ_A`-side taking the marked generator values
and the `G_{ℚ₂}`-side pinned intrinsically (Lemma 3.3 2-core kernel; `proPKernel` kernel).
The construction instantiates `BoundaryMaps` from Prop. 3.2 and Prop. 1.1.

Proof for Proposition 4.9

Proof uses 2

Proof dependency previews

Preview

Proposition 4.2

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §3 of the paper. Ingredients: Proposition 4.8 Proposition 4.2.