OAI/NumberTheory/DukePrimeDegree/Geometry/PositiveRootFactorization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact elimination in a positive root group

Positive root patterns are exactly the groups generated by their root lines. Removing a shortest root gives a triangular factorization with that root as the first factor. In particular these generated groups are already closed; no additional matrices appear on taking their closure.

  1. lemma OAI.DukePrimeDegree.positiveRootGeneratedGroup_mono line 21
  2. lemma OAI.DukePrimeDegree.transvection_mem_positiveRootGeneratedGroup line 27
  3. lemma OAI.DukePrimeDegree.positiveRootPattern_eliminate line 33
  4. theorem OAI.DukePrimeDegree.positiveRootPattern_mem_generated line 57

    Source documentation

    Every matrix with the prescribed positive pattern is a product of the corresponding root transvections.

    theorem positiveRootPattern_mem_generated {n : ℕ} (S : Finset (Fin n × Fin n))
    (hpos : ∀ p ∈ S, p.1 < p.2)
    (hcomp : ∀ a b c : Fin n, (a, b) ∈ S → (b, c) ∈ S → (a, c) ∈ S)
    {g : G n} (hg : PositiveRootPattern S g) : g ∈ positiveRootGeneratedGroup S := by
…

    Mentions: OAI.DukePrimeDegree.PositiveRootPattern, OAI.DukePrimeDegree.positiveRootGeneratedGroup

  5. theorem OAI.DukePrimeDegree.positiveRootGeneratedGroup_iff line 81
  6. theorem OAI.DukePrimeDegree.isClosed_positiveRootGeneratedGroup line 87