-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathSectionTenSources.lean
More file actions
139 lines (111 loc) · 6.18 KB
/
Copy pathSectionTenSources.lean
File metadata and controls
139 lines (111 loc) · 6.18 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
/-
Copyright (c) 2026 David Roe. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: David Roe, roed@mit.edu, using Claude Opus-4.8 and Fable-5
-/
import GQ2.SectionTen
import GQ2.ThmFourTwo
import GQ2.BoundaryMapsWitness
import GQ2.TameOrientationWitness
/-!
# §10 — the per-source discharge of Lemma 10.1's hypotheses
`SectionTen.card_contSurj_eq` (Lemma 10.1, counting form) is stated Γ-generically over the two
hypotheses on a boundary map `b`:
* `htame : Function.Surjective (tameCoord b)` — the tame coordinate `pr₁ ∘ b` is onto `Ttame`;
* `hwild : IsProP 2 (tameCoord b).toMonoidHom.ker` — its kernel (the wild inertia) is pro-2.
This file discharges both for the two real sources, so `eq_154` can invoke
`card_contSurj_eq` twice. Since `tameCoord (B.bA) = B.tameA` and `tameCoord (B.bF) = B.tameF`
(`bA_apply_coe`/`bF_apply_coe`):
* **`G_ℚ₂` (F-side) — generic**, straight from the `BoundaryMaps` clauses `tameF_surjective`
(surjectivity) and `wild_isProP` (`= W_F = O₂(G_ℚ₂)` pro-2, Lemma 3.3).
* **`Γ_A` (A-side) — for the concrete `boundaryMapsWitness`**: `tameA := φ_A` is surjective
(`phiA_surjective`), and `ker φ_A = W_A` (the wild core) because the descent
`φ_A / W_A = ψ_W` is injective (`tameAEquiv`, Prop 3.2's `Γ_A`-side iso), which is pro-2 by
`isProP_wildPart`. Thus the A-side needs **no `BoundaryMaps` amendment** — the witness
supplies it.
-/
namespace GQ2
namespace SectionTen
open SectionThree
/-- The tame coordinate of `b_{G_ℚ₂}` is the boundary bundle's tame component `tameF`. -/
theorem tameCoord_bF (B : BoundaryMaps) : tameCoord B.bF = B.tameF := by
ext g; simp only [tameCoord_apply, B.bF_apply_coe]
/-- The tame coordinate of `b_{Γ_A}` is the boundary bundle's tame component `tameA`. -/
theorem tameCoord_bA (B : BoundaryMaps) : tameCoord B.bA = B.tameA := by
ext g; simp only [tameCoord_apply, B.bA_apply_coe]
/-! ## `G_ℚ₂` (F-side): from the `BoundaryMaps` fields -/
/-- **`htame` for `G_ℚ₂`**: `tameF` is onto (`BoundaryMaps.tameF_surjective`). -/
theorem tameCoord_bF_surjective (B : BoundaryMaps) :
Function.Surjective (tameCoord B.bF) := by
rw [tameCoord_bF]; exact B.tameF_surjective
/-- **`hwild` for `G_ℚ₂`**: the wild inertia `ker tameF = O₂(G_ℚ₂)` is pro-2
(`BoundaryMaps.wild_isProP`). -/
theorem tameCoord_bF_ker_isProP (B : BoundaryMaps) :
IsProP 2 (tameCoord B.bF).toMonoidHom.ker := by
rw [tameCoord_bF]; exact B.wild_isProP
/-! ## `Γ_A` (A-side): the kernel of `φ_A` -/
/-- **`ker φ_A = W_A`.** `⊇` is `wildPartB_le_ker_phiA`; `⊆` because the descent
`ψ_W = φ_A / W_A` is injective — it is the underlying map of the Prop-3.2 iso `tameAEquiv`. -/
theorem ker_phiA : phiA.toMonoidHom.ker = wildPartB := by
refine le_antisymm (fun x hx => ?_) wildPartB_le_ker_phiA
have h1 : psiW (quotientMk wildPartB x) = 1 :=
(quotientLift_quotientMk _ _ _ _).trans (MonoidHom.mem_ker.mp hx)
have h2 : quotientMk wildPartB x = 1 :=
tameAEquiv.injective (h1.trans (map_one psiW).symm)
exact (quotientMk_eq_one_iff _).mp h2
/- The concrete `Γ_A` witness `boundaryMapsWitness` (Prop 3.14) lives over `AbsGalQ2`, so its
users carry the tower's standing `AbsGalQ2` topology instances. -/
section Witness
variable [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2]
/-- **`htame` for `Γ_A`** (the witness `boundaryMapsWitness`): `tameA = φ_A` is onto
(`phiA_surjective`). -/
theorem tameCoord_bA_surjective :
Function.Surjective (tameCoord boundaryMapsWitness.bA) := by
rw [tameCoord_bA]; exact phiA_surjective
/-- **`hwild` for `Γ_A`** (the witness): the wild inertia `ker tameA = ker φ_A = W_A` is pro-2
(`isProP_wildPart`). -/
theorem tameCoord_bA_ker_isProP :
IsProP 2 (tameCoord boundaryMapsWitness.bA).toMonoidHom.ker := by
rw [tameCoord_bA]
show IsProP 2 phiA.toMonoidHom.ker
rw [ker_phiA]; exact isProP_wildPart
/-! ## Eq. (154) and the surjection-count theorem
Both live here (not in `SectionTen`) because `eq_154`'s A-side needs the concrete
`boundaryMapsWitness` (`Γ_A`'s tame surjectivity `phiA_surjective` is witness-specific), and
`BoundaryMapsWitness` is downstream of `SectionTen`. The proof then applies the proved
`thm_4_2` frame by frame. -/
/-- **Eq. (154)**: the two sources have identical continuous-surjection counts onto every finite
group. `card_contSurj_eq` at `boundaryMapsWitness.bA`/`.bF` (per-source hypotheses above) rewrites
each count as the sum of the fixed-frame exact-image counts; `thm_4_2` equates them frame-by-frame
(`hE2` trivial on `E₀ = PUnit`). -/
theorem eq_154 (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] :
Nat.card (ContSurj GammaA G) = Nat.card (ContSurj AbsGalQ2 G) := by
have hE2 : ∀ e : E₀, e ^ 2 = 1 := fun _ => Subsingleton.elim _ _
rw [card_contSurj_eq boundaryMapsWitness.bA G tameCoord_bA_surjective
tameCoord_bA_ker_isProP gammaA_topologicallyFinitelyGenerated,
card_contSurj_eq boundaryMapsWitness.bF G (tameCoord_bF_surjective boundaryMapsWitness)
(tameCoord_bF_ker_isProP boundaryMapsWitness)
Foundations.absGalQ2_isTopologicallyFinitelyGenerated]
exact finsum_congr fun α =>
thm_4_2 boundaryMapsWitness (tameFrame α.1 α.2) localReciprocity
tameUnitOrientation_witness (tameTarget G) hE2
/-- **Theorem 1.2, surjection-count form** (`GQ2.main_surjection_count`), proved from eq. (154) +
Prop 2.3. The original `Statement.lean` placeholder was resolved by the statement-move pattern
(Statement is upstream of the tower); the moved statement carries the tower-standing
`AbsGalQ2` instance binders. -/
theorem main_surjection_count'
(G : Type) [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] :
contSurjCount G = admissibleCount G :=
(eq_154 G).symm.trans (prop_2_3 (G := G))
end Witness
end SectionTen
end GQ2
/-! ### Paper-tag ledger (auto-generated by paperforge; do not edit)
* eq. (154) = ⟦eq-app-cup-convention⟧ [≥ drift window; verify against v428 tex]
* Lemma 10.1 = ⟦lem-tameframeexhaustion⟧
* Lemma 3.3 = ⟦lem-o2tame⟧
* Prop 2.3 = ⟦prop-epi-semantics⟧
* Prop 3.14 = ⟦prop-compatiblemarking⟧
* Prop 3.2 = ⟦prop-tamequotient⟧
* Theorem 1.2 = ⟦thm-main⟧
-/