[Merged by Bors] - feat(Algebra/Lie): prove derivations are inner in finite-dimensional Killing Lie algebra

[frederic-marbach]

This finishes the proof that all derivations in a finite-dimensional Lie algebra with non-degenerate Killing form are inner derivations, a project discussed in this thread with @ocfnash.

---

I am particularly open to design remarks or suggestions. More specifically, here are some points of which I doubt:

• I took the liberty of introducing local notations to ease my mind,
• I stated intermediary lemmas which might be useless outside of this file,
• I left a comment in the Killing.lean file for a hacky coercion I could not figure my way out otherwise.

[ocfnash]

@frederic-marbach Thanks for doing this. I added a commit because I realised that new lemma you proposed LieIdeal.killingCompl_eq_orthogonalBilin should be true by definition (I also renamed it to LieIdeal.toSubmodule_killingCompl).

I'm out of time for today so I'll have to finish reviewing tomorrow.

[ocfnash]

I thought about this PR quite a bit today and I have some remarks:

1. The local notation is great: IMHO we underuse this feature.
2. The lemmas about 𝕀ᗮ are not really so desirable because ultimately you prove this is ⊥ (I recognise you allude to this above)
3. Some of the results are true more generally, e.g., without assuming [LieAlgebra.IsKilling R L] so it would be nice to extract these
4. I think it's better to have lemmas which talk about (ad R L).range rather than (ad R L).idealRange unless the statement actually needs an ideal, since it's a simpler object

With all that in mind I tried to work out what was the core result and I learned (from your code!) that seems to be that if D is orthogonal to (ad R L).range then so is ad R L (D x) for any x. So I extracted this lemma (which doesn't require the assumption [LieAlgebra.IsKilling R L]) and then after adding a bit of API to LinearMap.BilinForm things seemed to work out quite nicely. I've pushed a commit (and merged master) so that the following suggestion should work:

[ocfnash]

So here's what I suggest:

variable (R L : Type*) [Field R] [LieRing L] [LieAlgebra R L] [Module.Finite R L]

/-- A local notation for the set of (Lie) derivations on `L`. -/
local notation "𝔻" => (LieDerivation R L L)

-- /-- A local notation for the ideal range of `ad`. -/
-- local notation "𝕀" => LieHom.idealRange (ad R L)

-- /-- A local notation for the Killing complement of the ideal range of `ad`. -/
-- local notation "𝕀ᗮ" => LieIdeal.killingCompl R 𝔻 𝕀

lemma killingForm_restrict_range_ad :
    (killingForm R 𝔻).restrict (ad R L).range = killingForm R (ad R L).range := by
  rw [← (ad_isIdealMorphism R L).eq, ← LieIdeal.killingForm_eq]
  rfl

variable {R L}

-- This is really the key result
lemma ad_mem_orthogonal_of_mem_orthogonal
    {D : LieDerivation R L L} (hD : D ∈ (killingForm R 𝔻).orthogonal (ad R L).range) (x : L) :
    ad R L (D x) ∈ (killingForm R 𝔻).orthogonal (ad R L).range := by
  have : (killingForm R 𝔻).orthogonal (ad R L).range = (ad R L).idealRange.killingCompl := by
    simp [← (ad_isIdealMorphism R L).eq]
  rw [this] at hD ⊢
  rw [← lie_der_ad_eq_ad_der]
  exact lie_mem_left _ _ (ad R L).idealRange.killingCompl _ _ hD

lemma add_mem_ker_killingForm_ad_range_of_mem_orthogonal
    {D : LieDerivation R L L} (hD : D ∈ (killingForm R 𝔻).orthogonal (ad R L).range) (x : L) :
    ad R L (D x) ∈ (LinearMap.ker <| killingForm R (ad R L).range).map (ad R L).range.subtype := by
  rw [← killingForm_restrict_range_ad]
  exact LinearMap.BilinForm.inf_orthogonal_self_le_ker_restrict
    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl ⟨by simp, ad_mem_orthogonal_of_mem_orthogonal hD x⟩

variable (R L)
variable [LieAlgebra.IsKilling R L]

@[simp] lemma ad_apply_eq_zero_iff (x : L) : ad R L x = 0 ↔ x = 0 := by
  refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
  rwa [← LieHom.mem_ker, ad_ker_eq_center, LieAlgebra.center_eq_bot_of_semisimple,
    LieSubmodule.mem_bot] at h

instance instIsKilling_range_ad : LieAlgebra.IsKilling R (ad R L).range :=
  (LieEquiv.ofInjective (ad R L) (injective_ad_of_center_eq_bot <| by simp)).isKilling

lemma killingForm_restrict_range_ad_nondegenerate :
    ((killingForm R 𝔻).restrict (ad R L).range).Nondegenerate :=
  killingForm_restrict_range_ad R L ▸ LieAlgebra.IsKilling.killingForm_nondegenerate R _

lemma range_ad_eq_top : (ad R L).range = ⊤ := by
  rw [← LieSubalgebra.coe_to_submodule_eq_iff]
  apply LinearMap.BilinForm.eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot
    (LieModule.traceForm_isSymm R 𝔻 𝔻).isRefl (killingForm_restrict_range_ad_nondegenerate R L)
  refine (Submodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
  simpa using add_mem_ker_killingForm_ad_range_of_mem_orthogonal hD x

lemma exists_eq_ad (D : 𝔻) : ∃ x, ad R L x = D := by
  change D ∈ (ad R L).range
  rw [range_ad_eq_top R L]
  exact Submodule.mem_top

I've been too lazy to add comments or to use the local notation though both would be good.

What do you think?

[frederic-marbach]

I applied your suggestions, with local notations and (some) comments.

I have a few questions:

• You added ad_apply_eq_zero_iff (in Semisimple.lean), which looks a lot like injective_ad_of_center_eq_bot (in AdjointAction.lean). Should we keep both?
• I had added equivRangeAdOfCenterEqBot (in AdjointAction.lean), but your solution does not use it anymore, should we keep it?
• Eventually, I had named the file Semisimple.lean, but should it be Killing.lean?

[ocfnash]

* You added `ad_apply_eq_zero_iff ` (in `Semisimple.lean`), which looks a lot like `injective_ad_of_center_eq_bot` (in `AdjointAction.lean`). Should we keep both?

Yes, we should keep both. injective_ad_of_center_eq_bot is useful as input to lemmas that demand this hypothesis and ad_apply_eq_zero_iff has several useful features:

• It is a useful simp lemma
• It is useful for rewriting
• It picks up the trivial center condition via typeclasses

It could be generalised if we had a typeclass LieAlgebra.HasTrivialCenter (or something) but I'm not sure if we need this and anyway, that's out of scope for this PR.

* I had added `equivRangeAdOfCenterEqBot` (in `AdjointAction.lean`), but your solution does not use it anymore, should we keep it?

Good point, I think we should drop this now.

* Eventually, I had named the file `Semisimple.lean`, but should it be `Killing.lean`?

Yes, probably Killing.lean is a better name

[ocfnash]

Thanks for doing this, I learned the proof from your work!

I think this is ready to be merged but I'm going to ask for another reviewer to take a look because the PR now contains a mixture of your work and mine.

[frederic-marbach]

Thanks. I fixed the typo, renamed the file, and removed my useless lemma.

[jcommelin]

Thanks. Very nice work! Two mini comments

bors d+

[mathlib-bors]

✌️ frederic-marbach can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[frederic-marbach]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style