PositiveRootPattern.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Matrix support of groups generated by positive roots

Transitive positive root sets define matrix patterns preserved by all products of their root generators. The assertion also holds on the closure, supplying the concrete support restriction for root induction.

def OAI.DukePrimeDegree.PositiveRootPattern line 22
Source documentation
Outside the chosen positive roots the matrix equals the identity.
```
def PositiveRootPattern {n : ℕ} (S : Finset (Fin n × Fin n)) (g : G n) : Prop :=
…
```
lemma OAI.DukePrimeDegree.positiveRootPattern_one line 25
lemma OAI.DukePrimeDegree.positiveRootPattern_transvection line 30
lemma OAI.DukePrimeDegree.positiveRootPattern_mul line 45
def OAI.DukePrimeDegree.positiveRootGeneratedGroup line 70
Source documentation
The subgroup generated by the root lines in S.
```
def positiveRootGeneratedGroup {n : ℕ} (S : Finset (Fin n × Fin n)) : Subgroup (G n) :=
…
```
lemma OAI.DukePrimeDegree.positiveRootGeneratedGroup_pattern line 74
lemma OAI.DukePrimeDegree.isClosed_positiveRootPattern line 87

lemma OAI.DukePrimeDegree.positiveRootClosure_pattern line 99

Source documentation

The root support restriction survives topological closure.

lemma positiveRootClosure_pattern {n : ℕ} (S : Finset (Fin n × Fin n))
    (htrans : ∀ a b c : Fin n, (a, b) ∈ S → (b, c) ∈ S → (a, c) ∈ S)
    {g : G n} (hg : g ∈ (positiveRootGeneratedGroup S).topologicalClosure) :
    PositiveRootPattern S g := by
…

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