Elementary kernels

structure Q2Presentation.Lifting.ElementaryKernel (Yt : BoundaryFramedTarget) : Type

A normal subgroup of a framed target that is killed by the decoration, contained in the wild kernel, abelian, and of exponent 2 — the shape of the chief kernels the cochain keeps quantify over.

• N : Subgroup Yt.Y
• normal : self.N.Normal
• le_LY : self.N ≤ Yt.LY
• theta_dies (n : Yt.Y) : n ∈ self.N → Yt.thetaY n = 1
• comm (a b : Yt.Y) : a ∈ self.N → b ∈ self.N → a * b = b * a
• exp2 (n : Yt.Y) : n ∈ self.N → n * n = 1

instance Q2Presentation.Lifting.instNormalYN {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : E.N.Normal

instance Q2Presentation.Lifting.instCommGroupSubtypeYMemSubgroupN {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : CommGroup ↥E.N

Equations

• Q2Presentation.Lifting.instCommGroupSubtypeYMemSubgroupN E = { toGroup := inferInstance, mul_comm := ⋯ }

@[reducible, inline]

abbrev Q2Presentation.Lifting.NAdd {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : Type

The additive F₂-carrier of an elementary kernel.

Equations

• Q2Presentation.Lifting.NAdd E = Additive ↥E.N

instance Q2Presentation.Lifting.instAddCommGroupNAdd {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : AddCommGroup (NAdd E)

Equations

• Q2Presentation.Lifting.instAddCommGroupNAdd E = Additive.addCommGroup

instance Q2Presentation.Lifting.instModuleZModOfNatNatNAdd {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : Module (ZMod 2) (NAdd E)

Equations

• Q2Presentation.Lifting.instModuleZModOfNatNatNAdd E = AddCommGroup.zmodModule ⋯

instance Q2Presentation.Lifting.instFiniteNAddOfY {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) [Finite Yt.Y] : Finite (NAdd E)

theorem Q2Presentation.Lifting.add_self_eq_zero_NAdd {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (x : NAdd E) : x + x = 0

Char-2: every element of the kernel module is 2-torsion.

The conjugation operators

def Q2Presentation.Lifting.conjOnN {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (y : Yt.Y) : ↥E.N →* ↥E.N

Right conjugation by y on the kernel: n ↦ y⁻¹ n y (the operator appearing in the engine's twisted-cocycle law).

Equations

• Q2Presentation.Lifting.conjOnN E y = { toFun := fun (n : ↥E.N) => ⟨y⁻¹ * ↑n * y, ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Q2Presentation.Lifting.conjOnN_coe {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (y : Yt.Y) (n : ↥E.N) : ↑((conjOnN E y) n) = y⁻¹ * ↑n * y

def Q2Presentation.Lifting.conjEndN {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (y : Yt.Y) : Module.End (ZMod 2) (NAdd E)

Right conjugation by y as an F₂-linear endomorphism of N.

Equations

• Q2Presentation.Lifting.conjEndN E y = { toFun := ⇑(MonoidHom.toAdditive (Q2Presentation.Lifting.conjOnN E y)), map_add' := ⋯, map_smul' := ⋯ }

theorem Q2Presentation.Lifting.conjEndN_apply {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (y : Yt.Y) (m : NAdd E) : (conjEndN E y) m = Additive.ofMul ((conjOnN E y) (Additive.toMul m))

theorem Q2Presentation.Lifting.conjEndN_one {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) : conjEndN E 1 = 1

Conjugation by 1 is the identity operator.

theorem Q2Presentation.Lifting.conjEndN_mul {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (y₁ y₂ : Yt.Y) : conjEndN E (y₁ * y₂) = conjEndN E y₂ * conjEndN E y₁

Right conjugation is contravariantly multiplicative: conj_{y₁y₂} = conj_{y₂} ∘ conj_{y₁}.

theorem Q2Presentation.Lifting.conjEndN_of_mem {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) (y : Yt.Y) (hy : y ∈ E.N) : conjEndN E y = 1

Conjugation by an element of N is trivial (N abelian).

The additive reading of engine twisted cocycles

def Q2Presentation.Lifting.cocycleAdd {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) : ↑Γ.toProfinite.toTop → NAdd E

The additive reading of an engine twisted cocycle: pointwise, the N-valued function as a map into the F₂-space.

Equations

• Q2Presentation.Lifting.cocycleAdd E B F g f₀ z γ = Additive.ofMul ⟨↑z γ, ⋯⟩

theorem Q2Presentation.Lifting.cocycleAdd_law {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (γ γ' : ↑Γ.toProfinite.toTop) : cocycleAdd E B F g f₀ z (γ * γ') = (conjEndN E ((ProfiniteGrp.Hom.hom ↑f₀) γ')) (cocycleAdd E B F g f₀ z γ) + cocycleAdd E B F g f₀ z γ'

The additive twisted-cocycle law: the engine law z(γγ') = (f₀γ')⁻¹ z(γ) f₀(γ') · z(γ') reads additively as z(γγ') = conj_{f₀ γ'}(z γ) + z γ'.

C2: cocycle values at 1 and inverses, and extensionality

theorem Q2Presentation.Lifting.Z1_val_one {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) : ↑z 1 = 1

A twisted cocycle vanishes at 1.

theorem Q2Presentation.Lifting.Z1_val_inv {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (γ : ↑Γ.toProfinite.toTop) : ↑z γ⁻¹ = (ProfiniteGrp.Hom.hom ↑f₀) γ * (↑z γ)⁻¹ * ((ProfiniteGrp.Hom.hom ↑f₀) γ)⁻¹

The value at an inverse is conjugate-inverse of the value.

theorem Q2Presentation.Lifting.Z1_ext {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (K : Subgroup ↑Γ.toProfinite.toTop) (hK : K.topologicalClosure = ⊤) (S : Set ↑Γ.toProfinite.toTop) (hSK : Subgroup.closure S = K) (z₁ z₂ : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (hagree : ∀ γ ∈ S, ↑z₁ γ = ↑z₂ γ) : z₁ = z₂

Cocycle extensionality: two twisted cocycles agreeing on a topologically generating set are equal (the agreement set is a closed subgroup).

C4a: generator operators and the telescoping toolkit

def Q2Presentation.Lifting.genOp {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (γ : ↑Γ.toProfinite.toTop) : Module.End (ZMod 2) (NAdd E)

The conjugation operator of γ through the base lift.

Equations

• Q2Presentation.Lifting.genOp E B F g f₀ γ = Q2Presentation.Lifting.conjEndN E ((ProfiniteGrp.Hom.hom ↑f₀) γ)

theorem Q2Presentation.Lifting.genOp_one {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) : genOp E B F g f₀ 1 = 1

theorem Q2Presentation.Lifting.genOp_mul {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (γ γ' : ↑Γ.toProfinite.toTop) : genOp E B F g f₀ (γ * γ') = genOp E B F g f₀ γ' * genOp E B F g f₀ γ

theorem Q2Presentation.Lifting.genOp_inv_mul {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (γ : ↑Γ.toProfinite.toTop) : genOp E B F g f₀ γ⁻¹ * genOp E B F g f₀ γ = 1

theorem Q2Presentation.Lifting.genOp_mul_inv {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (γ : ↑Γ.toProfinite.toTop) : genOp E B F g f₀ γ * genOp E B F g f₀ γ⁻¹ = 1

theorem Q2Presentation.Lifting.cocycleAdd_one {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) : cocycleAdd E B F g f₀ z 1 = 0

The cocycle vanishes at 1, additively.

theorem Q2Presentation.Lifting.cocycleAdd_mul {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (γ γ' : ↑Γ.toProfinite.toTop) : cocycleAdd E B F g f₀ z (γ * γ') = (genOp E B F g f₀ γ') (cocycleAdd E B F g f₀ z γ) + cocycleAdd E B F g f₀ z γ'

Additive law, genOp form.

theorem Q2Presentation.Lifting.cocycleAdd_add_self {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (γ : ↑Γ.toProfinite.toTop) : cocycleAdd E B F g f₀ z γ + cocycleAdd E B F g f₀ z γ = 0

Every additive value is 2-torsion.

theorem Q2Presentation.Lifting.cocycleAdd_inv {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (γ : ↑Γ.toProfinite.toTop) : cocycleAdd E B F g f₀ z γ⁻¹ = (genOp E B F g f₀ γ⁻¹) (cocycleAdd E B F g f₀ z γ)

Values at inverses: z(γ⁻¹) = genOp(γ⁻¹) (z γ).

theorem Q2Presentation.Lifting.cocycleAdd_pow {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (γ : ↑Γ.toProfinite.toTop) (n : ℕ) : cocycleAdd E B F g f₀ z (γ ^ n) = (∑ i ∈ Finset.range n, genOp E B F g f₀ γ ^ i) (cocycleAdd E B F g f₀ z γ)

Values at powers: the geometric telescope.

theorem Q2Presentation.Lifting.tame_relation_row {Yt : BoundaryFramedTarget} (E : ElementaryKernel Yt) {Γ : ProfiniteGrp.{0}} (B : BoundaryPackage Γ) (F : BoundaryFrame Yt) (g : boundaryFramedSurj B (TorsorProgram.quotientFramedTarget Yt E.N ⋯ ⋯) (TorsorProgram.quotientFrame Yt E.N ⋯ ⋯ F)) (f₀ : TorsorProgram.liftHom Yt E.N ⋯ ⋯ B F g) (z : TorsorProgram.Z1 Yt E.N ⋯ ⋯ B F g f₀) (γs γt : ↑Γ.toProfinite.toTop) (hrel : γs⁻¹ * γt * γs = γt ^ 2) : (genOp E B F g f₀ γs * genOp E B F g f₀ γt * genOp E B F g f₀ γs⁻¹ + 1) (cocycleAdd E B F g f₀ z γs) + (genOp E B F g f₀ γs + 1 + genOp E B F g f₀ γt) (cocycleAdd E B F g f₀ z γt) = 0

The tame relation row: if γs⁻¹ γt γs = γt² holds in Γ, the generator values satisfy the corresponding linear condition.