The natural Sp₄(𝔽₂) action

This module gives the conceptual finite proof that Sp₄(𝔽₂) acts transitively on nonzero vectors. It realizes the action with symplectic transvections and keeps the exhaustive normal-subgroup certificate separate.

@[reducible, inline]

abbrev Connes.Sp4.F : Type

Characteristic-two scalar field. Paper: §§2, 6.

Equations

• Connes.Sp4.F = ZMod 2

@[reducible, inline]

abbrev Connes.Sp4.Group : Submonoid (Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) F)

Symplectic group carrier. Paper: §§2, 6.

Equations

• Connes.Sp4.Group = Matrix.symplecticGroup (Fin 2) Connes.Sp4.F

@[reducible, inline]

abbrev Connes.Sp4.Matrix4 : Type

Four-by-four matrices with the symplectic block indexing.

Equations

• Connes.Sp4.Matrix4 = Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) Connes.Sp4.F

def Connes.Sp4.allMatrices : Finset Matrix4

The finite set of all four-by-four matrices over the coefficient field.

Equations

• Connes.Sp4.allMatrices = Finset.univ

def Connes.Sp4.symplecticMatrices : Finset Matrix4

Matrices preserving the standard symplectic form.

Equations

• Connes.Sp4.symplecticMatrices = {A ∈ Connes.Sp4.allMatrices | A * Matrix.J (Fin 2) Connes.Sp4.F * Matrix.transpose A = Matrix.J (Fin 2) Connes.Sp4.F}

@[instance_reducible]

instance Connes.Sp4.instFintypeSubtypeMatrixSumFinOfNatNatFMemSubmonoidGroup : Fintype ↥Group

Equations

• Connes.Sp4.instFintypeSubtypeMatrixSumFinOfNatNatFMemSubmonoidGroup = Fintype.subtype Connes.Sp4.symplecticMatrices Connes.Sp4.instFintypeSubtypeMatrixSumFinOfNatNatFMemSubmonoidGroup._proof_3

theorem Connes.Sp4.transitive_on_nonzero_vectors (v : OpenAIPort.ModTwoSpace) : v ≠ 0 → ∀ (w : OpenAIPort.ModTwoSpace), w ≠ 0 → ∃ (g : ↥Group), g • v = w

Nonzero-vector transitivity. Paper: §2.