OAI/GroupTheory/PolycyclicRecognition/Algebra/PositiveAnnihilatorCriterion.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.finite_character_positive_lower_bound line 13
2. theorem OAI.PolycyclicRecognition.representation_groupRing_apply line 26
3. theorem OAI.PolycyclicRecognition.finite_characterMonoidModule_of_positive_identity line 33

   Source documentation

   This is the positive identity criterion, with support in the strict character half-space. It supplies a concrete sufficient Bieri--Strebel direction.

   theorem finite_characterMonoidModule_of_positive_identity
       (ρ : Representation ℤ Q M) [Module.Finite ℤ[Q] ρ.asModule]
       (χ : Q →* Multiplicative ℝ) (a : ℤ[Q])
       (ha : ∀ g ∈ a.coeff.support, 0 < (χ g).toAdd)
       (hid : ρ.asAlgebraHom a = 1) :
       Module.Finite ℤ[characterNonnegativeMonoid χ] (characterMonoidRepresentation ρ χ).asModule := by
   …

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