FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet.LieDeriv

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import Mathlib.Analysis.Calculus.ContDiff.Comp
public import Mathlib.Analysis.Calculus.ContDiff.Operations
public import Mathlib.Analysis.Calculus.FDeriv.Bilinear
public import Mathlib.Analysis.Calculus.FDeriv.Symmetric
public import Mathlib.Analysis.Matrix.Normed
public import Mathlib.Analysis.Normed.Module.FiniteDimension
public import Mathlib.Analysis.SpecialFunctions.Exponential
public import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
public import Mathlib.Topology.Instances.Matrix

@[expose] public section

Lie derivatives of smooth functions on `GL n ℝ`

The C^∞ functions on GL n ℝ and the action on them of 𝔤𝔩 n ℝ and of its complexification 𝔤𝔩 n ℂ by left invariant differential operators. This is the analytic machinery behind condition (c) in the Borel-Jacquet definition of an automorphic form; see FormalConjecturesForMathlib.NumberTheory.AutomorphicForm.BorelJacquet for that definition, and Borel and Jacquet's Corvallis article, the reference below, for its source.

Main declarations

All in the namespace Matrix.GeneralLinearGroup unless qualified otherwise:

AutomorphicForm.LieDerivAux.fderiv_rightDeriv_apply and …_sub_comm: the product rule and bracket identity for the operator F ↦ fun M => fderiv ℝ F M (M * X) over an abstract normed algebra.

IsSmoothOnGL and smoothGL: the C^∞ functions on GL n ℝ, as a predicate and as a ℂ-submodule.

expGL and lieDerivFun: the matrix exponential as an element of GL n ℝ, and the left invariant derivative (X • φ) y = d/dt φ (y * exp (t • X)) |_{t = 0}.

lieDeriv and lieDerivC: the actions on smoothGL n of 𝔤𝔩 n ℝ and of its complexification 𝔤𝔩 n ℂ, with their bracket identities lieDeriv_bracket and lieDerivC_bracket.

Implementation notes

Smoothness on GL n ℝ is phrased as the existence of a C^∞ extension to the open set of invertible matrices (IsSmoothOnGL), rather than through a manifold structure: the normed ring instances on Matrix n n ℝ that would give GL n ℝ a chart are scoped, and conflict with the product topology that GL n ℝ already carries.

X ∈ 𝔤𝔩 n ℝ acts by differentiating along the one-parameter subgroup, (X • φ) y = d/dt φ (y * exp (t • X)) |_{t = 0}; this equals fderiv ℝ F y (y * X) for any C^∞ extension F of φ (lieDerivFun_eq_fderiv), through which every algebraic property is proved. The bracket identity is the product rule plus symmetry of the second derivative.

The product rule is proved over an abstract finite-dimensional normed ℝ-algebra and instantiated at Matrix n n ℝ. That is forced: Mathlib's norms on Matrix n n ℝ are scoped instances while its topology is global, so instance search cannot assemble SeminormedAddCommGroup (Matrix n n ℝ →L[ℝ] ℂ) for the written-out type even though the instance term typechecks, and the second-derivative lemmas behind the product rule need that instance as an argument. Instantiating an abstract lemma supplies its instance arguments instead of searching for them.

References:

A. Borel and H. Jacquet, Automorphic forms and automorphic representations, in Automorphic Forms, Representations and L-functions (Corvallis), Proc. Sympos. Pure Math. 33, Part 1, Amer. Math. Soc. (1979), 189–207; §4.

open scoped ContDiff

The product rule, over an abstract normed algebra

In a group of units, left translation is the restriction of a linear map, so the left invariant vector field with value X at 1 has value M * X at M, and the first-order operator is F ↦ fun M => fderiv ℝ F M (M * X) — no manifold structure needed. This section proves its product rule and bracket identity over an abstract algebra A; see the implementation notes for why A cannot simply be Matrix n n ℝ.

namespace AutomorphicForm.LieDerivAux

variable {A : Type*} [NormedRing A] [NormedAlgebra ℝ A]
  [FiniteDimensional ℝ A]

Right multiplication by X, as a continuous linear map.

noncomputable def mulRightL (X : A) : A →L[ℝ] A :=
  LinearMap.toContinuousLinearMap (LinearMap.mulRight ℝ X)

@[simp]
lemma mulRightL_apply (X M : A) : mulRightL X M = M * X := byA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AX:AM:A⊢ (mulRightL X) M = M * X simp [mulRightL]All goals completed! 🐙

The product rule for the left invariant derivative F ↦ fun M => D F M (M * X): its derivative at y in the direction v picks up the first-order term D F y (v * X), from differentiating M ↦ M * X, and the second-order term D² F y v (y * X).


