OAI/GroupTheory/PolycyclicRecognition/Geometry/WeightRayPermutation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.PolycyclicRecognition.exists_weight_ray_permutation line 17

   Source documentation

   Pullback preserving a finite family of distinct positive rays acts by a permutation. Distinctness is on rays, not on a possibly repeated generator list.

   theorem exists_weight_ray_permutation
       (α : I → W →ₗ[ℝ] ℝ) (A : W ≃ₗ[ℝ] W)
       (hdistinct : ∀ i j (r : ℝ), 0 < r → α i = r • α j → i = j)
       (hmaps : ∀ i, ∃ (j : I) (r : ℝ), 0 < r ∧ (α i).comp A.toLinearMap = r • α j) :
       ∃ σ : I ≃ I, ∃ r : I → ℝ, (∀ i, 0 < r i) ∧
         ∀ i, (α i).comp A.toLinearMap = r i • α (σ i) := by
   …

2. theorem OAI.PolycyclicRecognition.positive_weight_count_of_ray_permutation line 43

   Source documentation

   A ray permutation preserves the number of positive weights at every vector. This supplies the fixed-count input of the line-sign argument.

   theorem positive_weight_count_of_ray_permutation
       (α : I → W →ₗ[ℝ] ℝ) (A : W ≃ₗ[ℝ] W) (σ : I ≃ I) (r : I → ℝ)
       (hr : ∀ i, 0 < r i)
       (heq : ∀ i, (α i).comp A.toLinearMap = r i • α (σ i)) (w : W) :
       (Finset.univ.filter (fun i => 0 < α i (A w))).card =
         (Finset.univ.filter (fun i => 0 < α i w)).card := by
   …

3. theorem OAI.PolycyclicRecognition.nonzero_weights_of_ray_permutation line 60

   Source documentation

   Genericity is also preserved by the same positive ray permutation.

   theorem nonzero_weights_of_ray_permutation
       (α : I → W →ₗ[ℝ] ℝ) (A : W ≃ₗ[ℝ] W) (σ : I ≃ I) (r : I → ℝ)
       (hr : ∀ i, 0 < r i)
       (heq : ∀ i, (α i).comp A.toLinearMap = r i • α (σ i))
       (w : W) (hw : ∀ i, α i w ≠ 0) : ∀ i, α i (A w) ≠ 0 := by
   …