LeanPool.VirasoroProject.ToMathlib.Algebra.Lie.Basic

def LieAlgebra.bracketHom (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] : 𝓰 →ₗ[𝕜] 𝓰 →ₗ[𝕜] 𝓰

⁅·,·⁆ as a bilinear map.

Equations

• LieAlgebra.bracketHom 𝕜 𝓰 = { toFun := fun (X : 𝓰) => { toFun := fun (Y : 𝓰) => ⁅X, Y⁆, map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LieAlgebra.bracketHom_apply (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 : Type u) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {X Y : 𝓰} : ((bracketHom 𝕜 𝓰) X) Y = ⁅X, Y⁆

def LieEquiv.mkOfCompEqId {R : Type u_2} {L : Type u_3} {L' : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing L'] [LieAlgebra R L'] {f : L →ₗ⁅R⁆ L'} {g : L' →ₗ⁅R⁆ L} (leftInv : g.comp f = LieHom.id) (rightInv : f.comp g = LieHom.id) : L ≃ₗ⁅R⁆ L'

Construct an isomorphism of Lie algebras from a pair of inverse Lie algebra homomorphisms.

Equations

• LieEquiv.mkOfCompEqId leftInv rightInv = { toFun := ⇑f, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯ }