theorem Q2Presentation.Induction.TerminalBridge.surjContHom_ext {P Q : ProfiniteGrp.{0}} {f g : Profinite.SurjContHom P Q} (h : f.hom = g.hom) : f = g

Extensionality for surjective continuous homs.

@[reducible, inline]

abbrev Q2Presentation.Induction.TerminalBridge.QObj (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] : ProfiniteGrp.{0}

The finite quotient object Q = Y/Ñ in ProfiniteGrp.

Equations

• Q2Presentation.Induction.TerminalBridge.QObj Yt N = ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.Y ⧸ N))

def Q2Presentation.Induction.TerminalBridge.rho2 (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] : Yt.Y ⧸ N →* H2grp Yt N

The descent ρ₂ : Q →* H₂.

Equations

• Q2Presentation.Induction.TerminalBridge.rho2 Yt N = QuotientGroup.map N (N ⊔ Yt.LY) (MonoidHom.id Yt.Y) ⋯

@[simp]

theorem Q2Presentation.Induction.TerminalBridge.rho2_mk (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (y : Yt.Y) : (rho2 Yt N) ((QuotientGroup.mk' N) y) = (QuotientGroup.mk' (N ⊔ Yt.LY)) y

def Q2Presentation.Induction.TerminalBridge.CompatQbar (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) (N : Subgroup Yt.Y) [hNn : N.Normal] (hodd : Odd (Nat.card ↥N)) (hidx : ∃ (k : ℕ), N.index = 2 ^ k) : Type

The source-independent comparison set.

Equations

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

theorem Q2Presentation.Induction.TerminalBridge.framing_components (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (fs : boundaryFramedSurj B Yt F) (γ : ↑Γ.toProfinite.toTop) : Yt.piY ((ProfiniteGrp.Hom.hom (↑fs).hom) γ) = (ProfiniteGrp.Hom.hom F.alpha) ((ProfiniteGrp.Hom.hom B.tameMap) γ) ∧ Yt.thetaY ((ProfiniteGrp.Hom.hom (↑fs).hom) γ) = (ProfiniteGrp.Hom.hom F.psi) ((ProfiniteGrp.Hom.hom B.pro2Map) γ)

The two components of the framing condition.

def Q2Presentation.Induction.TerminalBridge.qComposite (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) (N : Subgroup Yt.Y) [hNn : N.Normal] {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (fs : boundaryFramedSurj B Yt F) : Γ ⟶ QObj Yt N

The Q-composite of a framed surjection, as a hom.

Equations

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

@[simp]

theorem Q2Presentation.Induction.TerminalBridge.qComposite_apply (Yt : BoundaryFramedTarget) (F : BoundaryFrame Yt) (N : Subgroup Yt.Y) [hNn : N.Normal] {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (fs : boundaryFramedSurj B Yt F) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (qComposite Yt F N B fs)) γ = (QuotientGroup.mk' N) ((ProfiniteGrp.Hom.hom (↑fs).hom) γ)

def Q2Presentation.Induction.TerminalBridge.fwd (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) (fs : boundaryFramedSurj B Yt F) : CompatQbar Yt F N hodd hidx

Forward: a framed surjection yields a compatible Π-level map.

Equations

• Q2Presentation.Induction.TerminalBridge.fwd Yt F N hodd hidx B hfact fs = ⟨⋯.choose, ⋯⟩

The backward reconstruction

theorem Q2Presentation.Induction.TerminalBridge.pair_exists_unique (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 Γ) (qc : CompatQbar Yt F N hodd hidx) (γ : ↑Γ.toProfinite.toTop) : ∃! y : Yt.Y, Yt.piY y = (ProfiniteGrp.Hom.hom F.alpha) ((ProfiniteGrp.Hom.hom B.tameMap) γ) ∧ (QuotientGroup.mk' N) y = (ProfiniteGrp.Hom.hom ↑qc) ((ProfiniteGrp.Hom.hom B.pro2Map) γ)

The pointwise fibre-pair witness exists uniquely.

def Q2Presentation.Induction.TerminalBridge.bwdFun (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 Γ) (qc : CompatQbar Yt F N hodd hidx) : ↑Γ.toProfinite.toTop → Yt.Y

The reconstructed function.

Equations

• Q2Presentation.Induction.TerminalBridge.bwdFun Yt F N hodd hidx B qc γ = ⋯.choose

theorem Q2Presentation.Induction.TerminalBridge.bwdFun_spec (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 Γ) (qc : CompatQbar Yt F N hodd hidx) (γ : ↑Γ.toProfinite.toTop) : Yt.piY (bwdFun Yt F N hodd hidx B qc γ) = (ProfiniteGrp.Hom.hom F.alpha) ((ProfiniteGrp.Hom.hom B.tameMap) γ) ∧ (QuotientGroup.mk' N) (bwdFun Yt F N hodd hidx B qc γ) = (ProfiniteGrp.Hom.hom ↑qc) ((ProfiniteGrp.Hom.hom B.pro2Map) γ)

theorem Q2Presentation.Induction.TerminalBridge.bwdFun_uniq (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 Γ) (qc : CompatQbar Yt F N hodd hidx) (γ : ↑Γ.toProfinite.toTop) (y : Yt.Y) (hy : Yt.piY y = (ProfiniteGrp.Hom.hom F.alpha) ((ProfiniteGrp.Hom.hom B.tameMap) γ) ∧ (QuotientGroup.mk' N) y = (ProfiniteGrp.Hom.hom ↑qc) ((ProfiniteGrp.Hom.hom B.pro2Map) γ)) : bwdFun Yt F N hodd hidx B qc γ = y

def Q2Presentation.Induction.TerminalBridge.bwd (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 Γ) (qc : CompatQbar Yt F N hodd hidx) : boundaryFramedSurj B Yt F

Backward: a compatible Π-level map reconstructs a framed surjection.

Equations

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

@[simp]

theorem Q2Presentation.Induction.TerminalBridge.bwd_hom_apply (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 Γ) (qc : CompatQbar Yt F N hodd hidx) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (↑(bwd Yt F N hodd hidx B qc)).hom) γ = bwdFun Yt F N hodd hidx B qc γ