RepresentationOrbitGenerators.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Positive annihilators give finite generation over a character monoid

theorem OAI.PolycyclicRecognition.representation_finite_orbit_generators line 13

theorem OAI.PolycyclicRecognition.finite_characterMonoidModule_of_positive_relation line 38

Source documentation

The sufficient positive-annihilator criterion. The relation is an actual identity on the module, not an assumed finiteness or solvability conclusion.

theorem finite_characterMonoidModule_of_positive_relation
    (ρ : Representation ℤ Q M) [Module.Finite ℤ[Q] ρ.asModule]
    (χ : Q →* Multiplicative ℝ) (a : Finset Q) (c : Q → ℤ)
    {δ : ℝ} (hδ : 0 < δ) (ha : ∀ g ∈ a, δ ≤ (χ g).toAdd)
    (hrec : ∀ x : M, x = ∑ g ∈ a, c g • ρ g x) :
    Module.Finite ℤ[characterNonnegativeMonoid χ] (characterMonoidRepresentation ρ χ).asModule := by
…

Mentions: OAI.PolycyclicRecognition.characterNonnegativeMonoid, OAI.PolycyclicRecognition.characterMonoidRepresentation