OAI/GroupTheory/PolycyclicRecognition/Geometry/WeightChambers.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Incident weight chambers determine an extreme ray

Both signs of every active hyperplane occur among genuine open chambers. Intersecting their closures therefore imposes the active equations; actual extremality, rather than a rank assumption, identifies the resulting ray.

  1. def OAI.PolycyclicRecognition.orientedWeight line 23
  2. def OAI.PolycyclicRecognition.weightChamber line 26
  3. def OAI.PolycyclicRecognition.closedWeightChamber line 29
  4. def OAI.PolycyclicRecognition.incidentWeightChamber line 32
  5. def OAI.PolycyclicRecognition.weightSigns line 35
  6. theorem OAI.PolycyclicRecognition.exists_positive_chamber_perturbation line 38
  7. theorem OAI.PolycyclicRecognition.exists_incident_chamber_of_generic line 63

    Source documentation

    Break ties at the active hyperplanes using a generic direction.

    theorem exists_incident_chamber_of_generic (α : I → W →L[ℝ] ℝ) (w : W)
    {v : W} (hv : v ∈ genericWeightDirections α) :
    ∃ σ : I → Bool, incidentWeightChamber α w σ ∧
      ∀ i, α i w = 0 → σ i = weightSigns α v i := by
…

    Mentions: OAI.PolycyclicRecognition.genericWeightDirections, OAI.PolycyclicRecognition.incidentWeightChamber, OAI.PolycyclicRecognition.weightSigns

  8. theorem OAI.PolycyclicRecognition.exists_incident_chamber_positive line 89
  9. theorem OAI.PolycyclicRecognition.exists_incident_chamber_negative line 96
  10. theorem OAI.PolycyclicRecognition.incident_chamber_intersection_eq_ray line 105