PositiveRootCoordinates.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinates separating an extremal root

Multiplication identifies a positive-root group with one real root coordinate and the group of remaining roots. Both directions are continuous, and the first coordinate is the corresponding matrix entry.

lemma OAI.DukePrimeDegree.transvection_mul_root_entry line 20
lemma OAI.DukePrimeDegree.remaining_root_entry line 27

def OAI.DukePrimeDegree.positiveRootFactorHomeomorph line 43

Source documentation

The explicit root-times-remainder coordinates used in the positive-root product induction.

def positiveRootFactorHomeomorph {n : ℕ} (S : Finset (Fin n × Fin n))
    (hpos : ∀ p ∈ S, p.1 < p.2)
    (hcomp : ∀ i j k : Fin n, (i, j) ∈ S → (j, k) ∈ S → (i, k) ∈ S)
    {a b : Fin n} (hab : a ≠ b) (habS : (a, b) ∈ S)
    (herase : ∀ i j k : Fin n, (i, j) ∈ S.erase (a, b) →
      (j, k) ∈ S.erase (a, b) → (i, k) ∈ S.erase (a, b)) :
    (ℝ × positiveRootGeneratedGroup (S.erase (a, b))) ≃ₜ positiveRootGeneratedGroup S where
…

Mentions: OAI.DukePrimeDegree.positiveRootGeneratedGroup

lemma OAI.DukePrimeDegree.root_entry_mul_transvection line 89
lemma OAI.DukePrimeDegree.positiveRootPattern_eliminate_right line 96

def OAI.DukePrimeDegree.positiveRootRightFactorHomeomorph line 120

Source documentation

With the root factor last, its coordinate lines are actual right root orbits. These are the coordinates used for disintegration.

def positiveRootRightFactorHomeomorph {n : ℕ} (S : Finset (Fin n × Fin n))
    (hpos : ∀ p ∈ S, p.1 < p.2)
    (hcomp : ∀ i j k : Fin n, (i, j) ∈ S → (j, k) ∈ S → (i, k) ∈ S)
    {a b : Fin n} (hab : a ≠ b) (habS : (a, b) ∈ S)
    (herase : ∀ i j k : Fin n, (i, j) ∈ S.erase (a, b) →
      (j, k) ∈ S.erase (a, b) → (i, k) ∈ S.erase (a, b)) :
    (positiveRootGeneratedGroup (S.erase (a, b)) × ℝ) ≃ₜ positiveRootGeneratedGroup S where
…

Mentions: OAI.DukePrimeDegree.positiveRootGeneratedGroup