splittingOfFunOnFintypeSurjective

English

If f: M → α → R is a surjective linear map and α is finite, there exists a linear map splitting f to recover α → R from M.

Русский

Если f: M → α → R линейно сюръективно и α конечно, существует расщепление f, позволяющее восстановить α → R из M.

LaTeX

$$$\text{splittingOfFunOnFintypeSurjective} : (M \to α → R) \to M$ является расщеплением для сюръективного f, когда α конечен$$

Lean4

/-- A surjective linear map to functions on a finite type has a splitting. -/
def splittingOfFunOnFintypeSurjective [Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) : (α → R) →ₗ[R] M :=
  (Finsupp.lift _ _ _ fun x : α => (s (Finsupp.single x 1)).choose).comp (linearEquivFunOnFinite R R α).symm.toLinearMap

Похожие утверждения