ConnectedBlockContainment.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Local block preservation implies global preservation

Conjugates of coordinate projections detect the off-block entries of a matrix close to the identity. For a connected subgroup, this local condition gives containment in the actual block-diagonal subgroup. The next root-extraction argument supplies the projection identities.

theorem OAI.DukePrimeDegree.subgroup_le_of_mem_nhds_one line 24
Source documentation
An open neighborhood of the identity in a subgroup is enough for containment in another subgroup when the first group is connected.
```
theorem subgroup_le_of_mem_nhds_one {n : ℕ}
    (L K : Subgroup (G n)) [PreconnectedSpace L]
    (hlocal : {g : L | g.val ∈ K} ∈ 𝓝 (1 : L)) : L ≤ K := by
…
```

theorem OAI.DukePrimeDegree.blockIntersection_mem_nhds_one_of_projection_products line 40

Source documentation

Conjugated coordinate projections force block preservation on an open neighborhood inside L, without a connectedness assumption.

theorem blockIntersection_mem_nhds_one_of_projection_products {n : ℕ}
    (L : Subgroup (G n)) (r : Setoid (Fin n))
    (hproducts : ∀ g : L, ∀ a b, ¬ r a b → ∀ k,
      g.val.val a k * g.val⁻¹.val k b = 0) :
    {g : L | g.val ∈ blockMatrixGroup r} ∈ 𝓝 (1 : L) := by
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup

theorem OAI.DukePrimeDegree.blockIntersection_isOpen_of_projection_products line 71

Source documentation

The subgroup preserving the blocks is open in L.

theorem blockIntersection_isOpen_of_projection_products {n : ℕ}
    (L : Subgroup (G n)) (r : Setoid (Fin n))
    (hproducts : ∀ g : L, ∀ a b, ¬ r a b → ∀ k,
      g.val.val a k * g.val⁻¹.val k b = 0) :
    IsOpen (((blockMatrixGroup r).comap L.subtype : Subgroup L) : Set L) :=
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup

theorem OAI.DukePrimeDegree.connected_subgroup_le_blocks_of_projection_products line 81

Source documentation

The polynomial identities on conjugated coordinate projections force block preservation everywhere in a connected subgroup.

theorem connected_subgroup_le_blocks_of_projection_products {n : ℕ}
    (L : Subgroup (G n)) [PreconnectedSpace L] (r : Setoid (Fin n))
    (hproducts : ∀ g : L, ∀ a b, ¬ r a b → ∀ k,
      g.val.val a k * g.val⁻¹.val k b = 0) : L ≤ blockMatrixGroup r :=
…

Mentions: OAI.DukePrimeDegree.blockMatrixGroup