lemma fderiv_rightDeriv_apply {F : A → ℂ} {y : A} (hF : ContDiffAt ℝ ∞ F y) (X v : A) :
    fderiv ℝ (fun M => fderiv ℝ F M (M * X)) y v
      = fderiv ℝ F y (v * X) + fderiv ℝ (fderiv ℝ F) y v (y * X) := byA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:A⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)
  have h₁ : HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) y :=
    ((hF.fderiv_right (m := ∞) (byA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:A⊢ ∞ + 1 ≤ ∞A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X) simpAll goals completed! 🐙A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X))).differentiableAt (byA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:A⊢ ∞ ≠ 0A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X) simpAll goals completed! 🐙A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X))).hasFDerivAtA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)
  have h₂ : HasFDerivAt (fun M : A => M * X) (mulRightL X) y := (mulRightL X).hasFDerivAtA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) yh₂:HasFDerivAt (fun M ↦ M * X) (mulRightL X) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)
  have h₃ := ((isBoundedBilinearMap_apply (𝕜 := ℝ) (E := A) (F := ℂ)).hasFDerivAt
    (fderiv ℝ F y, y * X)).comp y (h₁.prodMk h₂)A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) yh₂:HasFDerivAt (fun M ↦ M * X) (mulRightL X) yh₃:HasFDerivAt ((fun p ↦ p.1 p.2) ∘ fun x ↦ (fderiv ℝ F x, x * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)
  have h₄ : HasFDerivAt (fun M : A => fderiv ℝ F M (M * X)) _ y := h₃A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) yh₂:HasFDerivAt (fun M ↦ M * X) (mulRightL X) yh₃:HasFDerivAt ((fun p ↦ p.1 p.2) ∘ fun x ↦ (fderiv ℝ F x, x * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) yh₄:HasFDerivAt (fun M ↦ (fderiv ℝ F M) (M * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) y⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) v = (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)
  rw [h₄.fderivA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) yh₂:HasFDerivAt (fun M ↦ M * X) (mulRightL X) yh₃:HasFDerivAt ((fun p ↦ p.1 p.2) ∘ fun x ↦ (fderiv ℝ F x, x * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) yh₄:HasFDerivAt (fun M ↦ (fderiv ℝ F M) (M * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) y⊢ (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) v =
  (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) yh₂:HasFDerivAt (fun M ↦ M * X) (mulRightL X) yh₃:HasFDerivAt ((fun p ↦ p.1 p.2) ∘ fun x ↦ (fderiv ℝ F x, x * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) yh₄:HasFDerivAt (fun M ↦ (fderiv ℝ F M) (M * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) y⊢ (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) v =
  (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)]A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:Av:Ah₁:HasFDerivAt (fderiv ℝ F) (fderiv ℝ (fderiv ℝ F) y) yh₂:HasFDerivAt (fun M ↦ M * X) (mulRightL X) yh₃:HasFDerivAt ((fun p ↦ p.1 p.2) ∘ fun x ↦ (fderiv ℝ F x, x * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) yh₄:HasFDerivAt (fun M ↦ (fderiv ℝ F M) (M * X))
  (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) y⊢ (⋯.deriv (fderiv ℝ F y, y * X) ∘SL (fderiv ℝ (fderiv ℝ F) y).prod (mulRightL X)) v =
  (fderiv ℝ F y) (v * X) + ((fderiv ℝ (fderiv ℝ F) y) v) (y * X)
  simp [IsBoundedBilinearMap.deriv_apply]All goals completed! 🐙

The commutator of two left invariant derivatives is the left invariant derivative along the commutator: the second-order terms cancel by symmetry of the second derivative.


lemma fderiv_rightDeriv_sub_comm {F : A → ℂ} {y : A} (hF : ContDiffAt ℝ ∞ F y) (X Y : A) :
    fderiv ℝ (fun M => fderiv ℝ F M (M * Y)) y (y * X)
      - fderiv ℝ (fun M => fderiv ℝ F M (M * X)) y (y * Y)
      = fderiv ℝ F y (y * (X * Y - Y * X)) := byA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:A⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * Y)) y) (y * X) - (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))
  have hle : minSmoothness ℝ 2 ≤ (∞ : WithTop ℕ∞) := by
    rw [minSmoothness_of_isRCLikeNormedFieldA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:A⊢ 2 ≤ ∞A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:A⊢ 2 ≤ ∞A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * Y)) y) (y * X) - (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))]A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:A⊢ 2 ≤ ∞A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * Y)) y) (y * X) - (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X)); exact WithTop.coe_le_coe.mpr le_topA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * Y)) y) (y * X) - (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * Y)) y) (y * X) - (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))
  have hsymm := (hF.isSymmSndFDerivAt hle).eq (y * X) (y * Y)A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * Y)) y) (y * X) - (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))
  rw [fderiv_rightDeriv_apply hF Y (y * X),A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * X * Y) - (fderiv ℝ F y) (y * Y * X) fderiv_rightDeriv_apply hF X (y * Y),A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * X * Y) - (fderiv ℝ F y) (y * Y * X)
    show y * (X * Y - Y * X) = y * X * Y - y * Y * X byA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:A⊢ (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * Y)) y) (y * X) - (fderiv ℝ (fun M ↦ (fderiv ℝ F M) (M * X)) y) (y * Y) =
  (fderiv ℝ F y) (y * (X * Y - Y * X))A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * X * Y) - (fderiv ℝ F y) (y * Y * X) noncomm_ringAll goals completed! 🐙A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * X * Y) - (fderiv ℝ F y) (y * Y * X), map_subA:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * X * Y) - (fderiv ℝ F y) (y * Y * X)A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * X * Y) - (fderiv ℝ F y) (y * Y * X)]A:Type u_1inst✝²:NormedRing Ainst✝¹:NormedAlgebra ℝ Ainst✝:FiniteDimensional ℝ AF:A → ℂy:AhF:ContDiffAt ℝ ∞ F yX:AY:Ahle:minSmoothness ℝ 2 ≤ ∞hsymm:((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) = ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)⊢ (fderiv ℝ F y) (y * X * Y) + ((fderiv ℝ (fderiv ℝ F) y) (y * X)) (y * Y) -
    ((fderiv ℝ F y) (y * Y * X) + ((fderiv ℝ (fderiv ℝ F) y) (y * Y)) (y * X)) =
  (fderiv ℝ F y) (y * X * Y) - (fderiv ℝ F y) (y * Y * X)
  linear_combination hsymmAll goals completed! 🐙

end AutomorphicForm.LieDerivAuxnamespace Matrix.GeneralLinearGroupvariable {n : Type*} [Fintype n] [DecidableEq n]

Smooth functions on `GL n ℝ`

section Smoothopen scoped Matrix.Norms.Frobenius

φ : GL n ℝ → ℂ is C^∞: it extends to a C^∞ function on the open set of invertible matrices. Stating it this way avoids putting a manifold structure on GL n ℝ.

def IsSmoothOnGL (φ : GL n ℝ → ℂ) : Prop :=
  ∃ F : Matrix n n ℝ → ℂ, ContDiffOn ℝ ∞ F {M : Matrix n n ℝ | IsUnit M} ∧
    ∀ y : GL n ℝ, F (y : Matrix n n ℝ) = φ y

lemma isSmoothOnGL_const (c : ℂ) : IsSmoothOnGL (fun _ : GL n ℝ => c) :=
  ⟨fun _ => c, contDiffOn_const, fun _ => rfl⟩

