feat(algebra/lie_algebra): conjugation transformation for Lie algebra…

…s of skew-adjoint endomorphims, matrices (#3229)

The two main results are the lemmas:
 * skew_adjoint_lie_subalgebra_equiv
 * skew_adjoint_matrices_lie_subalgebra_equiv

The latter is expected to be useful when defining the classical Lie algebras
of type B and D.

src/algebra/lie_algebra.lean

@@ -257,28 +257,59 @@ variables {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁}
 variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_ring L₃]
 variables [lie_algebra R L₁] [lie_algebra R L₂] [lie_algebra R L₃]
 
+instance has_coe_to_lie_hom : has_coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂) := ⟨to_morphism⟩
+instance has_coe_to_linear_equiv : has_coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ ≃ₗ[R] L₂) := ⟨to_linear_equiv⟩
+
+/-- see Note [function coercion] -/
+instance : has_coe_to_fun (L₁ ≃ₗ⁅R⁆ L₂) := ⟨_, to_fun⟩
+
+@[simp, norm_cast] lemma coe_to_lie_equiv (e : L₁ ≃ₗ⁅R⁆ L₂) : ((e : L₁ →ₗ⁅R⁆ L₂) : L₁ → L₂) = e :=
+  rfl
+
+@[simp, norm_cast] lemma coe_to_linear_equiv (e : L₁ ≃ₗ⁅R⁆ L₂) : ((e : L₁ ≃ₗ[R] L₂) : L₁ → L₂) = e :=
+  rfl
+
 instance : has_one (L₁ ≃ₗ⁅R⁆ L₁) :=
 ⟨{ map_lie := λ x y, by { change ((1 : L₁→ₗ[R] L₁) ⁅x, y⁆) = ⁅(1 : L₁→ₗ[R] L₁) x, (1 : L₁→ₗ[R] L₁) y⁆, simp, },
   ..(1 : L₁ ≃ₗ[R] L₁)}⟩
 
+@[simp] lemma one_apply (x : L₁) : (1 : (L₁ ≃ₗ⁅R⁆ L₁)) x = x := rfl
+
 instance : inhabited (L₁ ≃ₗ⁅R⁆ L₁) := ⟨1⟩
 
 /-- Lie algebra equivalences are reflexive. -/
 @[refl]
 def refl : L₁ ≃ₗ⁅R⁆ L₁ := 1
 
+@[simp] lemma refl_apply (x : L₁) : (refl : L₁ ≃ₗ⁅R⁆ L₁) x = x := rfl
+
 /-- Lie algebra equivalences are symmetric. -/
 @[symm]
 def symm (e : L₁ ≃ₗ⁅R⁆ L₂) : L₂ ≃ₗ⁅R⁆ L₁ :=
 { ..morphism.inverse e.to_morphism e.inv_fun e.left_inv e.right_inv,
   ..e.to_linear_equiv.symm }
 
+@[simp] lemma symm_symm (e : L₁ ≃ₗ⁅R⁆ L₂) : e.symm.symm = e :=
+by { cases e, refl, }
+
+@[simp] lemma apply_symm_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e (e.symm x) = x :=
+  e.to_linear_equiv.apply_symm_apply
+
+@[simp] lemma symm_apply_apply (e : L₁ ≃ₗ⁅R⁆ L₂) : ∀ x, e.symm (e x) = x :=
+  e.to_linear_equiv.symm_apply_apply
+
 /-- Lie algebra equivalences are transitive. -/
 @[trans]
 def trans (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) : L₁ ≃ₗ⁅R⁆ L₃ :=
 { ..morphism.comp e₂.to_morphism e₁.to_morphism,
   ..linear_equiv.trans e₁.to_linear_equiv e₂.to_linear_equiv }
 
+@[simp] lemma trans_apply (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₁) :
+  (e₁.trans e₂) x = e₂ (e₁ x) := rfl
+
+@[simp] lemma symm_trans_apply (e₁ : L₁ ≃ₗ⁅R⁆ L₂) (e₂ : L₂ ≃ₗ⁅R⁆ L₃) (x : L₃) :
+  (e₁.trans e₂).symm x = e₁.symm (e₂.symm x) := rfl
+
 end equiv
 
 namespace direct_sum
