Invariant Lie subalgebras under automorphisms

An automorphism σ of a Lie algebra L normalises a Lie subalgebra H when H.map σ = H. This file records that the inverse normalises H too, and identifies the inverse of Mathlib's LieEquiv.ofSubalgebras restriction with the corresponding restriction of the inverse automorphism.

Nothing here involves weights, nilpotence, or any hypothesis on the base ring beyond commutativity. What the automorphism does to the root spaces of H is in TauCeti/Algebra/Lie/Weights/Automorphism.lean.

Main results

• LieSubalgebra.map_eq_self_of_forall_mem_apply_eq_neg: an automorphism acting by -1 on a subalgebra normalises it.
• LieSubalgebra.map_symm_eq_self_of_map_eq_self: the inverse of a normalising automorphism normalises the subalgebra as well.
• TauCeti.ofSubalgebras_symm: restricting the inverse gives the inverse of Mathlib's restriction.

theorem LieSubalgebra.map_eq_self_of_forall_mem_apply_eq_neg {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (e : L ≃ₗ⁅R⁆ L) (hneg : ∀ y ∈ H, e y = -y) : map e.toLieHom H = H

An automorphism acting by -1 on a subalgebra normalises it, since a subalgebra is closed under negation.

theorem LieSubalgebra.map_symm_eq_self_of_map_eq_self {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (e : L ≃ₗ⁅R⁆ L) (he : map e.toLieHom H = H) : map e.symm.toLieHom H = H

The inverse of a normalising automorphism normalises H as well.

theorem TauCeti.ofSubalgebras_symm {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (e : L ≃ₗ⁅R⁆ L) (he : LieSubalgebra.map e.toLieHom H = H) : (LieEquiv.ofSubalgebras H H e he).symm = LieEquiv.ofSubalgebras H H e.symm ⋯

The inverse of the restriction of a normalising automorphism is the restriction of the inverse automorphism.