Documentation

LeanPool.ConnesRigidity.Foundation.GroupTheory.Sp4Basic

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.

source
@[reducible, inline]
abbrev Connes.Sp4.F :
Type

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

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Connes.Sp4.Group :
    Submonoid (Matrix (Fin 2 ⊕ Fin 2) (Fin 2 ⊕ Fin 2) F)

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

    Equations
    Instances For
      source
      @[instance_reducible]
      instance Connes.Sp4.instFintypeSubtypeMatrixSumFinOfNatNatFMemSubmonoidGroup :
      Fintype ↥Group
      Equations
      source
      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.