@@ -392,6 +423,7 @@ instance : has_zero (lie_subalgebra R L) :=
 
 instance : inhabited (lie_subalgebra R L) := ⟨0⟩
 instance : has_coe (lie_subalgebra R L) (set L) := ⟨lie_subalgebra.carrier⟩
+instance : has_mem L (lie_subalgebra R L) := ⟨λ x L', x ∈ (L' : set L)⟩
 
 instance lie_subalgebra_coe_submodule : has_coe (lie_subalgebra R L) (submodule R L) :=
 ⟨lie_subalgebra.to_submodule⟩
@@ -409,39 +441,126 @@ instance lie_subalgebra_lie_algebra (L' : lie_subalgebra R L) :
     @lie_algebra R L' _ (lie_subalgebra_lie_ring _ _ _) :=
 { lie_smul := by { intros, apply set_coe.ext, apply lie_smul } }
 
+@[simp] lemma lie_subalgebra.mem_coe {L' : lie_subalgebra R L} {x : L} :
+  x ∈ (L' : set L) ↔ x ∈ L' := iff.rfl
+
+@[simp] lemma lie_subalgebra.mem_coe' {L' : lie_subalgebra R L} {x : L} :
+  x ∈ (L' : submodule R L) ↔ x ∈ L' := iff.rfl
+
+@[simp, norm_cast] lemma lie_subalgebra.coe_bracket (L' : lie_subalgebra R L) (x y : L') :
+  (↑⁅x, y⁆ : L) = ⁅↑x, ↑y⁆ := rfl
+
+@[ext] lemma lie_subalgebra.ext (L₁' L₂' : lie_subalgebra R L) (h : ∀ x, x ∈ L₁' ↔ x ∈ L₂') :
+  L₁' = L₂' :=
+by { cases L₁', cases L₂', simp only [], ext x, exact h x, }
+
+lemma lie_subalgebra.ext_iff (L₁' L₂' : lie_subalgebra R L) : L₁' = L₂' ↔ ∀ x, x ∈ L₁' ↔ x ∈ L₂' :=
+⟨λ h x, by rw h, lie_subalgebra.ext R L L₁' L₂'⟩
+
 local attribute [instance] lie_ring.of_associative_ring
 local attribute [instance] lie_algebra.of_associative_algebra
 
+/-- A subalgebra of an associative algebra is a Lie subalgebra of the associated Lie algebra. -/
+def lie_subalgebra_of_subalgebra (A : Type v) [ring A] [algebra R A]
+  (A' : subalgebra R A) : lie_subalgebra R A :=
+{ lie_mem := λ x y hx hy, by {
+    change ⁅x, y⁆ ∈ A', change x ∈ A' at hx, change y ∈ A' at hy,
+    rw lie_ring.of_associative_ring_bracket,
+    have hxy := subalgebra.mul_mem A' x y hx hy,
+    have hyx := subalgebra.mul_mem A' y x hy hx,
+    exact submodule.sub_mem A'.to_submodule hxy hyx, },
+  ..A'.to_submodule }
+
+variables {R L} {L₂ : Type w} [lie_ring L₂] [lie_algebra R L₂]
+
 /-- The embedding of a Lie subalgebra into the ambient space as a Lie morphism. -/
-def lie_subalgebra.incl
-  {R : Type u} {L : Type v} [comm_ring R] [lie_ring L] [lie_algebra R L]
-  (L' : lie_subalgebra R L) : L' →ₗ⁅R⁆ L :=
+def lie_subalgebra.incl (L' : lie_subalgebra R L) : L' →ₗ⁅R⁆ L :=
 { map_lie := λ x y, by { rw [linear_map.to_fun_eq_coe, submodule.subtype_apply], refl, },
   ..L'.to_submodule.subtype }
 
 /-- The range of a morphism of Lie algebras is a Lie subalgebra. -/
-def lie_algebra.morphism.range {R : Type u} {L₁ : Type v} {L₂ : Type w}
-  [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂]
-  (f : L₁ →ₗ⁅R⁆ L₂) : lie_subalgebra R L₂ :=
+def lie_algebra.morphism.range (f : L →ₗ⁅R⁆ L₂) : lie_subalgebra R L₂ :=
 { lie_mem := λ x y,
     show x ∈ f.to_linear_map.range → y ∈ f.to_linear_map.range → ⁅x, y⁆ ∈ f.to_linear_map.range,
     by { repeat { rw linear_map.mem_range }, rintros ⟨x', hx⟩ ⟨y', hy⟩, refine ⟨⁅x', y'⁆, _⟩,
          rw [←hx, ←hy], change f ⁅x', y'⁆ = ⁅f x', f y'⁆, rw lie_algebra.map_lie, },
   ..f.to_linear_map.range }
 
-/-- A subalgebra of an associative algebra is a Lie subalgebra of the associated Lie algebra. -/
-def lie_subalgebra_of_subalgebra (A : Type v) [ring A] [algebra R A]
-  (A' : subalgebra R A) : lie_subalgebra R A :=
+@[simp] lemma lie_algebra.morphism.range_bracket (f : L →ₗ⁅R⁆ L₂) (x y : f.range) :
+  (↑⁅x, y⁆ : L₂) = ⁅↑x, ↑y⁆ := rfl
+
+/-- The image of a Lie subalgebra under a Lie algebra morphism is a Lie subalgebra of the
+codomain. -/
+def lie_subalgebra.map (f : L →ₗ⁅R⁆ L₂) (L' : lie_subalgebra R L) : lie_subalgebra R L₂ :=
 { lie_mem := λ x y hx hy, by {
-    change ⁅x, y⁆ ∈ A', change x ∈ A' at hx, change y ∈ A' at hy,
-    rw lie_ring.of_associative_ring_bracket,
-    have hxy := subalgebra.mul_mem A' x y hx hy,
-    have hyx := subalgebra.mul_mem A' y x hy hx,
-    exact submodule.sub_mem A'.to_submodule hxy hyx, },
-  ..A'.to_submodule }
+    erw submodule.mem_map at hx, rcases hx with ⟨x', hx', hx⟩, rw ←hx,
+    erw submodule.mem_map at hy, rcases hy with ⟨y', hy', hy⟩, rw ←hy,
+    erw submodule.mem_map,
+    exact ⟨⁅x', y'⁆, L'.lie_mem hx' hy', lie_algebra.map_lie f x' y'⟩, },
+..((L' : submodule R L).map (f : L →ₗ[R] L₂))}
+
+@[simp] lemma lie_subalgebra.mem_map_submodule (e : L ≃ₗ⁅R⁆ L₂) (L' : lie_subalgebra R L) (x : L₂) :
+  x ∈ L'.map (e : L →ₗ⁅R⁆ L₂) ↔ x ∈ (L' : submodule R L).map (e : L →ₗ[R] L₂) :=
+by refl
 
 end lie_subalgebra
 
+namespace lie_algebra
+
+variables {R : Type u} {L₁ : Type v} {L₂ : Type w}
+variables [comm_ring R] [lie_ring L₁] [lie_ring L₂] [lie_algebra R L₁] [lie_algebra R L₂]
+
+namespace equiv
+
+/-- An injective Lie algebra morphism is an equivalence onto its range. -/
+noncomputable def of_injective (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) :
+  L₁ ≃ₗ⁅R⁆ f.range :=
+have h' : (f : L₁ →ₗ[R] L₂).ker = ⊥ := linear_map.ker_eq_bot_of_injective h,
+{ map_lie := λ x y, by { apply set_coe.ext,
+    simp only [linear_equiv.of_injective_apply, lie_algebra.morphism.range_bracket],
+    apply f.map_lie, },
+..(linear_equiv.of_injective ↑f h')}
+
+@[simp] lemma of_injective_apply (f : L₁ →ₗ⁅R⁆ L₂) (h : function.injective f) (x : L₁) :
+  ↑(of_injective f h x) = f x := rfl
+
+variables (L₁' L₁'' : lie_subalgebra R L₁) (L₂' : lie_subalgebra R L₂)
+
+/-- Lie subalgebras that are equal as sets are equivalent as Lie algebras. -/
+def of_eq (h : (L₁' : set L₁) = L₁'') : L₁' ≃ₗ⁅R⁆ L₁'' :=
+{ map_lie := λ x y, by { apply set_coe.ext, simp, },
+  ..(linear_equiv.of_eq ↑L₁' ↑L₁''
+      (by {ext x, change x ∈ (L₁' : set L₁) ↔ x ∈ (L₁'' : set L₁), rw h, } )) }
+
+@[simp] lemma of_eq_apply (L L' : lie_subalgebra R L₁) (h : (L : set L₁) = L') (x : L) :
+  (↑(of_eq L L' h x) : L₁) = x := rfl
+
+variables (e : L₁ ≃ₗ⁅R⁆ L₂)
+
+/-- An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its
+image. -/
+def of_subalgebra : L₁'' ≃ₗ⁅R⁆ (L₁''.map e : lie_subalgebra R L₂) :=
+{ map_lie := λ x y, by { apply set_coe.ext, exact lie_algebra.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y, }
+  ..(linear_equiv.of_submodule (e : L₁ ≃ₗ[R] L₂) ↑L₁'') }
+
+@[simp] lemma of_subalgebra_apply (x : L₁'') : ↑(e.of_subalgebra _  x) = e x := rfl
+
+/-- An equivalence of Lie algebras restricts to an equivalence from any Lie subalgebra onto its
+image. -/
+def of_subalgebras (h : L₁'.map ↑e = L₂') : L₁' ≃ₗ⁅R⁆ L₂' :=
+{ map_lie := λ x y, by { apply set_coe.ext, exact lie_algebra.map_lie (↑e : L₁ →ₗ⁅R⁆ L₂) ↑x ↑y, },
+  ..(linear_equiv.of_submodules (e : L₁ ≃ₗ[R] L₂) ↑L₁' ↑L₂' (by { rw ←h, refl, })) }
+
+@[simp] lemma of_subalgebras_apply (h : L₁'.map ↑e = L₂') (x : L₁') :
+  ↑(e.of_subalgebras _ _ h x) = e x := rfl
+
+@[simp] lemma of_subalgebras_symm_apply (h : L₁'.map ↑e = L₂') (x : L₂') :
+  ↑((e.of_subalgebras _ _ h).symm x) = e.symm x := rfl
+
+end equiv
+
+end lie_algebra
+
 section lie_module
 
 variables (R : Type u) (L : Type v) [comm_ring R] [lie_ring L] [lie_algebra R L]
@@ -625,6 +744,24 @@ end quotient
 
 end lie_submodule
 
+namespace linear_equiv
+
+variables {R : Type u} {M₁ : Type v} {M₂ : Type w}
+variables [comm_ring R] [add_comm_group M₁] [module R M₁] [add_comm_group M₂] [module R M₂]
+variables (e : M₁ ≃ₗ[R] M₂)
+
+/-- A linear equivalence of two modules induces a Lie algebra equivalence of their endomorphisms. -/
+def lie_conj : module.End R M₁ ≃ₗ⁅R⁆ module.End R M₂ :=
+{ map_lie := λ f g, show e.conj ⁅f, g⁆ =  ⁅e.conj f, e.conj g⁆,
+             by simp only [lie_algebra.endo_algebra_bracket, e.conj_comp, linear_equiv.map_sub],
+  ..e.conj }
+
+@[simp] lemma lie_conj_apply (f : module.End R M₁) : e.lie_conj f = e.conj f := rfl
+
+@[simp] lemma lie_conj_symm : e.lie_conj.symm = e.symm.lie_conj := rfl
+
+end linear_equiv
+
 section matrices
 open_locale matrix
 
@@ -657,18 +794,34 @@ def lie_equiv_matrix' : module.End R (n → R) ≃ₗ⁅R⁆ matrix n n R :=
   end,
   ..linear_equiv_matrix' }
 
-end matrices
+@[simp] lemma lie_equiv_matrix'_apply (f : module.End R (n → R)) :
+  lie_equiv_matrix' f = f.to_matrix := rfl
 
-namespace bilin_form
+@[simp] lemma lie_equiv_matrix'_symm_apply (A : matrix n n R) :
+  (@lie_equiv_matrix' R _ n _ _).symm A = A.to_lin := rfl
 
-variables {R : Type u} [comm_ring R]
+/-- An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself. -/
+noncomputable def matrix.lie_conj (P : matrix n n R) (h : is_unit P) :
+  matrix n n R ≃ₗ⁅R⁆ matrix n n R :=
+((@lie_equiv_matrix' R _ n _ _).symm.trans (P.to_linear_equiv h).lie_conj).trans lie_equiv_matrix'
+
+@[simp] lemma matrix.lie_conj_apply (P A : matrix n n R) (h : is_unit P) :
+  P.lie_conj h A = P ⬝ A ⬝ P⁻¹ :=
+by simp [linear_equiv.conj_apply, matrix.lie_conj, matrix.comp_to_matrix_mul, to_lin_to_matrix]
+
+@[simp] lemma matrix.lie_conj_symm_apply (P A : matrix n n R) (h : is_unit P) :
+  (P.lie_conj h).symm A = P⁻¹ ⬝ A ⬝ P :=
+by simp [linear_equiv.symm_conj_apply, matrix.lie_conj, matrix.comp_to_matrix_mul, to_lin_to_matrix]
+
+end matrices
 
 section skew_adjoint_endomorphisms
+open bilin_form
 
-variables {M : Type v} [add_comm_group M] [module R M]
+variables {R : Type u} {M : Type v} [comm_ring R] [add_comm_group M] [module R M]
 variables (B : bilin_form R M)
 
-lemma is_skew_adjoint_bracket (f g : module.End R M)
+lemma bilin_form.is_skew_adjoint_bracket (f g : module.End R M)
   (hf : f ∈ B.skew_adjoint_submodule) (hg : g ∈ B.skew_adjoint_submodule) :
   ⁅f, g⁆ ∈ B.skew_adjoint_submodule :=
 begin
@@ -684,28 +837,76 @@ Lie subalgebra of the Lie algebra of endomorphisms. -/
 def skew_adjoint_lie_subalgebra : lie_subalgebra R (module.End R M) :=
 { lie_mem := B.is_skew_adjoint_bracket, ..B.skew_adjoint_submodule }
 
+variables {N : Type w} [add_comm_group N] [module R N] (e : N ≃ₗ[R] M)
+
+/-- An equivalence of modules with bilinear forms gives equivalence of Lie algebras of skew-adjoint
+endomorphisms. -/
+def skew_adjoint_lie_subalgebra_equiv :
+  skew_adjoint_lie_subalgebra (B.comp (↑e : N →ₗ[R] M) ↑e) ≃ₗ⁅R⁆ skew_adjoint_lie_subalgebra B :=
+begin
+  apply lie_algebra.equiv.of_subalgebras _ _ e.lie_conj,
+  ext f,
+  simp only [lie_subalgebra.mem_coe, submodule.mem_map_equiv, lie_subalgebra.mem_map_submodule,
+    coe_coe],
+  exact (bilin_form.is_pair_self_adjoint_equiv (-B) B e f).symm,
+end
+
+@[simp] lemma skew_adjoint_lie_subalgebra_equiv_apply
+  (f : skew_adjoint_lie_subalgebra (B.comp ↑e ↑e)) :
+  ↑(skew_adjoint_lie_subalgebra_equiv B e f) = e.lie_conj f :=
+by simp [skew_adjoint_lie_subalgebra_equiv]
+
+@[simp] lemma skew_adjoint_lie_subalgebra_equiv_symm_apply (f : skew_adjoint_lie_subalgebra B) :
+  ↑((skew_adjoint_lie_subalgebra_equiv B e).symm f) = e.symm.lie_conj f :=
+by simp [skew_adjoint_lie_subalgebra_equiv]
+
 end skew_adjoint_endomorphisms
 
 section skew_adjoint_matrices
+open_locale matrix
 
-variables {n : Type w} [fintype n] [decidable_eq n]
+variables {R : Type u} {n : Type w} [comm_ring R] [fintype n] [decidable_eq n]
 variables (J : matrix n n R)
 
 local attribute [instance] matrix.lie_ring
 local attribute [instance] matrix.lie_algebra
 
-/-- Given a square matrix `J` defining a bilinear form on the free module, there is a natural
-embedding from the corresponding Lie subalgebra of skew-adjoint endomorphisms into the Lie algebra
-of matrices. -/
-def skew_adjoint_matrices_lie_embedding :
-  J.to_bilin_form.skew_adjoint_lie_subalgebra →ₗ⁅R⁆ matrix n n R :=
-lie_algebra.morphism.comp (lie_algebra.equiv.to_morphism lie_equiv_matrix')
-  (skew_adjoint_lie_subalgebra J.to_bilin_form).incl
+lemma matrix.lie_transpose (A B : matrix n n R) : ⁅A, B⁆ᵀ = ⁅Bᵀ, Aᵀ⁆ :=
+show (A * B - B * A)ᵀ = (Bᵀ * Aᵀ - Aᵀ * Bᵀ), by simp
+
+lemma matrix.is_skew_adjoint_bracket (A B : matrix n n R)
+  (hA : A ∈ skew_adjoint_matrices_submodule J) (hB : B ∈ skew_adjoint_matrices_submodule J) :
+  ⁅A, B⁆ ∈ skew_adjoint_matrices_submodule J :=
+begin
+  simp only [mem_skew_adjoint_matrices_submodule] at *,
+  change ⁅A, B⁆ᵀ ⬝ J = J ⬝ -⁅A, B⁆, change Aᵀ ⬝ J = J ⬝ -A at hA, change Bᵀ ⬝ J = J ⬝ -B at hB,
+  simp only [←matrix.mul_eq_mul] at *,
+  rw [matrix.lie_transpose, lie_ring.of_associative_ring_bracket, lie_ring.of_associative_ring_bracket,
+    sub_mul, mul_assoc, mul_assoc, hA, hB, ←mul_assoc, ←mul_assoc, hA, hB],
+  noncomm_ring,
+end
 
 /-- The Lie subalgebra of skew-adjoint square matrices corresponding to a square matrix `J`. -/
 def skew_adjoint_matrices_lie_subalgebra : lie_subalgebra R (matrix n n R) :=
-(skew_adjoint_matrices_lie_embedding J).range
+{ lie_mem := J.is_skew_adjoint_bracket, ..(skew_adjoint_matrices_submodule J) }
 
-end skew_adjoint_matrices
+/-- An invertible matrix `P` gives a Lie algebra equivalence between those endomorphisms that are
+skew-adjoint with respect to a square matrix `J` and those with respect to `PᵀJP`. -/
+noncomputable def skew_adjoint_matrices_lie_subalgebra_equiv (P : matrix n n R) (h : is_unit P) :
+  skew_adjoint_matrices_lie_subalgebra J ≃ₗ⁅R⁆ skew_adjoint_matrices_lie_subalgebra (Pᵀ ⬝ J ⬝ P) :=
+lie_algebra.equiv.of_subalgebras _ _ (P.lie_conj h).symm
+begin
+  ext A,
+  suffices : P.lie_conj h A ∈ skew_adjoint_matrices_submodule J ↔
+    A ∈ skew_adjoint_matrices_submodule (Pᵀ ⬝ J ⬝ P),
+  { simp only [lie_subalgebra.mem_coe, submodule.mem_map_equiv, lie_subalgebra.mem_map_submodule,
+      coe_coe], exact this, },
+  simp [matrix.is_skew_adjoint, J.is_adjoint_pair_equiv _ _ P h],
+end
 
-end bilin_form
+lemma skew_adjoint_matrices_lie_subalgebra_equiv_apply
+  (P : matrix n n R) (h : is_unit P) (A : skew_adjoint_matrices_lie_subalgebra J) :
+  ↑(skew_adjoint_matrices_lie_subalgebra_equiv J P h A) = P⁻¹ ⬝ ↑A ⬝ P :=
+by simp [skew_adjoint_matrices_lie_subalgebra_equiv]
+
+end skew_adjoint_matrices

src/data/matrix/basic.lean

@@ -488,6 +488,10 @@ end
   (M + N)ᵀ = Mᵀ + Nᵀ  :=
 by { ext i j, simp }
 
+@[simp] lemma transpose_sub [add_comm_group α] (M : matrix m n α) (N : matrix m n α) :
+  (M - N)ᵀ = Mᵀ - Nᵀ  :=
+by { ext i j, simp }
+
 @[simp] lemma transpose_mul [comm_ring α] (M : matrix m n α) (N : matrix n l α) :
   (M ⬝ N)ᵀ = Nᵀ ⬝ Mᵀ  :=
 begin