lemma IsSmoothOnGL.add {φ ψ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (hψ : IsSmoothOnGL ψ) :
    IsSmoothOnGL (φ + ψ) := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψ⊢ IsSmoothOnGL (φ + ψ)
  obtain ⟨F, hF, hFφ⟩ := hφn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhψ:IsSmoothOnGL ψF:Matrix n n ℝ → ℂhF:ContDiffOn ℝ ∞ F {M | IsUnit M}hFφ:∀ (y : GL n ℝ), F ↑y = φ y⊢ IsSmoothOnGL (φ + ψ)
  obtain ⟨G, hG, hGψ⟩ := hψn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhF:ContDiffOn ℝ ∞ F {M | IsUnit M}hFφ:∀ (y : GL n ℝ), F ↑y = φ yG:Matrix n n ℝ → ℂhG:ContDiffOn ℝ ∞ G {M | IsUnit M}hGψ:∀ (y : GL n ℝ), G ↑y = ψ y⊢ IsSmoothOnGL (φ + ψ)
  exact ⟨F + G, ContDiffOn.add hF hG, fun y => byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhF:ContDiffOn ℝ ∞ F {M | IsUnit M}hFφ:∀ (y : GL n ℝ), F ↑y = φ yG:Matrix n n ℝ → ℂhG:ContDiffOn ℝ ∞ G {M | IsUnit M}hGψ:∀ (y : GL n ℝ), G ↑y = ψ yy:GL n ℝ⊢ (F + G) ↑y = (φ + ψ) y simp [hFφ, hGψ]All goals completed! 🐙⟩

lemma IsSmoothOnGL.const_smul {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (c : ℂ) :
    IsSmoothOnGL (c • φ) := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂ⊢ IsSmoothOnGL (c • φ)
  obtain ⟨F, hF, hFφ⟩ := hφn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂc:ℂF:Matrix n n ℝ → ℂhF:ContDiffOn ℝ ∞ F {M | IsUnit M}hFφ:∀ (y : GL n ℝ), F ↑y = φ y⊢ IsSmoothOnGL (c • φ)
  exact ⟨c • F, ContDiffOn.const_smul c hF, fun y => byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂc:ℂF:Matrix n n ℝ → ℂhF:ContDiffOn ℝ ∞ F {M | IsUnit M}hFφ:∀ (y : GL n ℝ), F ↑y = φ yy:GL n ℝ⊢ (c • F) ↑y = (c • φ) y simp [hFφ]All goals completed! 🐙⟩

The invertible matrices are an open set: they are the nonvanishing locus of det.


lemma isOpen_setOf_isUnit : IsOpen {M : Matrix n n ℝ | IsUnit M} := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq n⊢ IsOpen {M | IsUnit M}
  have h : {M : Matrix n n ℝ | IsUnit M}
      = (fun M : Matrix n n ℝ => M.det) ⁻¹' {x : ℝ | x ≠ 0} := by
    ext Mn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nM:Matrix n n ℝ⊢ M ∈ {M | IsUnit M} ↔ M ∈ (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nh:{M | IsUnit M} = (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}⊢ IsOpen {M | IsUnit M}
    simp [Matrix.isUnit_iff_isUnit_det, isUnit_iff_ne_zero]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nh:{M | IsUnit M} = (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}⊢ IsOpen {M | IsUnit M}n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nh:{M | IsUnit M} = (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}⊢ IsOpen {M | IsUnit M}
  rw [hn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nh:{M | IsUnit M} = (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}⊢ IsOpen ((fun M ↦ M.det) ⁻¹' {x | x ≠ 0})n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nh:{M | IsUnit M} = (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}⊢ IsOpen ((fun M ↦ M.det) ⁻¹' {x | x ≠ 0})]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nh:{M | IsUnit M} = (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}⊢ IsOpen ((fun M ↦ M.det) ⁻¹' {x | x ≠ 0})
  exact isOpen_ne.preimage (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nh:{M | IsUnit M} = (fun M ↦ M.det) ⁻¹' {x | x ≠ 0}⊢ Continuous fun M ↦ M.det fun_propAll goals completed! 🐙)

lemma isUnit_coe (y : GL n ℝ) : IsUnit (y : Matrix n n ℝ) := ⟨y, rfl⟩

A choice of C^∞ extension of φ to the invertible matrices, when one exists. Only its germ at each invertible matrix matters, by fderiv_extendGL_eq.

noncomputable def extendGL (φ : GL n ℝ → ℂ) : Matrix n n ℝ → ℂ :=
  haveI := Classical.propDecidable (IsSmoothOnGL φ)
  if h : IsSmoothOnGL φ then h.choose else 0



lemma contDiffOn_extendGL {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) :
    ContDiffOn ℝ ∞ (extendGL φ) {M : Matrix n n ℝ | IsUnit M} := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φ⊢ ContDiffOn ℝ ∞ (extendGL φ) {M | IsUnit M}
  rw [extendGL,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φ⊢ ContDiffOn ℝ ∞ (if h : IsSmoothOnGL φ then Exists.choose h else 0) {M | IsUnit M}n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φ⊢ ContDiffOn ℝ ∞ (Exists.choose hφ) {M | IsUnit M} dif_pos hφn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φ⊢ ContDiffOn ℝ ∞ (Exists.choose hφ) {M | IsUnit M}n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φ⊢ ContDiffOn ℝ ∞ (Exists.choose hφ) {M | IsUnit M}]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φ⊢ ContDiffOn ℝ ∞ (Exists.choose hφ) {M | IsUnit M}
  exact hφ.choose_spec.1All goals completed! 🐙



@[simp]
lemma extendGL_coe {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (y : GL n ℝ) :
    extendGL φ (y : Matrix n n ℝ) = φ y := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φy:GL n ℝ⊢ extendGL φ ↑y = φ y
  rw [extendGL,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φy:GL n ℝ⊢ (if h : IsSmoothOnGL φ then Exists.choose h else 0) ↑y = φ yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φy:GL n ℝ⊢ Exists.choose hφ ↑y = φ y dif_pos hφn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φy:GL n ℝ⊢ Exists.choose hφ ↑y = φ yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φy:GL n ℝ⊢ Exists.choose hφ ↑y = φ y]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φy:GL n ℝ⊢ Exists.choose hφ ↑y = φ y
  exact hφ.choose_spec.2 yAll goals completed! 🐙

lemma contDiffAt_extendGL {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (y : GL n ℝ) :
    ContDiffAt ℝ ∞ (extendGL φ) (y : Matrix n n ℝ) :=
  (contDiffOn_extendGL hφ).contDiffAt (isOpen_setOf_isUnit.mem_nhds (isUnit_coe y))

The derivative of the chosen extension at an invertible matrix does not depend on the choice: any two extensions of φ agree on the open set of invertible matrices.


lemma fderiv_extendGL_eq {φ : GL n ℝ → ℂ} {F : Matrix n n ℝ → ℂ} (hφ : IsSmoothOnGL φ)
    (hF : ∀ y : GL n ℝ, F (y : Matrix n n ℝ) = φ y) (y : GL n ℝ) :
    fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) = fderiv ℝ F (y : Matrix n n ℝ) := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhφ:IsSmoothOnGL φhF:∀ (y : GL n ℝ), F ↑y = φ yy:GL n ℝ⊢ fderiv ℝ (extendGL φ) ↑y = fderiv ℝ F ↑y
  refine Filter.EventuallyEq.fderiv_eq ?_n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhφ:IsSmoothOnGL φhF:∀ (y : GL n ℝ), F ↑y = φ yy:GL n ℝ⊢ extendGL φ =ᶠ[nhds ↑y] F
  filter_upwards [isOpen_setOf_isUnit.mem_nhds (isUnit_coe y)] with M hMn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhφ:IsSmoothOnGL φhF:∀ (y : GL n ℝ), F ↑y = φ yy:GL n ℝM:Matrix n n ℝhM:IsUnit M⊢ extendGL φ M = F M
  obtain ⟨u, rfl⟩ := hMn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhφ:IsSmoothOnGL φhF:∀ (y : GL n ℝ), F ↑y = φ yy:GL n ℝu:(Matrix n n ℝ)ˣ⊢ extendGL φ ↑u = F ↑u
  rw [extendGL_coe hφ,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhφ:IsSmoothOnGL φhF:∀ (y : GL n ℝ), F ↑y = φ yy:GL n ℝu:(Matrix n n ℝ)ˣ⊢ φ u = F ↑uAll goals completed! 🐙 hFn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂF:Matrix n n ℝ → ℂhφ:IsSmoothOnGL φhF:∀ (y : GL n ℝ), F ↑y = φ yy:GL n ℝu:(Matrix n n ℝ)ˣ⊢ φ u = φ uAll goals completed! 🐙]All goals completed! 🐙

Left invariant derivatives

(X • φ) y = d/dt φ (y * exp (t • X)) |_{t = 0}, proved equal to the directional derivative fderiv ℝ F y (y * X) of any smooth extension F (lieDerivFun_eq_fderiv), which is the form all its properties are established in.

The exponential of a matrix, as an element of GL n ℝ: exp X is invertible with inverse exp (-X).

noncomputable def expGL (X : Matrix n n ℝ) : GL n ℝ := (NormedSpace.isUnit_exp X).unit

@[simp]
lemma coe_expGL (X : Matrix n n ℝ) : (expGL X : Matrix n n ℝ) = NormedSpace.exp X :=
  (NormedSpace.isUnit_exp X).unit_spec

@[simp]
lemma expGL_zero : expGL (0 : Matrix n n ℝ) = 1 := Units.ext (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq n⊢ ↑(expGL 0) = ↑1 simpAll goals completed! 🐙)

The left invariant derivative of φ along X: differentiate φ along the one-parameter subgroup t ↦ exp (t • X) acting on the right,

(X • φ) y = d/dt φ (y * exp (t • X)) |_{t = 0}.

This is the derivative that condition (c) of the definition of an automorphic form is about: the left invariant vector field with value X at 1 has value y * X at y, and lieDerivFun_eq_fderiv identifies the two descriptions for C^∞ functions.

noncomputable def lieDerivFun (X : Matrix n n ℝ) (φ : GL n ℝ → ℂ) (y : GL n ℝ) : ℂ :=
  deriv (fun t : ℝ => φ (y * expGL (t • X))) 0

Differentiating along the one-parameter subgroup computes the derivative of any smooth extension in the direction y * X.


lemma hasDerivAt_lieDerivFun {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X : Matrix n n ℝ)
    (y : GL n ℝ) :
    HasDerivAt (fun t : ℝ => φ (y * expGL (t • X)))
      (fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) ((y : Matrix n n ℝ) * X)) 0 := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝ⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0
  -- The instance arguments on `Matrix n n ℝ` are deliberately never written out here: see the
  -- implementation notes. Every one of them arrives by unification from a Mathlib lemma.
  have hexp := (hasDerivAt_exp_smul_const X (0 : ℝ)).const_mul (y : Matrix n n ℝ)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * (NormedSpace.exp (0 • X) * X)) 0⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0
  simp only [zero_smul, NormedSpace.exp_zero, one_mul] at hexpn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0
  have hfun : (fun t : ℝ => φ (y * expGL (t • X)))
      = fun t : ℝ => extendGL φ ((y : Matrix n n ℝ) * NormedSpace.exp (t • X)) := by
    funext tn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0t:ℝ⊢ φ (y * expGL (t • X)) = extendGL φ (↑y * NormedSpace.exp (t • X))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0
    rw [← extendGL_coe hφ (y * expGL (t • X))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0t:ℝ⊢ extendGL φ ↑(y * expGL (t • X)) = extendGL φ (↑y * NormedSpace.exp (t • X))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0t:ℝ⊢ extendGL φ ↑(y * expGL (t • X)) = extendGL φ (↑y * NormedSpace.exp (t • X))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0t:ℝ⊢ extendGL φ ↑(y * expGL (t • X)) = extendGL φ (↑y * NormedSpace.exp (t • X))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0
    simpn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ φ (y * expGL (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0
  rw [hfunn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ HasDerivAt (fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))) ((fderiv ℝ (extendGL φ) ↑y) (↑y * X)) 0
  exact HasFDerivAt.comp_hasDerivAt_of_eq
    (hl := ((contDiffAt_extendGL hφ y).differentiableAt (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ ∞ ≠ 0 simpAll goals completed! 🐙)).hasFDerivAt)
    (hf := hexp) (hy := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝy:GL n ℝhexp:HasDerivAt (fun y_1 ↦ ↑y * NormedSpace.exp (y_1 • X)) (↑y * X) 0hfun:(fun t ↦ φ (y * expGL (t • X))) = fun t ↦ extendGL φ (↑y * NormedSpace.exp (t • X))⊢ ↑y = ↑y * NormedSpace.exp (0 • X) simpAll goals completed! 🐙)

The one-parameter-subgroup description of the left invariant derivative agrees with the directional-derivative one. Every algebraic property below is proved through this bridge.

lemma lieDerivFun_eq_fderiv {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X : Matrix n n ℝ)
    (y : GL n ℝ) :
    lieDerivFun X φ y
      = fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) ((y : Matrix n n ℝ) * X) :=
  (hasDerivAt_lieDerivFun hφ X y).deriv

lemma IsSmoothOnGL.lieDerivFun {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X : Matrix n n ℝ) :
    IsSmoothOnGL (lieDerivFun X φ) := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝ⊢ IsSmoothOnGL (GeneralLinearGroup.lieDerivFun X φ)
  refine ⟨fun M => fderiv ℝ (extendGL φ) M (M * X), fun M hM => ?_,
    fun y => (lieDerivFun_eq_fderiv hφ X y).symm⟩n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝM:Matrix n n ℝhM:M ∈ {M | IsUnit M}⊢ ContDiffWithinAt ℝ ∞ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) {M | IsUnit M} M
  have h : ContDiffAt ℝ ∞ (extendGL φ) M :=
    (contDiffOn_extendGL hφ).contDiffAt (isOpen_setOf_isUnit.mem_nhds hM)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝM:Matrix n n ℝhM:M ∈ {M | IsUnit M}h:ContDiffAt ℝ ∞ (extendGL φ) M⊢ ContDiffWithinAt ℝ ∞ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) {M | IsUnit M} M
  exact (((h.fderiv_right (m := ∞) (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝM:Matrix n n ℝhM:M ∈ {M | IsUnit M}h:ContDiffAt ℝ ∞ (extendGL φ) M⊢ ∞ + 1 ≤ ∞ simpAll goals completed! 🐙)).clm_apply
    (contDiffAt_id.mul contDiffAt_const))).contDiffWithinAt

The ℂ-submodule of C^∞ functions on GL n ℝ, which is what the Lie algebra and hence the universal enveloping algebra acts on.

def smoothGL (n : Type*) [Fintype n] [DecidableEq n] : Submodule ℂ (GL n ℝ → ℂ) where
  carrier := {φ | IsSmoothOnGL φ}
  zero_mem' := isSmoothOnGL_const 0
  add_mem' hφ hψ := hφ.add hψ
  smul_mem' c _ hφ := hφ.const_smul c

@[simp]
lemma mem_smoothGL {φ : GL n ℝ → ℂ} : φ ∈ smoothGL n ↔ IsSmoothOnGL φ := Iff.rfl



lemma lieDerivFun_add {φ ψ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (hψ : IsSmoothOnGL ψ)
    (X : Matrix n n ℝ) : lieDerivFun X (φ + ψ) = lieDerivFun X φ + lieDerivFun X ψ := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝ⊢ lieDerivFun X (φ + ψ) = lieDerivFun X φ + lieDerivFun X ψ
  funext yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝ⊢ lieDerivFun X (φ + ψ) y = (lieDerivFun X φ + lieDerivFun X ψ) y
  have hadd : fderiv ℝ (extendGL φ + extendGL ψ) (y : Matrix n n ℝ)
      = fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) + fderiv ℝ (extendGL ψ) (y : Matrix n n ℝ) :=
    ((((contDiffAt_extendGL hφ y).differentiableAt (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝ⊢ ∞ ≠ 0n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ lieDerivFun X (φ + ψ) y = (lieDerivFun X φ + lieDerivFun X ψ) y simpAll goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ lieDerivFun X (φ + ψ) y = (lieDerivFun X φ + lieDerivFun X ψ) y)).hasFDerivAt).add
      (((contDiffAt_extendGL hψ y).differentiableAt (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝ⊢ ∞ ≠ 0n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ lieDerivFun X (φ + ψ) y = (lieDerivFun X φ + lieDerivFun X ψ) y simpAll goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ lieDerivFun X (φ + ψ) y = (lieDerivFun X φ + lieDerivFun X ψ) y)).hasFDerivAt)).fderivn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ lieDerivFun X (φ + ψ) y = (lieDerivFun X φ + lieDerivFun X ψ) y
  rw [lieDerivFun_eq_fderiv (hφ.add hψ),n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ (fderiv ℝ (extendGL (φ + ψ)) ↑y) (↑y * X) = (lieDerivFun X φ + lieDerivFun X ψ) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y) (↑y * X) = (lieDerivFun X φ + lieDerivFun X ψ) y fderiv_extendGL_eq (hφ.add hψ)
    (F := extendGL φ + extendGL ψ)
    (fun z => byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑yz:GL n ℝ⊢ (extendGL φ + extendGL ψ) ↑z = (φ + ψ) zn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y) (↑y * X) = (lieDerivFun X φ + lieDerivFun X ψ) y simp [extendGL_coe hφ, extendGL_coe hψ]All goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y) (↑y * X) = (lieDerivFun X φ + lieDerivFun X ψ) y) y, haddn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y) (↑y * X) = (lieDerivFun X φ + lieDerivFun X ψ) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y) (↑y * X) = (lieDerivFun X φ + lieDerivFun X ψ) y]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂψ:GL n ℝ → ℂhφ:IsSmoothOnGL φhψ:IsSmoothOnGL ψX:Matrix n n ℝy:GL n ℝhadd:fderiv ℝ (extendGL φ + extendGL ψ) ↑y = fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y + fderiv ℝ (extendGL ψ) ↑y) (↑y * X) = (lieDerivFun X φ + lieDerivFun X ψ) y
  simp [lieDerivFun_eq_fderiv hφ, lieDerivFun_eq_fderiv hψ]All goals completed! 🐙



