def Q2Presentation.Induction.TerminalBridge.framedSurjEquiv (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) (N : Subgroup Yt.Y) [hNn : N.Normal] (hodd : Odd (Nat.card ↥N)) (hidx : ∃ (k : ℕ), N.index = 2 ^ k) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (hfact : ∀ (g : Γ ⟶ QObj Yt N), ∃! gbar : PiGrp ⟶ QObj Yt N, CategoryTheory.CategoryStruct.comp B.pro2Map gbar = g) : boundaryFramedSurj B Yt F ≃ CompatQbar Yt F N hodd hidx

The full equivalence for one source.

Equations

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

theorem Q2Presentation.Induction.TerminalBridge.count_eq (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) (N : Subgroup Yt.Y) [hNn : N.Normal] (hodd : Odd (Nat.card ↥N)) (hidx : ∃ (k : ℕ), N.index = 2 ^ k) (hfactA : ∀ (g : GammaA ⟶ QObj Yt N), ∃! gbar : PiGrp ⟶ QObj Yt N, CategoryTheory.CategoryStruct.comp boundaryPackage_GammaA.pro2Map gbar = g) (hfactQ : ∀ (g : GQ2Profinite ⟶ QObj Yt N), ∃! gbar : PiGrp ⟶ QObj Yt N, CategoryTheory.CategoryStruct.comp boundaryPackage_GQ2.pro2Map gbar = g) : Cardinal.mk (boundaryFramedSurj boundaryPackage_GammaA Yt F) = Cardinal.mk (boundaryFramedSurj boundaryPackage_GQ2 Yt F)

The terminal count equality over any terminal-reduction data.