OAI/GroupTheory/PolycyclicRecognition/Geometry/NormalizedWeightRays.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Deduplicating positive weight rays

Unit normalization gives a concrete finite set of positive rays, even when the original generator list repeats some rays with different multiplicities.

  1. def OAI.PolycyclicRecognition.normalizedWeight line 20
  2. def OAI.PolycyclicRecognition.NormalizedWeightRays line 22
  3. instance OAI.PolycyclicRecognition.(instance at line 25) line 25
  4. theorem OAI.PolycyclicRecognition.norm_normalizedWeight line 28
  5. theorem OAI.PolycyclicRecognition.normalizedWeight_pos_iff line 32
  6. theorem OAI.PolycyclicRecognition.normalizedWeightRays_distinct line 38
  7. theorem OAI.PolycyclicRecognition.exists_normalizedWeightRays_permutation line 59

    Source documentation

    A pullback on the original weights induces a permutation of the actual distinct rays, independently of duplicate generator weights.

    theorem exists_normalizedWeightRays_permutation
    (α : I → W →L[ℝ] ℝ) (hα : ∀ i, α i ≠ 0) (A : W ≃ₗ[ℝ] W)
    (hmaps : ∀ i, ∃ (j : I) (r : ℝ), 0 < r ∧
      (α i).toLinearMap.comp A.toLinearMap = r • (α j).toLinearMap) :
    ∃ σ : NormalizedWeightRays α ≃ NormalizedWeightRays α,
      ∃ r : NormalizedWeightRays α → ℝ, (∀ x, 0 < r x) ∧
        ∀ x, x.val.toLinearMap.comp A.toLinearMap = r x • (σ x).val.toLinearMap := by
…

    Mentions: OAI.PolycyclicRecognition.NormalizedWeightRays