splittingOfFinsuppSurjective_splits

English

The composite of f with its splitting equals the identity on α →₀ R.

Русский

Составное отображение f и его разложение равно тождественному на α →₀ R.

LaTeX

$$$f \circ (splittingOfFinsuppSurjective\;f\;s) = id$$$

Lean4

theorem splittingOfFinsuppSurjective_splits (f : M →ₗ[R] α →₀ R) (s : Surjective f) :
    f.comp (splittingOfFinsuppSurjective f s) = LinearMap.id :=
  by
  ext x
  dsimp [splittingOfFinsuppSurjective]
  congr
  rw [sum_single_index, one_smul]
  · exact (s (Finsupp.single x 1)).choose_spec
  · rw [zero_smul]

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