lemma lieDerivFun_const_smul {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (c : ℂ)
    (X : Matrix n n ℝ) : lieDerivFun X (c • φ) = c • lieDerivFun X φ := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝ⊢ lieDerivFun X (c • φ) = c • lieDerivFun X φ
  funext yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝ⊢ lieDerivFun X (c • φ) y = (c • lieDerivFun X φ) y
  have hsmul : fderiv ℝ (c • extendGL φ) (y : Matrix n n ℝ)
      = c • fderiv ℝ (extendGL φ) (y : Matrix n n ℝ) :=
    ((((contDiffAt_extendGL hφ y).differentiableAt (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝ⊢ ∞ ≠ 0n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ lieDerivFun X (c • φ) y = (c • lieDerivFun X φ) y simpAll goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ lieDerivFun X (c • φ) y = (c • lieDerivFun X φ) y)).hasFDerivAt).const_smul c).fderivn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ lieDerivFun X (c • φ) y = (c • lieDerivFun X φ) y
  rw [lieDerivFun_eq_fderiv (hφ.const_smul c),n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ (fderiv ℝ (extendGL (c • φ)) ↑y) (↑y * X) = (c • lieDerivFun X φ) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ (c • fderiv ℝ (extendGL φ) ↑y) (↑y * X) = (c • lieDerivFun X φ) y fderiv_extendGL_eq (hφ.const_smul c)
    (F := c • extendGL φ) (fun z => byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑yz:GL n ℝ⊢ (c • extendGL φ) ↑z = (c • φ) zn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ (c • fderiv ℝ (extendGL φ) ↑y) (↑y * X) = (c • lieDerivFun X φ) y simp [extendGL_coe hφ]All goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ (c • fderiv ℝ (extendGL φ) ↑y) (↑y * X) = (c • lieDerivFun X φ) y) y, hsmuln:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ (c • fderiv ℝ (extendGL φ) ↑y) (↑y * X) = (c • lieDerivFun X φ) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ (c • fderiv ℝ (extendGL φ) ↑y) (↑y * X) = (c • lieDerivFun X φ) y]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φc:ℂX:Matrix n n ℝy:GL n ℝhsmul:fderiv ℝ (c • extendGL φ) ↑y = c • fderiv ℝ (extendGL φ) ↑y⊢ (c • fderiv ℝ (extendGL φ) ↑y) (↑y * X) = (c • lieDerivFun X φ) y
  simp [lieDerivFun_eq_fderiv hφ]All goals completed! 🐙

@[simp]
lemma lieDerivFun_zero_left (φ : GL n ℝ → ℂ) : lieDerivFun 0 φ = 0 := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂ⊢ lieDerivFun 0 φ = 0
  funext yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂy:GL n ℝ⊢ lieDerivFun 0 φ y = 0 y; simp [lieDerivFun]All goals completed! 🐙

lemma lieDerivFun_add_left {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X X' : Matrix n n ℝ) :
    lieDerivFun (X + X') φ = lieDerivFun X φ + lieDerivFun X' φ := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDerivFun (X + X') φ = lieDerivFun X φ + lieDerivFun X' φ
  funext yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝX':Matrix n n ℝy:GL n ℝ⊢ lieDerivFun (X + X') φ y = (lieDerivFun X φ + lieDerivFun X' φ) y
  simp [lieDerivFun_eq_fderiv hφ, mul_add]All goals completed! 🐙

lemma lieDerivFun_smul_left {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (r : ℝ) (X : Matrix n n ℝ) :
    lieDerivFun (r • X) φ = r • lieDerivFun X φ := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φr:ℝX:Matrix n n ℝ⊢ lieDerivFun (r • X) φ = r • lieDerivFun X φ
  funext yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φr:ℝX:Matrix n n ℝy:GL n ℝ⊢ lieDerivFun (r • X) φ y = (r • lieDerivFun X φ) y
  simp [lieDerivFun_eq_fderiv hφ]All goals completed! 🐙

lemma lieDerivFun_const (X : Matrix n n ℝ) (c : ℂ) :
    lieDerivFun X (fun _ : GL n ℝ => c) = 0 := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝc:ℂ⊢ (lieDerivFun X fun x ↦ c) = 0
  funext yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝc:ℂy:GL n ℝ⊢ lieDerivFun X (fun x ↦ c) y = 0 y
  simp [lieDerivFun]All goals completed! 🐙

The left invariant derivative along X as a ℂ-linear endomorphism of the C^∞ functions on GL n ℝ.

noncomputable def lieDeriv (X : Matrix n n ℝ) : smoothGL n →ₗ[ℂ] smoothGL n where
  toFun φ := ⟨lieDerivFun X (φ : GL n ℝ → ℂ), φ.2.lieDerivFun X⟩
  map_add' φ ψ := Subtype.ext (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝφ:↥(smoothGL n)ψ:↥(smoothGL n)⊢ ↑⟨lieDerivFun X ↑(φ + ψ), ⋯⟩ = ↑(⟨lieDerivFun X ↑φ, ⋯⟩ + ⟨lieDerivFun X ↑ψ, ⋯⟩) simpa using lieDerivFun_add φ.2 ψ.2 XAll goals completed! 🐙)
  map_smul' c φ := Subtype.ext (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝc:ℂφ:↥(smoothGL n)⊢ ↑⟨lieDerivFun X ↑(c • φ), ⋯⟩ = ↑((RingHom.id ℂ) c • ⟨lieDerivFun X ↑φ, ⋯⟩) simpa using lieDerivFun_const_smul φ.2 c XAll goals completed! 🐙)

@[simp]
lemma coe_lieDeriv (X : Matrix n n ℝ) (φ : smoothGL n) :
    (lieDeriv X φ : GL n ℝ → ℂ) = lieDerivFun X (φ : GL n ℝ → ℂ) := rfl

The commutator of two left invariant derivatives is the left invariant derivative along the commutator of the directions. This is the bracket identity that makes lieDeriv a Lie algebra homomorphism; the second-order terms cancel by symmetry of the second derivative.


lemma lieDerivFun_bracket {φ : GL n ℝ → ℂ} (hφ : IsSmoothOnGL φ) (X Y : Matrix n n ℝ) :
    lieDerivFun (X * Y - Y * X) φ
      = lieDerivFun X (lieDerivFun Y φ) - lieDerivFun Y (lieDerivFun X φ) := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝ⊢ lieDerivFun (X * Y - Y * X) φ = lieDerivFun X (lieDerivFun Y φ) - lieDerivFun Y (lieDerivFun X φ)
  funext yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝ⊢ lieDerivFun (X * Y - Y * X) φ y = (lieDerivFun X (lieDerivFun Y φ) - lieDerivFun Y (lieDerivFun X φ)) y
  have hY : fderiv ℝ (extendGL (lieDerivFun Y φ)) (y : Matrix n n ℝ)
      = fderiv ℝ (fun M => fderiv ℝ (extendGL φ) M (M * Y)) (y : Matrix n n ℝ) :=
    fderiv_extendGL_eq (hφ.lieDerivFun Y) (fun z => (lieDerivFun_eq_fderiv hφ Y z).symm) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y⊢ lieDerivFun (X * Y - Y * X) φ y = (lieDerivFun X (lieDerivFun Y φ) - lieDerivFun Y (lieDerivFun X φ)) y
  have hX : fderiv ℝ (extendGL (lieDerivFun X φ)) (y : Matrix n n ℝ)
      = fderiv ℝ (fun M => fderiv ℝ (extendGL φ) M (M * X)) (y : Matrix n n ℝ) :=
    fderiv_extendGL_eq (hφ.lieDerivFun X) (fun z => (lieDerivFun_eq_fderiv hφ X z).symm) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ lieDerivFun (X * Y - Y * X) φ y = (lieDerivFun X (lieDerivFun Y φ) - lieDerivFun Y (lieDerivFun X φ)) y
  rw [Pi.sub_apply,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ lieDerivFun (X * Y - Y * X) φ y = lieDerivFun X (lieDerivFun Y φ) y - lieDerivFun Y (lieDerivFun X φ) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y) lieDerivFun_eq_fderiv hφ (X * Y - Y * X) y,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  lieDerivFun X (lieDerivFun Y φ) y - lieDerivFun Y (lieDerivFun X φ) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y)
    lieDerivFun_eq_fderiv (hφ.lieDerivFun Y) X y,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y) (↑y * X) - lieDerivFun Y (lieDerivFun X φ) yn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y) lieDerivFun_eq_fderiv (hφ.lieDerivFun X) Y y,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y) (↑y * X) - (fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y) (↑y * Y)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y)
    hX,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y) hYn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y)]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:GL n ℝ → ℂhφ:IsSmoothOnGL φX:Matrix n n ℝY:Matrix n n ℝy:GL n ℝhY:fderiv ℝ (extendGL (lieDerivFun Y φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑yhX:fderiv ℝ (extendGL (lieDerivFun X φ)) ↑y = fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y⊢ (fderiv ℝ (extendGL φ) ↑y) (↑y * (X * Y - Y * X)) =
  (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * Y)) ↑y) (↑y * X) -
    (fderiv ℝ (fun M ↦ (fderiv ℝ (extendGL φ) M) (M * X)) ↑y) (↑y * Y)
  exact (AutomorphicForm.LieDerivAux.fderiv_rightDeriv_sub_comm
    (contDiffAt_extendGL hφ y) X Y).symmAll goals completed! 🐙

