OAI/GroupTheory/PolycyclicRecognition/Algebra/HigherExteriorFiniteRank.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

All finite exterior modules force finite dimension for an abelian action

  1. theorem OAI.PolycyclicRecognition.no_free_orbit_of_finite_higher_exterior line 16

    Source documentation

    Only one exterior degree, chosen larger than a finite algebra presentation of the group ring, is needed for the free-orbit contradiction.

    theorem no_free_orbit_of_finite_higher_exterior (ρ : Representation K Q M)
    (hext : ∀ n : ℕ, Module.Finite K[Q] (higherExteriorRepresentation ρ (n + 1)).asModule)
    (g : Q) (v : M) : ¬LinearIndependent K (fun i : ℕ => (ρ g ^ i) v) := by
…

    Mentions: OAI.PolycyclicRecognition.higherExteriorRepresentation

  2. theorem OAI.PolycyclicRecognition.finite_rank_of_finite_higher_exterior line 33