English
Let M be semisimple. For any surjective f: M → N and any g: P → N, there exists h: P → M with f ∘ h = g.
Русский
Пусть M — полупростый модуль. Любое сюръективное отображение f: M → N и любое g: P → N допускают существование h: P → M с f ∘ h = g.
LaTeX
$$∃ h : P →ₗ[R] M, f ∘ₗ h = g$$
Lean4
theorem lifting_property {P} [AddCommGroup P] [Module R P] (f : M →ₗ[R] N) (hf : Function.Surjective f)
(g : P →ₗ[R] N) : ∃ h : P →ₗ[R] M, f ∘ₗ h = g :=
by
have ⟨m, compl⟩ := exists_isCompl (LinearMap.ker f)
let e := (Submodule.quotientEquivOfIsCompl _ m compl).symm ≪≫ₗ f.quotKerEquivOfSurjective hf
refine ⟨Submodule.subtype _ ∘ₗ e.symm.toLinearMap ∘ₗ g, LinearMap.ext fun x ↦ ?_⟩
obtain ⟨z, eq⟩ := e.surjective (g x)
simp only [LinearMap.comp_apply, ← eq, LinearEquiv.coe_coe, e.symm_apply_apply]
simp [e]
