MatrixVelocitySpace.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

The actual vector space of subgroup velocities

Velocities are derivatives of genuine curves in the subgroup at its identity. Multiplication adds velocities and a linear reparametrization scales them. Conjugating the subgroup conjugates this vector space. No Lie-subgroup or homogeneous-support assertion is assumed here.

def OAI.DukePrimeDegree.HasIdentityMatrixDerivative line 24
lemma OAI.DukePrimeDegree.HasIdentityMatrixDerivative.hasMatrixVelocity line 28
lemma OAI.DukePrimeDegree.HasIdentityMatrixDerivative.mul line 33
lemma OAI.DukePrimeDegree.HasIdentityMatrixDerivative.reparametrize line 47
def OAI.DukePrimeDegree.matrixVelocitySpace line 62
Source documentation
The finite-dimensional real subspace comes from actual subgroup curves. In particular, it is not an arbitrary assigned frame.
```
def matrixVelocitySpace {n : ℕ} (H : Subgroup (G n)) :
    Submodule ℝ (Matrix (Fin n) (Fin n) ℝ) where
…
```
lemma OAI.DukePrimeDegree.matrixVelocitySpace_mono line 77
lemma OAI.DukePrimeDegree.isClosed_matrixVelocitySpace line 84
Source documentation
Finite-dimensionality makes the actual velocity space closed; no closed-subgroup theorem is required for this linear fact.
```
lemma isClosed_matrixVelocitySpace {n : ℕ} (H : Subgroup (G n)) :
    IsClosed (matrixVelocitySpace H : Set (Matrix (Fin n) (Fin n) ℝ)) :=
…
```
Mentions: OAI.DukePrimeDegree.matrixVelocitySpace
lemma OAI.DukePrimeDegree.hasDerivAt_matrix_mul_const line 88
lemma OAI.DukePrimeDegree.hasDerivAt_const_matrix_mul line 100
lemma OAI.DukePrimeDegree.HasIdentityMatrixDerivative.conjugate line 112

theorem OAI.DukePrimeDegree.conjugate_mem_matrixVelocitySpace line 126

Source documentation

Conjugation acts on the actual curve-velocity spaces. This is the covariance needed before applying finite-dimensional recurrence.

theorem conjugate_mem_matrixVelocitySpace {n : ℕ}
    (H L : Subgroup (G n)) (a : G n)
    (hconj : ∀ h ∈ H, a * h * a⁻¹ ∈ L)
    {V : Matrix (Fin n) (Fin n) ℝ} (hV : V ∈ matrixVelocitySpace H) :
    a.val * V * a⁻¹.val ∈ matrixVelocitySpace L := by
…

Mentions: OAI.DukePrimeDegree.matrixVelocitySpace