The literal Frattini layer as an F_2[C]-module

This file supplies the R side of the corrected raw §7 tower packet. The M = K / Phi(K) side and the radical layer T are already built in Section7ConcreteObjects and Section7SimpleHeadRadical. Here we use the proved centrality [K, Phi(K)] = 1 and the exponent-two theorem for Phi(K) to make

• R = Additive (Phi(K)) a finite ZMod 2-module;
• conjugation by Y on R descend to an action of C = Y/K.

The literal R = Phi(K) object

theorem Q2Presentation.Induction.kernelFrattini_le_kernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : kernelFrattini K ≤ K.Ksub

The literal Frattini layer lies in the selected kernel.

theorem Q2Presentation.Induction.kernelFrattini_normal_local {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (kernelFrattini K).Normal

The literal Frattini layer is normal in the ambient finite target.

instance Q2Presentation.Induction.kernelFrattiniCommGroup {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : CommGroup ↥(kernelFrattini K)

The multiplicative Frattini layer is commutative: Phi(K) centralizes K and is contained in K.

Equations

• Q2Presentation.Induction.kernelFrattiniCommGroup chief K = { toGroup := inferInstanceAs (Group ↥(Q2Presentation.Induction.kernelFrattini K)), mul_comm := ⋯ }

@[reducible, inline]

abbrev Q2Presentation.Induction.towerR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

The additive R = Phi(K) layer.

Equations

• Q2Presentation.Induction.towerR chief K = Additive ↥(Q2Presentation.Induction.kernelFrattini K)

instance Q2Presentation.Induction.instAddCommGroupTowerR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : AddCommGroup (towerR chief K)

Equations

• Q2Presentation.Induction.instAddCommGroupTowerR chief K = Additive.addCommGroup

instance Q2Presentation.Induction.instModuleZModOfNatNatTowerR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Module (ZMod 2) (towerR chief K)

Equations

• Q2Presentation.Induction.instModuleZModOfNatNatTowerR chief K = AddCommGroup.zmodModule ⋯

instance Q2Presentation.Induction.instFiniteTowerR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Finite (towerR chief K)

noncomputable instance Q2Presentation.Induction.instFintypeTowerR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Fintype (towerR chief K)

Equations

• Q2Presentation.Induction.instFintypeTowerR chief K = Fintype.ofFinite (Q2Presentation.Induction.towerR chief K)

noncomputable instance Q2Presentation.Induction.instDecidableEqTowerR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : DecidableEq (towerR chief K)

Equations

• Q2Presentation.Induction.instDecidableEqTowerR chief K = Classical.decEq (Q2Presentation.Induction.towerR chief K)

Conjugation on R and descent to C = Y/K

def Q2Presentation.Induction.kernelFrattiniConjAut {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) : ↥(kernelFrattini K) ≃* ↥(kernelFrattini K)

Conjugation by an ambient element as an automorphism of R = Phi(K).

Equations

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

@[simp]

theorem Q2Presentation.Induction.kernelFrattiniConjAut_apply_coe {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (r : ↥(kernelFrattini K)) : ↑((kernelFrattiniConjAut chief K y) r) = y * ↑r * y⁻¹

def Q2Presentation.Induction.conjOnR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) : towerR chief K →+ towerR chief K

Conjugation by y on the additive R layer.

Equations

• Q2Presentation.Induction.conjOnR chief K y = MonoidHom.toAdditive (Q2Presentation.Induction.kernelFrattiniConjAut chief K y).toMonoidHom

theorem Q2Presentation.Induction.conjOnR_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (r : towerR chief K) : (conjOnR chief K y) r = Additive.ofMul ((kernelFrattiniConjAut chief K y) (Additive.toMul r))

theorem Q2Presentation.Induction.kernelFrattiniConjAut_mul {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y₁ y₂ : p.fst.Y) (r : ↥(kernelFrattini K)) : (kernelFrattiniConjAut chief K (y₁ * y₂)) r = (kernelFrattiniConjAut chief K y₁) ((kernelFrattiniConjAut chief K y₂) r)

The descended conjugations compose.

theorem Q2Presentation.Induction.kernelFrattiniConjAut_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (r : ↥(kernelFrattini K)) : (kernelFrattiniConjAut chief K 1) r = r

Conjugation by the identity is trivial on R.

theorem Q2Presentation.Induction.kernelFrattiniConjAut_kernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : p.fst.Y) (hk : k ∈ K.Ksub) (r : ↥(kernelFrattini K)) : (kernelFrattiniConjAut chief K k) r = r

Conjugation by an element of K is trivial on R, because R centralizes K.

def Q2Presentation.Induction.conjLinearOnR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) : towerR chief K ≃ₗ[ZMod 2] towerR chief K

Conjugation by y as a ZMod 2-linear equivalence of R.

Equations

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

theorem Q2Presentation.Induction.conjLinearOnR_apply {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (r : towerR chief K) : (conjLinearOnR chief K y) r = Additive.ofMul ((kernelFrattiniConjAut chief K y) (Additive.toMul r))

def Q2Presentation.Induction.towerActR {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : towerC K →* towerR chief K ≃ₗ[ZMod 2] towerR chief K

The conjugation action of C = Y/K on R = Phi(K).

Equations

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

theorem Q2Presentation.Induction.towerActR_mk {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (y : p.fst.Y) (r : towerR chief K) : ((towerActR chief K) ((QuotientGroup.mk' K.Ksub) y)) r = Additive.ofMul ((kernelFrattiniConjAut chief K y) (Additive.toMul r))