AlgebraGroupTangent.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Infinitesimal commutators of matrix groups

The finite-dimensional span of derivatives of curves in a subgroup records its infinitesimal action. Differentiating group commutators twice puts the algebra commutator into the tangent span of the derived subgroup.

def OAI.PolycyclicRecognition.AlgebraGroupTangentVector line 28
Source documentation
A derivative at the identity of a curve contained in a given matrix group.
```
def AlgebraGroupTangentVector (D : Subgroup Aˣ) (X : A) : Prop :=
…
```
def OAI.PolycyclicRecognition.algebraGroupTangentSpan line 33
Source documentation
The finite-dimensional linear span of the actual curve derivatives.
```
def algebraGroupTangentSpan (D : Subgroup Aˣ) : Submodule ℝ A :=
…
```

theorem OAI.PolycyclicRecognition.hasDerivAt_units_inverse_at_one line 38

Source documentation

Differentiating an inverse curve at the identity negates the tangent.

theorem hasDerivAt_units_inverse_at_one {c : ℝ → Aˣ} {X : A}
    (h0 : c 0 = 1) (hc : HasDerivAt (fun t => (c t : A)) X 0) :
    HasDerivAt (fun t => (((c t)⁻¹ : Aˣ) : A)) (-X) 0 := by
…

theorem OAI.PolycyclicRecognition.submodule_mem_of_hasDerivAt line 49
Source documentation
A derivative of a curve in a finite-dimensional linear subspace stays in that subspace.
```
theorem submodule_mem_of_hasDerivAt (M : Submodule ℝ A) {f : ℝ → A} {X : A}
    (hf : HasDerivAt f X 0) (hmem : ∀ t, f t ∈ M) : X ∈ M := by
…
```
theorem OAI.PolycyclicRecognition.algebraGroupTangentSpan_mono line 55
theorem OAI.PolycyclicRecognition.algebraGroupTangentSpan_bot line 63
Source documentation
The identity group has zero tangent span.
```
theorem algebraGroupTangentSpan_bot : algebraGroupTangentSpan (⊥ : Subgroup Aˣ) = ⊥ := by
…
```
Mentions: OAI.PolycyclicRecognition.algebraGroupTangentSpan
theorem OAI.PolycyclicRecognition.conjugation_difference_tangent line 77
Source documentation
Conjugation by one group element gives a tangent of the group commutator subgroup after subtracting the original tangent.
```
theorem conjugation_difference_tangent {D : Subgroup Aˣ} {u : Aˣ} (hu : u ∈ D)
    {Y : A} (hY : AlgebraGroupTangentVector D Y) :
    AlgebraGroupTangentVector ⁅D, D⁆ ((u : A) * Y * (u⁻¹ : Aˣ) - Y) := by
…
```
Mentions: OAI.PolycyclicRecognition.AlgebraGroupTangentVector
theorem OAI.PolycyclicRecognition.commutator_mem_derived_tangentSpan line 91
Source documentation
Two actual tangents have an algebra commutator tangent to the derived subgroup. The second differentiation uses closedness of the finite span.
```
theorem commutator_mem_derived_tangentSpan {D : Subgroup Aˣ} {X Y : A}
    (hX : AlgebraGroupTangentVector D X) (hY : AlgebraGroupTangentVector D Y) :
    X * Y - Y * X ∈ algebraGroupTangentSpan ⁅D, D⁆ := by
…
```
Mentions: OAI.PolycyclicRecognition.AlgebraGroupTangentVector, OAI.PolycyclicRecognition.algebraGroupTangentSpan