Concrete §7 tower objects over the ⊆-minimal kernel

The literal manuscript objects (eq:targettower, l.3626–3642) for a first non-scalar chief factor with ⊆-minimal kernel K:

• towerC K := Y ⧸ K — the lower target C (finite group);
• towerMgrp K := K ⧸ Φ(K) — the Frattini quotient, elementary abelian by the Burnside-basis core (FrattiniQuotientElementary), so towerM K := Additive (towerMgrp K) is a finite ZMod 2-module;
• towerActM K : towerC K →* (towerM K ≃ₗ[ZMod 2] towerM K) — conjugation, descended twice: through Φ(K) (characteristic) and through K (inner conjugation is trivial mod Φ(K) since commutators lie in Φ(K)).

Everything here is proved — no axioms. The simple-head facts (T, M/T ≅ V, (M^∨)^C = 0) and the K/R ≃ M bridge are the remaining parts of sec7_rawTowerPacket_exists (subsequent files).

The kernel is a finite 2-group

theorem Q2Presentation.Induction.KernelMinimal.isTwoGroup {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : IsPGroup 2 ↥K.Ksub

The ⊆-minimal kernel is a 2-group (it sits inside the marked wild kernel).

instance Q2Presentation.Induction.instFiniteSubtypeYFstBoundaryFramedTargetBoundaryFrameMemSubgroupKsub {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Finite ↥K.Ksub

The concrete tower objects

@[reducible, inline]

abbrev Q2Presentation.Induction.towerC {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Type

The lower target C = Y/K (eq:targettower).

Equations

• Q2Presentation.Induction.towerC K = (p.fst.Y ⧸ K.Ksub)

instance Q2Presentation.Induction.instGroupTowerC {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Group (towerC K)

Equations

• Q2Presentation.Induction.instGroupTowerC K = inferInstance

instance Q2Presentation.Induction.instFiniteTowerC {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Finite (towerC K)

@[reducible, inline]

abbrev Q2Presentation.Induction.towerMgrp {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Type

The multiplicative Frattini quotient K/Φ(K).

Equations

• Q2Presentation.Induction.towerMgrp K = (↥K.Ksub ⧸ frattini ↥K.Ksub)

instance Q2Presentation.Induction.towerMgrpCommGroup {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : CommGroup (towerMgrp K)

Equations

• Q2Presentation.Induction.towerMgrpCommGroup K = Q2Presentation.Induction.IsPGroup.frattiniQuotientCommGroup ⋯

@[reducible, inline]

abbrev Q2Presentation.Induction.towerM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Type

The additive elementary module layer M = K/Φ(K) (lem:simplehead).

Equations

• Q2Presentation.Induction.towerM K = Additive (Q2Presentation.Induction.towerMgrp K)

instance Q2Presentation.Induction.instAddCommGroupTowerM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : AddCommGroup (towerM K)

Equations

• Q2Presentation.Induction.instAddCommGroupTowerM K = Additive.addCommGroup

instance Q2Presentation.Induction.towerMModule {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Module (ZMod 2) (towerM K)

Equations

• Q2Presentation.Induction.towerMModule K = Q2Presentation.Induction.IsPGroup.frattiniQuotientModule ⋯

instance Q2Presentation.Induction.instFiniteTowerM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Finite (towerM K)

noncomputable instance Q2Presentation.Induction.instFintypeTowerM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : Fintype (towerM K)

Equations

• Q2Presentation.Induction.instFintypeTowerM K = Fintype.ofFinite (Q2Presentation.Induction.towerM K)

noncomputable instance Q2Presentation.Induction.instDecidableEqTowerM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : DecidableEq (towerM K)

Equations

• Q2Presentation.Induction.instDecidableEqTowerM K = Classical.decEq (Q2Presentation.Induction.towerM K)

Conjugation on the kernel and its descent to M

def Q2Presentation.Induction.kernelConjAut {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) : ↥K.Ksub ≃* ↥K.Ksub

Conjugation by an ambient element as an automorphism of the (normal) kernel.

Equations

• Q2Presentation.Induction.kernelConjAut K y = { toFun := fun (k : ↥K.Ksub) => ⟨y * ↑k * y⁻¹, ⋯⟩, invFun := fun (k : ↥K.Ksub) => ⟨y⁻¹ * ↑k * y, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem Q2Presentation.Induction.kernelConjAut_apply_coe {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) (k : ↥K.Ksub) : ↑((kernelConjAut K y) k) = y * ↑k * y⁻¹

theorem Q2Presentation.Induction.kernelConjAut_mem_frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) {k : ↥K.Ksub} (hk : k ∈ frattini ↥K.Ksub) : (kernelConjAut K y) k ∈ frattini ↥K.Ksub

Conjugation preserves the Frattini subgroup (it is characteristic).

def Q2Presentation.Induction.conjOnMgrp {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) : towerMgrp K →* towerMgrp K

Conjugation by y, descended to the Frattini quotient.

Equations

• Q2Presentation.Induction.conjOnMgrp K y = QuotientGroup.lift (frattini ↥K.Ksub) ((QuotientGroup.mk' (frattini ↥K.Ksub)).comp (Q2Presentation.Induction.kernelConjAut K y).toMonoidHom) ⋯

@[simp]

theorem Q2Presentation.Induction.conjOnMgrp_mk {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) (k : ↥K.Ksub) : (conjOnMgrp K y) ((QuotientGroup.mk' (frattini ↥K.Ksub)) k) = (QuotientGroup.mk' (frattini ↥K.Ksub)) ((kernelConjAut K y) k)

theorem Q2Presentation.Induction.conjOnMgrp_mul {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y₁ y₂ : p.fst.Y) (m : towerMgrp K) : (conjOnMgrp K (y₁ * y₂)) m = (conjOnMgrp K y₁) ((conjOnMgrp K y₂) m)

The descended conjugations compose: conj (y₁ y₂) = conj y₁ ∘ conj y₂.

theorem Q2Presentation.Induction.conjOnMgrp_one {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (m : towerMgrp K) : (conjOnMgrp K 1) m = m

Conjugation by the identity is the identity.

theorem Q2Presentation.Induction.conjOnMgrp_kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (k₀ : p.fst.Y) (hk₀ : k₀ ∈ K.Ksub) (m : towerMgrp K) : (conjOnMgrp K k₀) m = m

Inner conjugation is trivial on the Frattini quotient: for k₀ ∈ K, conjugation by k₀ fixes M = K/Φ(K) pointwise (commutators lie in Φ(K)).

The additive/linear form of the action

def Q2Presentation.Induction.conjOnM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) : towerM K →+ towerM K

Conjugation by y on the additive module M.

Equations

• Q2Presentation.Induction.conjOnM K y = MonoidHom.toAdditive (Q2Presentation.Induction.conjOnMgrp K y)

theorem Q2Presentation.Induction.conjOnM_apply {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) (m : towerM K) : (conjOnM K y) m = Additive.ofMul ((conjOnMgrp K y) (Additive.toMul m))

def Q2Presentation.Induction.conjLinearOnM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) : towerM K ≃ₗ[ZMod 2] towerM K

Conjugation by y as a ZMod 2-linear equivalence of M (linearity is automatic for additive maps of ZMod 2-modules).

Equations

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

theorem Q2Presentation.Induction.conjLinearOnM_apply {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) (m : towerM K) : (conjLinearOnM K y) m = Additive.ofMul ((conjOnMgrp K y) (Additive.toMul m))

def Q2Presentation.Induction.towerActM {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) : towerC K →* towerM K ≃ₗ[ZMod 2] towerM K

The conjugation action of the lower target C = Y/K on the additive module M = K/Φ(K), as ZMod 2-linear equivalences — the manuscript's 𝔽₂[C]-module structure on M (lem:simplehead), fully constructed.

Equations

• Q2Presentation.Induction.towerActM K = QuotientGroup.lift K.Ksub { toFun := fun (y : p.fst.Y) => Q2Presentation.Induction.conjLinearOnM K y, map_one' := ⋯, map_mul' := ⋯ } ⋯

theorem Q2Presentation.Induction.towerActM_mk {p : FramedPair} {chief : NonScalarChiefFactor p} (K : KernelMinimal chief) (y : p.fst.Y) (m : towerM K) : ((towerActM K) ((QuotientGroup.mk' K.Ksub) y)) m = Additive.ofMul ((conjOnMgrp K y) (Additive.toMul m))