lemma lieDeriv_bracket (X Y : Matrix n n ℝ) :
    lieDeriv (X * Y - Y * X) = lieDeriv X * lieDeriv Y - lieDeriv Y * lieDeriv X := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝY:Matrix n n ℝ⊢ lieDeriv (X * Y - Y * X) = lieDeriv X * lieDeriv Y - lieDeriv Y * lieDeriv X
  refine LinearMap.ext fun φ => Subtype.ext ?_n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝY:Matrix n n ℝφ:↥(smoothGL n)⊢ ↑((lieDeriv (X * Y - Y * X)) φ) = ↑((lieDeriv X * lieDeriv Y - lieDeriv Y * lieDeriv X) φ)
  simpa using lieDerivFun_bracket φ.2 X YAll goals completed! 🐙

@[simp]
lemma lieDeriv_zero : lieDeriv (0 : Matrix n n ℝ) = 0 :=
  LinearMap.ext fun φ => Subtype.ext (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nφ:↥(smoothGL n)⊢ ↑((lieDeriv 0) φ) = ↑(0 φ) simpAll goals completed! 🐙)

lemma lieDeriv_add (X X' : Matrix n n ℝ) : lieDeriv (X + X') = lieDeriv X + lieDeriv X' :=
  LinearMap.ext fun φ => Subtype.ext (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝφ:↥(smoothGL n)⊢ ↑((lieDeriv (X + X')) φ) = ↑((lieDeriv X + lieDeriv X') φ) simpa using lieDerivFun_add_left φ.2 X X'All goals completed! 🐙)

lemma lieDeriv_real_smul (r : ℝ) (X : Matrix n n ℝ) :
    lieDeriv (r • X) = (r : ℂ) • lieDeriv X :=
  LinearMap.ext fun φ => Subtype.ext (byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nr:ℝX:Matrix n n ℝφ:↥(smoothGL n)⊢ ↑((lieDeriv (r • X)) φ) = ↑((↑r • lieDeriv X) φ) simpa using lieDerivFun_smul_left φ.2 r XAll goals completed! 🐙)



lemma lieDeriv_neg (X : Matrix n n ℝ) : lieDeriv (-X) = -lieDeriv X := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ lieDeriv (-X) = -lieDeriv X
  rw [show -X = (-1 : ℝ) • X byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ lieDeriv (-X) = -lieDeriv Xn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ ↑(-1) • lieDeriv X = -lieDeriv X simpAll goals completed! 🐙n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ ↑(-1) • lieDeriv X = -lieDeriv X, lieDeriv_real_smuln:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ ↑(-1) • lieDeriv X = -lieDeriv Xn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ ↑(-1) • lieDeriv X = -lieDeriv X]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ ↑(-1) • lieDeriv X = -lieDeriv X
  push_castn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝ⊢ -1 • lieDeriv X = -lieDeriv X
  moduleAll goals completed! 🐙



lemma lieDeriv_sub (X X' : Matrix n n ℝ) : lieDeriv (X - X') = lieDeriv X - lieDeriv X' := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv (X - X') = lieDeriv X - lieDeriv X'
  rw [sub_eq_add_neg,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv (X + -X') = lieDeriv X - lieDeriv X'n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv X + -lieDeriv X' = lieDeriv X - lieDeriv X' lieDeriv_add,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv X + lieDeriv (-X') = lieDeriv X - lieDeriv X'n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv X + -lieDeriv X' = lieDeriv X - lieDeriv X' lieDeriv_negn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv X + -lieDeriv X' = lieDeriv X - lieDeriv X'n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv X + -lieDeriv X' = lieDeriv X - lieDeriv X']n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nX:Matrix n n ℝX':Matrix n n ℝ⊢ lieDeriv X + -lieDeriv X' = lieDeriv X - lieDeriv X'
  abelAll goals completed! 🐙

Complexification

𝔤𝔩 n ℂ = 𝔤𝔩 n ℝ ⊗ ℂ acts by X + i Y ↦ lieDeriv X + i • lieDeriv Y. Since the entrywise real and imaginary parts turn complex matrix multiplication into the expected pair of real products, the bracket identity over ℝ gives the bracket identity over ℂ.

sectionomit [Fintype n] [DecidableEq n]

lemma map_re_add (Z W : Matrix n n ℂ) :
    (Z + W).map Complex.re = Z.map Complex.re + W.map Complex.re :=
  Matrix.map_add _ Complex.add_re Z W

lemma map_im_add (Z W : Matrix n n ℂ) :
    (Z + W).map Complex.im = Z.map Complex.im + W.map Complex.im :=
  Matrix.map_add _ Complex.add_im Z W

lemma map_re_sub (Z W : Matrix n n ℂ) :
    (Z - W).map Complex.re = Z.map Complex.re - W.map Complex.re :=
  Matrix.map_sub _ Complex.sub_re Z W

lemma map_im_sub (Z W : Matrix n n ℂ) :
    (Z - W).map Complex.im = Z.map Complex.im - W.map Complex.im :=
  Matrix.map_sub _ Complex.sub_im Z W

lemma map_re_smul (c : ℂ) (Z : Matrix n n ℂ) :
    (c • Z).map Complex.re = c.re • Z.map Complex.re - c.im • Z.map Complex.im := byn:Type u_1c:ℂZ:Matrix n n ℂ⊢ (c • Z).map Complex.re = c.re • Z.map Complex.re - c.im • Z.map Complex.im
  ext i jn:Type u_1c:ℂZ:Matrix n n ℂi:nj:n⊢ (c • Z).map Complex.re i j = (c.re • Z.map Complex.re - c.im • Z.map Complex.im) i j; simp [Complex.mul_re]All goals completed! 🐙

lemma map_im_smul (c : ℂ) (Z : Matrix n n ℂ) :
    (c • Z).map Complex.im = c.re • Z.map Complex.im + c.im • Z.map Complex.re := byn:Type u_1c:ℂZ:Matrix n n ℂ⊢ (c • Z).map Complex.im = c.re • Z.map Complex.im + c.im • Z.map Complex.re
  ext i jn:Type u_1c:ℂZ:Matrix n n ℂi:nj:n⊢ (c • Z).map Complex.im i j = (c.re • Z.map Complex.im + c.im • Z.map Complex.re) i j; simp [Complex.mul_im]All goals completed! 🐙

endsectionomit [DecidableEq n]

lemma map_re_mul (Z W : Matrix n n ℂ) :
    (Z * W).map Complex.re
      = Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im := byn:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ (Z * W).map Complex.re = Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im
  ext i jn:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂi:nj:n⊢ (Z * W).map Complex.re i j = (Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im) i j
  simp [Matrix.mul_apply, Complex.mul_re, Finset.sum_sub_distrib]All goals completed! 🐙

lemma map_im_mul (Z W : Matrix n n ℂ) :
    (Z * W).map Complex.im
      = Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re := byn:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ (Z * W).map Complex.im = Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re
  ext i jn:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂi:nj:n⊢ (Z * W).map Complex.im i j = (Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re) i j
  simp [Matrix.mul_apply, Complex.mul_im, Finset.sum_add_distrib]All goals completed! 🐙

The real part of a complex commutator, arranged as a difference of two real commutators.


lemma map_re_bracket (Z W : Matrix n n ℂ) :
    (Z * W - W * Z).map Complex.re
      = (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re)
        - (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) := byn:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ (Z * W - W * Z).map Complex.re =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)
  rw [map_re_sub,n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ (Z * W).map Complex.re - (W * Z).map Complex.re =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im -
    (W.map Complex.re * Z.map Complex.re - W.map Complex.im * Z.map Complex.im) =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) map_re_mul,n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im - (W * Z).map Complex.re =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im -
    (W.map Complex.re * Z.map Complex.re - W.map Complex.im * Z.map Complex.im) =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) map_re_muln:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im -
    (W.map Complex.re * Z.map Complex.re - W.map Complex.im * Z.map Complex.im) =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im -
    (W.map Complex.re * Z.map Complex.re - W.map Complex.im * Z.map Complex.im) =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)]n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.re - Z.map Complex.im * W.map Complex.im -
    (W.map Complex.re * Z.map Complex.re - W.map Complex.im * Z.map Complex.im) =
  Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
    (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)
  abelAll goals completed! 🐙

