OAI/GroupTheory/PolycyclicRecognition/Geometry/WeightChamberAction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PolycyclicRecognition.PreservesPositiveWeightRays line 15
2. theorem OAI.PolycyclicRecognition.generic_of_mem_weightChamber line 19
3. theorem OAI.PolycyclicRecognition.weightSigns_eq_of_mem_chamber line 25
4. theorem OAI.PolycyclicRecognition.mem_weightChamber_signs_iff line 37
5. theorem OAI.PolycyclicRecognition.positive_weight_products_map line 57
6. theorem OAI.PolycyclicRecognition.generic_weights_map line 70
7. theorem OAI.PolycyclicRecognition.image_weightChamber line 80
8. theorem OAI.PolycyclicRecognition.image_closedWeightChamber line 100
9. theorem OAI.PolycyclicRecognition.image_closedWeightChamber_eq_of_signs line 119

   Source documentation

   Equal signs on one generic direction identify the full chamber images.

   theorem image_closedWeightChamber_eq_of_signs
       (α : I → W →L[ℝ] ℝ) (A B : W ≃ₗ[ℝ] W)
       (hA : PreservesPositiveWeightRays α A) (hAi : PreservesPositiveWeightRays α A.symm)
       (hB : PreservesPositiveWeightRays α B) (hBi : PreservesPositiveWeightRays α B.symm)
       {w : W} (hw : ∀ i, α i w ≠ 0)
       (hsign : ∀ i, 0 < α i (A w) ↔ 0 < α i (B w)) :
       A '' closedWeightChamber α (weightSigns α w) =
         B '' closedWeightChamber α (weightSigns α w) := by
   …

   Mentions: OAI.PolycyclicRecognition.PreservesPositiveWeightRays, OAI.PolycyclicRecognition.closedWeightChamber, OAI.PolycyclicRecognition.weightSigns