PositiveCharacterIdeal.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The positive character ideal and the determinant trick

Finite generation over a character monoid forces an identity supported in its strictly positive part. This is the reverse of the positive identity criterion.

theorem OAI.PolycyclicRecognition.ideal_identity_of_surjective_scalar line 20
theorem OAI.PolycyclicRecognition.representation_mapDomain line 33
def OAI.PolycyclicRecognition.characterPositiveIdeal line 49
theorem OAI.PolycyclicRecognition.mem_characterPositiveIdeal_iff line 54
theorem OAI.PolycyclicRecognition.positive_monomial_mem_characterPositiveIdeal line 68
theorem OAI.PolycyclicRecognition.characterMonoid_positive_identity line 74
theorem OAI.PolycyclicRecognition.positive_identity_of_finite_characterMonoidModule line 99
Source documentation
A nonzero character direction with finite monoid generation admits an actual group-ring identity whose support lies in the strict positive half-space.
```
theorem positive_identity_of_finite_characterMonoidModule
    (ρ : Representation ℤ Q M) (χ : Q →* Multiplicative ℝ)
    [Module.Finite ℤ[characterNonnegativeMonoid χ] (characterMonoidRepresentation ρ χ).asModule]
    (t : Q) (ht : 0 < (χ t).toAdd) :
    ∃ a : ℤ[Q], (∀ q ∈ a.coeff.support, 0 < (χ q).toAdd) ∧ ρ.asAlgebraHom a = 1 := by
…
```
Mentions: OAI.PolycyclicRecognition.characterNonnegativeMonoid, OAI.PolycyclicRecognition.characterMonoidRepresentation

theorem OAI.PolycyclicRecognition.finite_characterMonoidModule_iff_positive_identity line 116

Source documentation

The positive identity criterion, with both directions proved.

theorem finite_characterMonoidModule_iff_positive_identity
    (ρ : Representation ℤ Q M) [Module.Finite ℤ[Q] ρ.asModule]
    (χ : Q →* Multiplicative ℝ) (t : Q) (ht : 0 < (χ t).toAdd) :
    Module.Finite ℤ[characterNonnegativeMonoid χ] (characterMonoidRepresentation ρ χ).asModule ↔
      ∃ a : ℤ[Q], (∀ q ∈ a.coeff.support, 0 < (χ q).toAdd) ∧ ρ.asAlgebraHom a = 1 := by
…

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