Add a Group instance for LieEquiv (automorphisms of a Lie algebra / Lie module)

Summary

L ≃ₗ⁅R⁆ L is the automorphism group of a Lie algebra, and M ≃ₗ⁅R,L⁆ M that of a Lie module, but mathlib provides no Group instance (and no Mul/Inv) for either. All the ingredients are already present — refl, symm, trans, symm_apply_apply, self_trans_symm, symm_trans_self, ext, and even One/Inhabited instances — so this looks like an oversight rather than a design decision.

Why it matters

Without the instance, L ≃ₗ⁅R⁆ L cannot be used with any Group-generic API: Subgroup, MulEquiv, MulAut, Submonoid.closure, IsCyclic, the Fintype (MulAut _) lemmas, map/comap of subgroups, etc. In particular a statement of the form "conjugation induces a group isomorphism Aut_fin(P) ≃* Aut_{k-Lie}(W)" cannot be written with ≃* unless the codomain carries a group structure.

I ran into this while formalizing a paper whose main theorem is exactly such a group isomorphism, and had to introduce the instance locally in my project. The following version compiles (Lean 4.34.0, mathlib 5ed2965256430c3649e86755f9576b54eca72435):

instance : Group (W k ≃ₗ⁅k⁆ W k) where
  mul e₁ e₂ := e₂.trans e₁
  one := 1
  inv e := e.symm
  mul_assoc e₁ e₂ e₃ := LieEquiv.ext fun _ => rfl
  one_mul e := LieEquiv.ext fun _ => rfl
  mul_one e := LieEquiv.ext fun _ => rfl
  inv_mul_cancel e := LieEquiv.self_trans_symm e

Note that I had to make it a global instance on my own Lie algebra, because a letI-style local instance cannot be used to state a bundled ≃* whose codomain is the automorphism group — that is precisely the kind of thing that belongs in mathlib.

Precedents in mathlib

• Mathlib/Algebra/Module/Equiv/Basic.lean: instance automorphismGroup : Group (M ≃ₗ[R] M)
• Mathlib/Algebra/Algebra/Equiv.lean: instance aut : Group (A₁ ≃ₐ[R] A₁), with mul ϕ ψ := ψ.trans ϕ, @[simp] theorem mul_apply : (e₁ * e₂) x = e₁ (e₂ x), lemma aut_inv : ϕ⁻¹ = ϕ.symm, and AlgEquiv.autCongr.

Proposal

In Mathlib/Algebra/Lie/Basic.lean, inside namespace LieEquiv right after the existing One instance, mirroring AlgEquiv.aut:

@[simps -isSimp one mul]
instance aut : Group (L₁ ≃ₗ⁅R⁆ L₁) where
  mul ϕ ψ := ψ.trans ϕ
  mul_assoc _ _ _ := rfl        -- (rfl as in AlgEquiv.aut, if it goes through here)
  one := refl
  one_mul _ := ext fun _ => rfl
  mul_one _ := ext fun _ => rfl
  inv := symm
  inv_mul_cancel ϕ := ext <| symm_apply_apply ϕ

plus the usual @[simp] lemmas (one_apply, mul_apply, aut_inv, coe_inv), and the same for LieModuleEquiv (M ≃ₗ⁅R,L⁆ M). LieEquiv.autCongr / LieModuleEquiv.autCongr would also be natural.

Every lemma this needs already exists: LieEquiv.ext, LieEquiv.symm_apply_apply, LieEquiv.self_trans_symm; LieModuleEquiv.ext, LieModuleEquiv.symm_apply_apply, LieModuleEquiv.self_trans_symm.

Question for the maintainers

• Global instance (as for LinearEquiv / AlgEquiv) or scoped?
• Which name do you prefer: aut (matching AlgEquiv.aut) or automorphismGroup (matching LinearEquiv)?

(Checked against current master: Mathlib/Algebra/Lie/Basic.lean has instance : One (L₁ ≃ₗ⁅R⁆ L₁) and instance : One (M ≃ₗ⁅R,L⁆ M), but no Group/Mul/Inv for either.)

I am happy to open the PR if you tell me which of the two conventions you want — flagging this as an issue first since it is an API-design choice.

Start in Mathlib/Algebra/Lie/Basic.lean, inside the LieEquiv namespace, and compare the existing One instances with the LinearEquiv and AlgEquiv precedents named in the issue. Confirm the preferred instance scope and naming with maintainers, then ensure both LieEquiv and LieModuleEquiv automorphism groups have the requested group operations, simp lemmas, and autCongr APIs.