The terminal-case infrastructure for Section 9

The odd-complement, fibre-product, correspondence, and source-independence layers.

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

Terminal-case group-theory foundation

The coprime-centralization mechanism behind Lemma 9.2's odd normal lift Ñ ◁ Y: an odd-order subgroup acting on the scalar stack L_Y (a Y-central 2-group) centralizes it. This is GQ2.comm_bot_of_scalarChain (the Lemma 7.2 proof) unpacked at the IsScalarStack datum.

theorem GQ2.SectionNine.scalarStack_centralized_of_coprime {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (hstack : SectionSeven.IsScalarStack L) {N : Subgroup Y} (hcop : (Nat.card ↥N).Coprime (Nat.card ↥L)) : ⁅N, L⁆ = ⊥

Coprime centralization (Lemma 9.2 mechanism, §9.1): an odd-order subgroup N acting on a scalar stack L (a Y-central 2-group, SectionSeven.IsScalarStack) centralizes it — ⁅N, L⁆ = ⊥. This is how the odd normal lift Ñ of Lemma 9.2 centralizes L_Y (its uniqueness/normality then follow). Proved from comm_bot_of_scalarChain; reusable by the Lemma 9.2 structural subproof the §9 induction.

Tame 2-nilpotency

The gating foundation for Lemma 9.2: a finite quotient H of the tame group Ttame (generated by s, t with s⁻¹ t s = t²) is 2-nilpotent — O²(H) has odd order. ⟨t⟩ is odd (Tame.tame_odd_order) and normal (Tame.zpowers_normal_of_tame), the quotient H ⧸ ⟨t⟩ is cyclic, and a finite group with an odd normal subgroup and cyclic quotient is 2-nilpotent (the odd complement is the preimage of the odd part of the cyclic quotient). This lets the §9 induction build the odd normal lift Ñ ◁ Y via Schur–Zassenhaus (oddOrder_twoQuotient_split).

theorem GQ2.SectionNine.exists_normal_odd_pow_mem_of_cyclic {Q : Type u_1} [Group Q] [Finite Q] (hcyc : IsCyclic Q) : ∃ (Q0 : Subgroup Q), Q0.Normal ∧ Odd (Nat.card ↥Q0) ∧ ∀ (x : Q), ∃ (k : ℕ), x ^ 2 ^ k ∈ Q0

A finite cyclic group Q has a normal subgroup Q₀ of odd order (= ⟨g^{2ᵃ}⟩, the odd part) such that the 2ᵃ-power of every element lands in Q₀ (i.e. Q ⧸ Q₀ is a 2-group, expressed membership-wise to avoid forming the quotient here).

theorem GQ2.SectionNine.exists_normal_odd_twoQuotient_of_cyclic_quotient {H : Type u_1} [Group H] [Finite H] (C : Subgroup H) [C.Normal] (hC : Odd (Nat.card ↥C)) (hcyc : IsCyclic (H ⧸ C)) : ∃ (N : Subgroup H) (x : N.Normal), Odd (Nat.card ↥N) ∧ IsPGroup 2 (H ⧸ N)

2-nilpotency from a cyclic quotient. A finite group H with a normal subgroup C of odd order and cyclic quotient H ⧸ C has a normal subgroup N of odd order with 2-group quotient (necessarily N = O²(H)): the preimage of the odd part of the cyclic H ⧸ C.

theorem GQ2.SectionNine.tame_two_nilpotent {H : Type u_1} [Group H] [Finite H] {s t : H} (hgen : Subgroup.closure {s, t} = ⊤) (h : s⁻¹ * t * s = t ^ 2) : ∃ (N : Subgroup H) (x : N.Normal), Odd (Nat.card ↥N) ∧ IsPGroup 2 (H ⧸ N)

Tame 2-nilpotency (Lemma 3.1 structural content). A finite group generated by s, t with the tame relation s⁻¹ t s = t² is 2-nilpotent: it has a normal subgroup N of odd order with 2-group quotient (N = O²(H)). C = ⟨t⟩ is odd (Tame.tame_odd_order) and normal (Tame.zpowers_normal_of_tame), and H ⧸ C is cyclic (generated by the image of s, since t ↦ 1); apply exists_normal_odd_twoQuotient_of_cyclic_quotient. This is the foundation Lemma 9.2 rests on — the odd normal lift Ñ of the §9 induction lives over O²(H).

Lemma 9.2 — the odd normal complement Ñ ◁ Y

For a terminal target 1 → L_Y → Y → H → 1 (L_Y a scalar-stack 2-group, H tame hence 2-nilpotent by tame_two_nilpotent), Schur–Zassenhaus inside P = π_Y⁻¹(O²H) produces an odd complement Ñ to L_Y, which the scalar-stack centralization (scalarStack_centralized_of_coprime) forces to be normal in Y (Ñ = the odd-order elements of P). The output bundle — Ñ ◁ Y odd, Y/Ñ a 2-group, Ñ ∩ L_Y = ⊥, π_Y(Ñ) = O²H, Ñ·L_Y = π_Y⁻¹(O²H) — is exactly the data the §9 induction feeds to coprime_fiber_product (Lemma 9.1) for Y ≅ H ×_{H₂} (Y/Ñ).

theorem GQ2.SectionNine.sz_odd_complement {H Y : Type} [Group H] [Group Y] [Finite Y] (piY : Y →* H) (hpi : Function.Surjective ⇑piY) (L : Subgroup Y) (hkerL : piY.ker = L) (M : Subgroup H) [M.Normal] (hMcop : (Nat.card ↥L).Coprime (Nat.card ↥M)) : ∃ Ntil ≤ Subgroup.comap piY M, Ntil ⊓ L = ⊥ ∧ Ntil ⊔ L = Subgroup.comap piY M ∧ Nat.card ↥Ntil = Nat.card ↥M

Schur–Zassenhaus: the odd complement Ñ to L inside P = π⁻¹(M), where L = ker π is a 2-group and M ◁ H is odd.

theorem GQ2.SectionNine.lemma_9_2_core {H Y : Type} [Group H] [Group Y] [Finite Y] (piY : Y →* H) (hpi : Function.Surjective ⇑piY) (L : Subgroup Y) (hkerL : piY.ker = L) (hL2 : IsPGroup 2 ↥L) (hstack : SectionSeven.IsScalarStack L) (M : Subgroup H) [M.Normal] (hModd : Odd (Nat.card ↥M)) (hMtwo : IsPGroup 2 (H ⧸ M)) : ∃ (Ntil : Subgroup Y) (x : Ntil.Normal), Odd (Nat.card ↥Ntil) ∧ IsPGroup 2 (Y ⧸ Ntil) ∧ Ntil ⊓ L = ⊥ ∧ ⁅Ntil, L⁆ = ⊥ ∧ Subgroup.map piY Ntil = M ∧ Ntil ⊔ L = Subgroup.comap piY M

Lemma 9.2 (structure). For a marked target 1 → L → Y → H → 1 with L = ker π a 2-group scalar stack and H 2-nilpotent (M = O²H odd, H/M a 2-group), there is a unique odd normal complement Ñ ◁ Y to L over M: Ñ is odd, Y/Ñ is a 2-group, Ñ ∩ L = ⊥, Ñ centralizes L, π(Ñ) = M, and Ñ · L = π⁻¹(M). These are the fibre-product pieces feeding coprime_fiber_product in the §9 induction.

theorem GQ2.SectionNine.head_two_nilpotent {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] (F : BoundaryFrame H E) : ∃ (M : Subgroup H) (x : M.Normal), Odd (Nat.card ↥M) ∧ IsPGroup 2 (H ⧸ M)

The head of a boundary-framed target is 2-nilpotent. H is a finite tame quotient α : Ttame ↠ H (the frame α), so its generators α σ, α τ satisfy the tame relation and generate H; tame_two_nilpotent applies. This discharges the M hypothesis of lemma_9_2_core from the frame.

Lemma 9.2 fibre-product infrastructure

The concrete tools the (144) correspondence runs on, all proved std-3:

• odd_subgroup_le_ker_of_expTwo — θ_Y (decoration to the exponent-2 group E) kills the odd complement Ñ, so it descends to Q = Y/Ñ (L92.thetaBarQ). This is where hE2 enters.
• odd_mem_of_pTwo_quotient — an odd-order element dies in a 2-group quotient (⟹ H₂ = H/O²H is cyclic, the engine of source-independence).
• L92 — a bundle of the lemma_9_2_core outputs; L92.fibreMulEquiv is the fibre-product isomorphism Y ≃* {(h,q) | κ h = λ q} (eq. (143)), built from coprime_fiber_product.

Remaining for terminal_count_eq (the §9 induction): the boundary-lift ↔ Q-count bijection (two more coprime_fiber_product applications for surjectivity) and source-independence of the Q-count (the H₂-values factor through ν_t, so compatA/compatF make the two sources agree).

theorem GQ2.SectionNine.odd_subgroup_le_ker_of_expTwo {Y E : Type} [Group Y] [Finite Y] [Group E] {N : Subgroup Y} (hodd : Odd (Nat.card ↥N)) (hE2 : ∀ (e : E), e ^ 2 = 1) (θ : Y →* E) : N ≤ θ.ker

θ kills the odd complement. A homomorphism from a finite group to an exponent-2 group vanishes on every odd-order normal subgroup. (This is where hE2 enters the terminal case: θ_Y descends to Q = Y/Ñ.)

structure GQ2.SectionNine.L92 (H Y : Type) [Group H] [Group Y] [Finite Y] : Type

Bundle of the lemma_9_2_core outputs, to avoid threading a dozen hypotheses through the fibre-product construction.

• piY : Y →* H
• hpi : Function.Surjective ⇑self.piY
• L : Subgroup Y
• hkerL : self.piY.ker = self.L
• M : Subgroup H
• hMn : self.M.Normal
• hModd : Odd (Nat.card ↥self.M)
• Ntil : Subgroup Y
• hNn : self.Ntil.Normal
• hNodd : Odd (Nat.card ↥self.Ntil)
• hNL : self.Ntil ⊓ self.L = ⊥
• hmapM : Subgroup.map self.piY self.Ntil = self.M
• hNLsup : self.Ntil ⊔ self.L = Subgroup.comap self.piY self.M
• hQ2 : IsPGroup 2 (Y ⧸ self.Ntil)

@[reducible, inline]

abbrev GQ2.SectionNine.L92.Q {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : Type

Q = Y / Ñ.

Equations

• D.Q = (Y ⧸ D.Ntil)

instance GQ2.SectionNine.L92.instNormalNtil {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : D.Ntil.Normal

instance GQ2.SectionNine.L92.instNormalM {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : D.M.Normal

theorem GQ2.SectionNine.L92.ntil_le_ker {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : D.Ntil ≤ ((QuotientGroup.mk' D.M).comp D.piY).ker

Ntil ≤ ker (κ ∘ π_Y) = π_Y⁻¹(M).

noncomputable def GQ2.SectionNine.L92.lamQ {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : D.Q →* H ⧸ D.M

The lower map λ : Q ↠ H/M, descending κ ∘ π_Y.

Equations

• D.lamQ = QuotientGroup.lift D.Ntil ((QuotientGroup.mk' D.M).comp D.piY) ⋯

noncomputable def GQ2.SectionNine.L92.fibreSub {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : Subgroup (H × D.Q)

The fibre product {(h,q) | κ h = λ q} ≤ H × Q.

Equations

• D.fibreSub = ((QuotientGroup.mk' D.M).comp (MonoidHom.fst H D.Q)).eqLocus (D.lamQ.comp (MonoidHom.snd H D.Q))

theorem GQ2.SectionNine.L92.toFibre_mem {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) (y : Y) : (D.piY y, ↑y) ∈ D.fibreSub

(π_Y y, mk' Ntil y) lands in the fibre product.

noncomputable def GQ2.SectionNine.L92.toFibre {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : Y →* ↥D.fibreSub

The map Y → fibre product, y ↦ (π_Y y, mk' Ntil y).

Equations

• D.toFibre = (D.piY.prod (QuotientGroup.mk' D.Ntil)).codRestrict D.fibreSub ⋯

noncomputable def GQ2.SectionNine.L92.fibreMulEquiv {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) : Y ≃* ↥D.fibreSub

The fibre-product isomorphism Y ≃* {(h,q) | κ h = λ q} (Lemma 9.2, eq. (143)).

Equations

• D.fibreMulEquiv = MulEquiv.ofBijective D.toFibre ⋯

noncomputable def GQ2.SectionNine.L92.thetaBarQ {H Y : Type} [Group H] [Group Y] [Finite Y] (D : L92 H Y) {E : Type} [Group E] (θ : Y →* E) (hE2 : ∀ (e : E), e ^ 2 = 1) : D.Q →* E

A decoration θ : Y →* E to an exponent-2 group descends to Q = Y/Ñ (θ kills odd Ñ).

Equations

• D.thetaBarQ θ hE2 = QuotientGroup.lift D.Ntil θ ⋯

The (144) correspondence

Lemma 9.2's fibre product identifies the boundary-framed lifts Γ ↠ Y with a Q-count set (boundaryLifts_equiv_qlifts, source-generic); the maximal-pro-2 universal property then makes that count source-independent (qlifts_equiv_commonLifts), routed through ν-compatibility and b-surjectivity — no marked isomorphism is needed (only prop_3_10_gammaA and ker_pro2F).

theorem GQ2.SectionNine.L92.discreteTopology_Q {H : Type} [Group H] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (D : L92 H Y) : DiscreteTopology D.Q

Q = Y/Ñ is discrete (quotient of a discrete group by an open subgroup).

def GQ2.SectionNine.L92.mkCH {H : Type} [Group H] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] (D : L92 H Y) : Y →ₜ* D.Q

The quotient map Y ↠ Q as a continuous hom.

Equations

• D.mkCH = { toMonoidHom := QuotientGroup.mk' D.Ntil, continuous_toFun := ⋯ }

def GQ2.SectionNine.QLifts {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (D : L92 H Y) (b : Γ →ₜ* ↥boundarySubgroup) : Type

The Q-count set: continuous surjections Γ ↠ Q satisfying the descended boundary conditions (H-part through λ, θ-part through θ̄).

Equations

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

noncomputable def GQ2.SectionNine.qliftHom {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (F : BoundaryFrame H E) (D : L92 H Y) (b : Γ →ₜ* ↥boundarySubgroup) (g : ContSurj Γ D.Q) (h1 : ∀ (γ : Γ), D.lamQ (↑g γ) = (QuotientGroup.mk' D.M) (F.alpha (↑(b γ)).1)) : Γ →ₜ* Y

The reconstruction of a boundary lift f : Γ ↠ Y from a Q-lift g, via the fibre product Y ≅ H ×_{H₂} Q: f γ := fibreMulEquiv.symm (F.alpha (b γ).1, g γ).

Equations

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

theorem GQ2.SectionNine.qliftHom_surjective {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (F : BoundaryFrame H E) (D : L92 H Y) (b : Γ →ₜ* ↥boundarySubgroup) (hb : Function.Surjective ⇑b) (g : ContSurj Γ D.Q) (h1 : ∀ (γ : Γ), D.lamQ (↑g γ) = (QuotientGroup.mk' D.M) (F.alpha (↑(b γ)).1)) : Function.Surjective ⇑(qliftHom F D b g h1)

The reconstructed f = qliftHom … g is surjective (the "second coprime_fiber_product": the range of (γ ↦ (F.alpha (b γ).1, g γ)) is all of the fibre, since it projects onto both H and Q which have coprime kernels). Uses hb (surjectivity of b).

def GQ2.SectionNine.blToQ {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (D : L92 H Y) (hDpi : D.piY = T.piY) (b : Γ →ₜ* ↥boundarySubgroup) (x : BoundaryLifts b F T) : QLifts F T hE2 D b

Forward map of the (144) correspondence: a boundary lift f : Γ ↠ Y descends to the Q-lift mk ∘ f.

Equations

• GQ2.SectionNine.blToQ F T hE2 D hDpi b x = ⟨⟨D.mkCH.comp ↑↑x, ⋯⟩, ⋯⟩

noncomputable def GQ2.SectionNine.qToBl {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (D : L92 H Y) (hDpi : D.piY = T.piY) (b : Γ →ₜ* ↥boundarySubgroup) (hb : Function.Surjective ⇑b) (g : QLifts F T hE2 D b) : BoundaryLifts b F T

Backward map of the (144) correspondence: a Q-lift g reconstructs the boundary lift qliftHom … g via the fibre product.

Equations

• GQ2.SectionNine.qToBl F T hE2 D hDpi b hb g = ⟨⟨GQ2.SectionNine.qliftHom F D b ↑g ⋯, ⋯⟩, ⋯⟩

theorem GQ2.SectionNine.boundaryLifts_equiv_qlifts {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] {Γ : Type} [Group Γ] [TopologicalSpace Γ] (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (D : L92 H Y) (hDpi : D.piY = T.piY) (b : Γ →ₜ* ↥boundarySubgroup) (hb : Function.Surjective ⇑b) : Nat.card (BoundaryLifts b F T) = Nat.card (QLifts F T hE2 D b)

(A) The (144) correspondence (source-generic): the boundary-framed lifts Γ ↠ Y and the Q-count set are in bijection, hence equinumerous. Uses only surjectivity of b.

def GQ2.SectionNine.precompEquiv {A : Type u_1} {B : Type u_2} {Q : Type u_3} [Group A] [TopologicalSpace A] [Group B] [TopologicalSpace B] [Group Q] [TopologicalSpace Q] (ρ : A ≃ₜ* B) : (B →ₜ* Q) ≃ (A →ₜ* Q)

Precomposition with a topological iso is an equivalence of hom-sets.

Equations

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

noncomputable def GQ2.SectionNine.pro2FactorHom {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (pro2 : Γ →ₜ* ↑PiBd.toProfinite.toTop) : ↑(maxProPQuotient 2 Γ).toProfinite.toTop →ₜ* ↑PiBd.toProfinite.toTop

The factoring of pro2 : Γ ↠ Π through the maximal pro-2 quotient of Γ (Π is pro-2, isProP_maxProPQuotient).

Equations

• GQ2.SectionNine.pro2FactorHom pro2 = (GQ2.maxProPHomEquiv GQ2.SectionNine.pro2FactorHom._proof_8).symm pro2

noncomputable def GQ2.SectionNine.pro2Iso {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (pro2 : Γ →ₜ* ↑PiBd.toProfinite.toTop) (hsurj : Function.Surjective ⇑pro2) (hker : pro2.ker = proPKernel 2 Γ) : ↑(maxProPQuotient 2 Γ).toProfinite.toTop ≃ₜ* ↑PiBd.toProfinite.toTop

The maximal pro-2 quotient of Γ is Π (PiBd), via a pro-2 quotient map pro2 whose kernel is exactly proPKernel 2 Γ.

Equations

• GQ2.SectionNine.pro2Iso pro2 hsurj hker = GQ2.continuousMulEquivOfBijective (GQ2.SectionNine.pro2FactorHom pro2) ⋯

noncomputable def GQ2.SectionNine.compPro2Equiv {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [TotallyDisconnectedSpace Γ] (pro2 : Γ →ₜ* ↑PiBd.toProfinite.toTop) (hsurj : Function.Surjective ⇑pro2) (hker : pro2.ker = proPKernel 2 Γ) {Q : Type} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [T2Space Q] [TotallyDisconnectedSpace Q] (hQ : IsProP 2 Q) : (↑PiBd.toProfinite.toTop →ₜ* Q) ≃ (Γ →ₜ* Q)

Precomposition with the pro-2 quotient map is a bijection of hom-sets into a pro-2 group Q: every g : Γ ↠ Q factors uniquely through Π. (The universal property of the maximal pro-2 quotient, transported to Π.)

Equations

• GQ2.SectionNine.compPro2Equiv pro2 hsurj hker hQ = (GQ2.SectionNine.precompEquiv (GQ2.SectionNine.pro2Iso pro2 hsurj hker)).trans (GQ2.maxProPHomEquiv hQ)

def GQ2.SectionNine.CommonLifts {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [Finite Y] (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (D : L92 H Y) : Type

The common Q-count set on Π (source-free): the H-condition is indexed by ∂bd (so it never mentions a source), the θ-condition ranges over all of Π.

Equations

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

theorem GQ2.SectionNine.qlifts_equiv_commonLifts {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (F : BoundaryFrame H E) (T : MarkedTarget H E Y) (hE2 : ∀ (e : E), e ^ 2 = 1) (D : L92 H Y) {Γ : Type} [Group Γ] [TopologicalSpace Γ] [IsTopologicalGroup Γ] [CompactSpace Γ] [T2Space Γ] [TotallyDisconnectedSpace Γ] (b : Γ →ₜ* ↥boundarySubgroup) (hb : Function.Surjective ⇑b) (pro2 : Γ →ₜ* ↑PiBd.toProfinite.toTop) (hpro2 : Function.Surjective ⇑pro2) (hbpro2 : ∀ (γ : Γ), (↑(b γ)).2 = pro2 γ) (hker : pro2.ker = proPKernel 2 Γ) : Nat.card (QLifts F T hE2 D b) = Nat.card (CommonLifts F T hE2 D)

(B) Source-independence (per source): the Q-count for a source Γ (with pro-2 quotient map pro2 presenting Π, hker) equals the source-free count on Π. The H-condition transports through surjectivity of b (hbpro2: the pro-2 component of b is pro2); the θ-condition is already on Π.

theorem GQ2.SectionNine.ker_pro2A (B : BoundaryMaps) : B.pro2A.ker = proPKernel 2 ↑GammaA.toProfinite.toTop

ker pro2A = proPKernel 2 Γ_A for any BoundaryMaps B: pro2A agrees with the prop_3_10_gammaA isomorphism e ∘ maxProPMk on the four marked topological generators, hence equals it, and e is injective.