The imaginary part of a complex commutator, arranged as a sum of two real commutators.


lemma map_im_bracket (Z W : Matrix n n ℂ) :
    (Z * W - W * Z).map Complex.im
      = (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re)
        + (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im) := byn:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ (Z * W - W * Z).map Complex.im =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)
  rw [map_im_sub,n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ (Z * W).map Complex.im - (W * Z).map Complex.im =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re -
    (W.map Complex.re * Z.map Complex.im + W.map Complex.im * Z.map Complex.re) =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im) map_im_mul,n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re - (W * Z).map Complex.im =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re -
    (W.map Complex.re * Z.map Complex.im + W.map Complex.im * Z.map Complex.re) =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im) map_im_muln:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re -
    (W.map Complex.re * Z.map Complex.im + W.map Complex.im * Z.map Complex.re) =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re -
    (W.map Complex.re * Z.map Complex.im + W.map Complex.im * Z.map Complex.re) =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)]n:Type u_1inst✝:Fintype nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Z.map Complex.re * W.map Complex.im + Z.map Complex.im * W.map Complex.re -
    (W.map Complex.re * Z.map Complex.im + W.map Complex.im * Z.map Complex.re) =
  Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
    (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)
  abelAll goals completed! 🐙

end

The action of the complexified Lie algebra 𝔤𝔩 n ℂ of GL n ℝ on the C^∞ functions: X + i Y acts as lieDeriv X + i • lieDeriv Y.

