English
The functor X ↦ FreeLieAlgebra R X is left adjoint to the forgetful functor from Lie algebras to types: there is an equivalence between type maps X → L and Lie algebra homomorphisms FreeLieAlgebra R X → L.
Русский
Функтор X ↦ FreeLieAlgebra_R X является левым смежным к функтору забывания: существует эквивалентность между отображениями X → L и гомоморфизмами Lie-алгебр FreeLieAlgebra_R X → L.
LaTeX
$$$\bigl(X \to L\bigr) \simeq_{R} \bigl(\mathrm{FreeLieAlgebra}_R X \to_\ell L\bigr).$$$
Lean4
/-- The functor `X ↦ FreeLieAlgebra R X` from the category of types to the category of Lie
algebras over `R` is adjoint to the forgetful functor in the other direction. -/
def lift : (X → L) ≃ (FreeLieAlgebra R X →ₗ⁅R⁆ L)
where
toFun
f :=
{ toFun := fun c => Quot.liftOn c (liftAux R f) (liftAux_spec R f)
map_add' := by rintro ⟨a⟩ ⟨b⟩; rw [← liftAux_map_add]; rfl
map_smul' := by rintro t ⟨a⟩; rw [← liftAux_map_smul]; rfl
map_lie' := by rintro ⟨a⟩ ⟨b⟩; rw [← liftAux_map_mul]; rfl }
invFun F := F ∘ of R
left_inv
f := by
ext x
simp only [liftAux, of, LieHom.coe_mk, Function.comp_apply, lib.lift_of_apply]
right_inv
F := by
ext ⟨a⟩
let F' := F.toNonUnitalAlgHom.comp (mk R)
exact NonUnitalAlgHom.congr_fun (lib.lift_comp_of R F') a
