def Q2Presentation.TorsorProgram.quotientPiY (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) : Yt.Y ⧸ N →* Yt.H

The tame quotient map descends (its kernel L_Y contains N).

Equations

• Q2Presentation.TorsorProgram.quotientPiY Yt N hNLY = QuotientGroup.lift N Yt.piY ⋯

@[simp]

theorem Q2Presentation.TorsorProgram.quotientPiY_mk (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (y : Yt.Y) : (quotientPiY Yt N hNLY) ((QuotientGroup.mk' N) y) = Yt.piY y

def Q2Presentation.TorsorProgram.quotientTheta (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) : Yt.Y ⧸ N →* Multiplicative Yt.E

The decoration descends.

Equations

• Q2Presentation.TorsorProgram.quotientTheta Yt N hNθ = QuotientGroup.lift N Yt.thetaY ⋯

@[simp]

theorem Q2Presentation.TorsorProgram.quotientTheta_mk (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) (y : Yt.Y) : (quotientTheta Yt N hNθ) ((QuotientGroup.mk' N) y) = Yt.thetaY y

def Q2Presentation.TorsorProgram.quotientFramedTarget (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) : BoundaryFramedTarget

The quotient framed target Y/N (same H, same E, image wild kernel).

Equations

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

def Q2Presentation.TorsorProgram.quotientFrame (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) (F : BoundaryFrame Yt) : BoundaryFrame (quotientFramedTarget Yt N hNLY hNθ)

The frame transports verbatim (H, E, α, ψ, β unchanged).

Equations

• Q2Presentation.TorsorProgram.quotientFrame Yt N hNLY hNθ F = { alpha := F.alpha, alpha_surj := ⋯, psi := F.psi, beta := F.beta, beta_def := ⋯ }

T1b: restriction of framed surjections along the projection

def Q2Presentation.TorsorProgram.projHom (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] : ProfiniteGrp.ofFiniteGrp (FiniteGrp.of Yt.Y) ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (Yt.Y ⧸ N))

The projection as a hom of profinite groups (finite discrete objects).

Equations

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

@[simp]

theorem Q2Presentation.TorsorProgram.projHom_apply (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (y : Yt.Y) : (ProfiniteGrp.Hom.hom (projHom Yt N)) y = (QuotientGroup.mk' N) y

def Q2Presentation.TorsorProgram.restrictSurj (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (fs : boundaryFramedSurj B Yt F) : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)

Restriction: a parent-framed surjection restricts to a child-framed one.

Equations

• Q2Presentation.TorsorProgram.restrictSurj Yt N hNLY hNθ B F fs = ⟨{ hom := CategoryTheory.CategoryStruct.comp (↑fs).hom (Q2Presentation.TorsorProgram.projHom Yt N), surj := ⋯ }, ⋯⟩

@[simp]

theorem Q2Presentation.TorsorProgram.restrictSurj_hom_apply (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (fs : boundaryFramedSurj B Yt F) (γ : ↑Γ.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (↑(restrictSurj Yt N hNLY hNθ B F fs)).hom) γ = (QuotientGroup.mk' N) ((ProfiniteGrp.Hom.hom (↑fs).hom) γ)

T1c: lift fibres and the difference cocycle

def Q2Presentation.TorsorProgram.liftFibre (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) : Type

The fibre of the restriction over a child-framed surjection.

Equations

• Q2Presentation.TorsorProgram.liftFibre Yt N hNLY hNθ B F g = { fs : Q2Presentation.boundaryFramedSurj B Yt F // Q2Presentation.TorsorProgram.restrictSurj Yt N hNLY hNθ B F fs = g }

theorem Q2Presentation.TorsorProgram.lift_difference_mem (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) (f₀ f₁ : liftFibre Yt N hNLY hNθ B F g) (γ : ↑Γ.toProfinite.toTop) : ((ProfiniteGrp.Hom.hom (↑↑f₀).hom) γ)⁻¹ * (ProfiniteGrp.Hom.hom (↑↑f₁).hom) γ ∈ N

Two lifts of the same child map differ pointwise by elements of N.

theorem Q2Presentation.TorsorProgram.lift_difference_cocycle (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) (f₀ f₁ : liftFibre Yt N hNLY hNθ B F g) (γ γ' : ↑Γ.toProfinite.toTop) : ((ProfiniteGrp.Hom.hom (↑↑f₀).hom) (γ * γ'))⁻¹ * (ProfiniteGrp.Hom.hom (↑↑f₁).hom) (γ * γ') = ((ProfiniteGrp.Hom.hom (↑↑f₀).hom) γ')⁻¹ * (((ProfiniteGrp.Hom.hom (↑↑f₀).hom) γ)⁻¹ * (ProfiniteGrp.Hom.hom (↑↑f₁).hom) γ) * (ProfiniteGrp.Hom.hom (↑↑f₀).hom) γ' * (((ProfiniteGrp.Hom.hom (↑↑f₀).hom) γ')⁻¹ * (ProfiniteGrp.Hom.hom (↑↑f₁).hom) γ')

The difference cocycle law: with z γ := f₀(γ)⁻¹ f₁(γ) ∈ N, z(γγ') = (f₀ γ')⁻¹ · z γ · f₀ γ' · z γ' (a 1-cocycle for the conjugation action through the base lift).

T1d: the all-lifts set and the Z¹-bijection

def Q2Presentation.TorsorProgram.liftHom (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) : Type

All framed lifts of a child-framed surjection (surjectivity NOT imposed; the Frattini argument recovers it per use-site).

Equations

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

def Q2Presentation.TorsorProgram.Z1 (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) (f₀ : liftHom Yt N hNLY hNθ B F g) : Type

The twisted cocycle set relative to a base lift.

Equations

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

theorem Q2Presentation.TorsorProgram.qYMap_mul_mem (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) (y n : Yt.Y) (hn : n ∈ N) : Yt.qYMap (y * n) = Yt.qYMap y

Framing is insensitive to N-translation.

noncomputable def Q2Presentation.TorsorProgram.liftHom_equiv_Z1 (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) (f₀ : liftHom Yt N hNLY hNθ B F g) : liftHom Yt N hNLY hNθ B F g ≃ Z1 Yt N hNLY hNθ B F g f₀

The counting bijection: lifts of g biject with twisted cocycles.

Equations

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

T1e: the fibration partition and Frattini identification

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

Extensionality for surjective continuous homs (local copy).

noncomputable def Q2Presentation.TorsorProgram.framedSurj_equiv_sigma_fibre (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) : boundaryFramedSurj B Yt F ≃ (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) × liftFibre Yt N hNLY hNθ B F g

Fibration partition: parent framed surjections form the total space of the lift fibres over the child ones.

Equations

• Q2Presentation.TorsorProgram.framedSurj_equiv_sigma_fibre Yt N hNLY hNθ B F = (Equiv.sigmaFiberEquiv (Q2Presentation.TorsorProgram.restrictSurj Yt N hNLY hNθ B F)).symm

noncomputable def Q2Presentation.TorsorProgram.liftFibre_equiv_liftHom (Yt : BoundaryFramedTarget) (N : Subgroup Yt.Y) [hNn : N.Normal] (hNLY : N ≤ Yt.LY) (hNθ : ∀ n ∈ N, Yt.thetaY n = 1) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (hgen : ∀ (J : Subgroup Yt.Y), Subgroup.map (QuotientGroup.mk' N) J = ⊤ → J = ⊤) (g : boundaryFramedSurj B (quotientFramedTarget Yt N hNLY hNθ) (quotientFrame Yt N hNLY hNθ F)) : liftFibre Yt N hNLY hNθ B F g ≃ liftHom Yt N hNLY hNθ B F g

Frattini-conditional identification: if N is non-generating, every framed lift is automatically surjective, so fibres and all-lifts agree.

Equations

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