WellFoundedModuleRelations.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Finite generation from decreasing group-ring relations

A natural-number height measures distance from a submonoid. A bounded layer has finitely many representatives modulo that monoid. Relations which strictly decrease the height then give actual finite module generators.

def OAI.PolycyclicRecognition.submonoidRepresentationOrbit line 17
theorem OAI.PolycyclicRecognition.submonoidRepresentationOrbit_span_stable line 20
theorem OAI.PolycyclicRecognition.finite_submonoidRepresentation_of_orbitSpan line 38
theorem OAI.PolycyclicRecognition.representation_translate_identity line 61

theorem OAI.PolycyclicRecognition.finite_submonoidModule_of_decreasing_relations line 73

Source documentation

The finite descent argument used after the character geometry constructs a distance-to-cone height. Every relation is an actual identity on the module.

theorem finite_submonoidModule_of_decreasing_relations
    (ρ : Representation ℤ Q M) [Module.Finite ℤ[Q] ρ.asModule]
    (S : Submonoid Q) (height : Q → ℕ) (D : ℕ) (B : Finset Q)
    (hbase : ∀ q, height q ≤ D → ∃ b ∈ B, ∃ u : S, (u : Q) * b = q)
    (hrel : ∀ q, D < height q → ∃ a : ℤ[Q], ρ.asAlgebraHom a = 1 ∧
      ∀ g ∈ a.coeff.support, height (q * g) < height q) :
    Module.Finite ℤ[S] (Representation.asModule (ρ.comp S.subtype)) := by
…