splittingOfFunOnFintypeSurjective_splits

English

For a finite α, the composition of f with its splitting is the identity on α → R.

Русский

Для конечного α композиция f с его расщеплением равна тождественному отображению на α → R.

LaTeX

$$$f \circ (f.splittingOfFunOnFintypeSurjective) = \mathrm{Id}$$$

Lean4

theorem splittingOfFunOnFintypeSurjective_splits [Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) :
    f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id := by
  classical
  ext x y
  dsimp [splittingOfFunOnFintypeSurjective]
  rw [linearEquivFunOnFinite_symm_single, Finsupp.sum_single_index, one_smul, (s (Finsupp.single x 1)).choose_spec,
    Finsupp.single_eq_pi_single]
  rw [zero_smul]

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