noncomputable def lieDerivC (Z : Matrix n n ℂ) : Module.End ℂ (smoothGL n) :=
  lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)

lemma lieDerivC_add (Z W : Matrix n n ℂ) : lieDerivC (Z + W) = lieDerivC Z + lieDerivC W := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDerivC (Z + W) = lieDerivC Z + lieDerivC W
  simp only [lieDerivC, map_re_add, map_im_add, lieDeriv_add, smul_add]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re) + lieDeriv (W.map Complex.re) +
    (Complex.I • lieDeriv (Z.map Complex.im) + Complex.I • lieDeriv (W.map Complex.im)) =
  lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im) +
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im))
  abelAll goals completed! 🐙



lemma lieDerivC_smul (c : ℂ) (Z : Matrix n n ℂ) : lieDerivC (c • Z) = c • lieDerivC Z := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂ⊢ lieDerivC (c • Z) = c • lieDerivC Z
  have key : ∀ (a b : ℝ) (W : Matrix n n ℂ),
      lieDerivC (((a : ℂ) + (b : ℂ) * Complex.I) • W)
        = ((a : ℂ) + (b : ℂ) * Complex.I) • lieDerivC W := by
    intro a b Wn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂa:ℝb:ℝW:Matrix n n ℂ⊢ lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC Wn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂkey:∀ (a b : ℝ) (W : Matrix n n ℂ), lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC W⊢ lieDerivC (c • Z) = c • lieDerivC Z
    simp only [lieDerivC, map_re_smul, map_im_smul, lieDeriv_sub, lieDeriv_add,
      lieDeriv_real_smul, Complex.add_re, Complex.add_im, Complex.ofReal_re, Complex.ofReal_im,
      Complex.mul_re, Complex.mul_im, Complex.I_re, Complex.I_im]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂa:ℝb:ℝW:Matrix n n ℂ⊢ ↑(a + (b * 0 - 0 * 1)) • lieDeriv (W.map Complex.re) - ↑(0 + (b * 1 + 0 * 0)) • lieDeriv (W.map Complex.im) +
    Complex.I •
      (↑(a + (b * 0 - 0 * 1)) • lieDeriv (W.map Complex.im) + ↑(0 + (b * 1 + 0 * 0)) • lieDeriv (W.map Complex.re)) =
  (↑a + ↑b * Complex.I) • (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂkey:∀ (a b : ℝ) (W : Matrix n n ℂ), lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC W⊢ lieDerivC (c • Z) = c • lieDerivC Z
    match_scalarsn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂa:ℝb:ℝW:Matrix n n ℂ⊢ (↑a + (↑b * 0 - 0 * 1)) * 1 + Complex.I * ((0 + (↑b * 1 + 0 * 0)) * 1) = (↑a + ↑b * Complex.I) * 1n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂa:ℝb:ℝW:Matrix n n ℂ⊢ -((0 + (↑b * 1 + 0 * 0)) * 1) + Complex.I * ((↑a + (↑b * 0 - 0 * 1)) * 1) = (↑a + ↑b * Complex.I) * (Complex.I * 1)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂkey:∀ (a b : ℝ) (W : Matrix n n ℂ), lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC W⊢ lieDerivC (c • Z) = c • lieDerivC Z
    all_goals ring_nfn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂa:ℝb:ℝW:Matrix n n ℂ⊢ -↑b + Complex.I * ↑a = ↑b * Complex.I ^ 2 + Complex.I * ↑an:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂkey:∀ (a b : ℝ) (W : Matrix n n ℂ), lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC W⊢ lieDerivC (c • Z) = c • lieDerivC Z
    all_goals (try simp only [Complex.I_sq]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂa:ℝb:ℝW:Matrix n n ℂ⊢ -↑b + Complex.I * ↑a = ↑b * -1 + Complex.I * ↑an:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂkey:∀ (a b : ℝ) (W : Matrix n n ℂ), lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC W⊢ lieDerivC (c • Z) = c • lieDerivC Z)
    all_goals ringn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂkey:∀ (a b : ℝ) (W : Matrix n n ℂ), lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC W⊢ lieDerivC (c • Z) = c • lieDerivC Zn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nc:ℂZ:Matrix n n ℂkey:∀ (a b : ℝ) (W : Matrix n n ℂ), lieDerivC ((↑a + ↑b * Complex.I) • W) = (↑a + ↑b * Complex.I) • lieDerivC W⊢ lieDerivC (c • Z) = c • lieDerivC Z
  simpa [Complex.re_add_im] using key c.re c.im ZAll goals completed! 🐙



lemma lieDerivC_bracket (Z W : Matrix n n ℂ) :
    lieDerivC (Z * W - W * Z) = lieDerivC Z * lieDerivC W - lieDerivC W * lieDerivC Z := byn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDerivC (Z * W - W * Z) = lieDerivC Z * lieDerivC W - lieDerivC W * lieDerivC Z
  -- The two commutators have to be assembled before `lieDeriv_sub` is allowed near them,
  -- or it splits `lieDeriv (A * C - C * A)` and the bracket identity no longer applies.
  simp only [lieDerivC]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv ((Z * W - W * Z).map Complex.re) + Complex.I • lieDeriv ((Z * W - W * Z).map Complex.im) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im))
  rw [map_re_bracket,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv
      (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
        (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)) +
    Complex.I • lieDeriv ((Z * W - W * Z).map Complex.im) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re) -
      lieDeriv (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) +
    Complex.I •
      (lieDeriv (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re) +
        lieDeriv (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) map_im_bracket,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv
      (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re -
        (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im)) +
    Complex.I •
      lieDeriv
        (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
          (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re) -
      lieDeriv (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) +
    Complex.I •
      (lieDeriv (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re) +
        lieDeriv (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) lieDeriv_sub,n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re) -
      lieDeriv (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) +
    Complex.I •
      lieDeriv
        (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re +
          (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re) -
      lieDeriv (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) +
    Complex.I •
      (lieDeriv (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re) +
        lieDeriv (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) lieDeriv_addn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re) -
      lieDeriv (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) +
    Complex.I •
      (lieDeriv (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re) +
        lieDeriv (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im))n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re) -
      lieDeriv (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) +
    Complex.I •
      (lieDeriv (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re) +
        lieDeriv (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im))]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re * W.map Complex.re - W.map Complex.re * Z.map Complex.re) -
      lieDeriv (Z.map Complex.im * W.map Complex.im - W.map Complex.im * Z.map Complex.im) +
    Complex.I •
      (lieDeriv (Z.map Complex.re * W.map Complex.im - W.map Complex.im * Z.map Complex.re) +
        lieDeriv (Z.map Complex.im * W.map Complex.re - W.map Complex.re * Z.map Complex.im)) =
  (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im)) *
      (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) -
    (lieDeriv (W.map Complex.re) + Complex.I • lieDeriv (W.map Complex.im)) *
      (lieDeriv (Z.map Complex.re) + Complex.I • lieDeriv (Z.map Complex.im))
  simp only [lieDeriv_bracket, mul_add, add_mul, smul_mul_assoc,
    mul_smul_comm, smul_smul, smul_add]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ lieDeriv (Z.map Complex.re) * lieDeriv (W.map Complex.re) - lieDeriv (W.map Complex.re) * lieDeriv (Z.map Complex.re) -
      (lieDeriv (Z.map Complex.im) * lieDeriv (W.map Complex.im) -
        lieDeriv (W.map Complex.im) * lieDeriv (Z.map Complex.im)) +
    (Complex.I •
        (lieDeriv (Z.map Complex.re) * lieDeriv (W.map Complex.im) -
          lieDeriv (W.map Complex.im) * lieDeriv (Z.map Complex.re)) +
      Complex.I •
        (lieDeriv (Z.map Complex.im) * lieDeriv (W.map Complex.re) -
          lieDeriv (W.map Complex.re) * lieDeriv (Z.map Complex.im))) =
  lieDeriv (Z.map Complex.re) * lieDeriv (W.map Complex.re) +
        Complex.I • (lieDeriv (Z.map Complex.im) * lieDeriv (W.map Complex.re)) +
      (Complex.I • (lieDeriv (Z.map Complex.re) * lieDeriv (W.map Complex.im)) +
        (Complex.I * Complex.I) • (lieDeriv (Z.map Complex.im) * lieDeriv (W.map Complex.im))) -
    (lieDeriv (W.map Complex.re) * lieDeriv (Z.map Complex.re) +
        Complex.I • (lieDeriv (W.map Complex.im) * lieDeriv (Z.map Complex.re)) +
      (Complex.I • (lieDeriv (W.map Complex.re) * lieDeriv (Z.map Complex.im)) +
        (Complex.I * Complex.I) • (lieDeriv (W.map Complex.im) * lieDeriv (Z.map Complex.im))))
  match_scalarsn:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ 1 = 1n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ -1 = -1n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ -1 = Complex.I * Complex.I * 1n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ - -1 = -(Complex.I * Complex.I * 1)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Complex.I * 1 = Complex.I * 1n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Complex.I * -1 = -(Complex.I * 1)n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Complex.I * 1 = Complex.I * 1n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ Complex.I * -1 = -(Complex.I * 1)
  all_goals ring_nfAll goals completed! 🐙
  all_goals (try simp only [Complex.I_sq]n:Type u_1inst✝¹:Fintype ninst✝:DecidableEq nZ:Matrix n n ℂW:Matrix n n ℂ⊢ 1 = - -1)
  all_goals ringAll goals completed! 🐙

end Smoothend Matrix.GeneralLinearGroup

Lie derivatives of smooth functions on GL n ℝ