Mathlib.LinearAlgebra.Finsupp.Pi

Finsupp.LinearEquiv.finsuppUnique definition

: (α →₀ M) ≃ₗ[R] M

Full source

/-- If `α` has a unique term, then the type of finitely supported functions `α →₀ M` is
`R`-linearly equivalent to `M`. -/
noncomputable def LinearEquiv.finsuppUnique : (α →₀ M) ≃ₗ[R] M :=
  { Finsupp.equivFunOnFinite.trans (Equiv.funUnique α M) with
    map_add' := fun _ _ => rfl
    map_smul' := fun _ _ => rfl }

Linear equivalence between finitely supported functions on a singleton type and their codomain

Informal description

Given a type $\alpha$ with a unique element and a module $M$ over a semiring $R$, the space of finitely supported functions $\alpha \to_{\text{f}} M$ is linearly equivalent to $M$ itself. The equivalence maps a finitely supported function $f$ to its value at the unique element of $\alpha$, and conversely, any element $m \in M$ corresponds to the finitely supported function that sends the unique element of $\alpha$ to $m$.

Finsupp.LinearEquiv.finsuppUnique_apply theorem

(f : α →₀ M) : LinearEquiv.finsuppUnique R M α f = f default

Full source

@[simp]
theorem LinearEquiv.finsuppUnique_apply (f : α →₀ M) :
    LinearEquiv.finsuppUnique R M α f = f default :=
  rfl

Evaluation of Finitely Supported Function at Unique Element via Linear Equivalence

Informal description

For any finitely supported function $f \colon \alpha \to_{\text{f}} M$ on a type $\alpha$ with a unique element, the linear equivalence `LinearEquiv.finsuppUnique` maps $f$ to its value at the unique element of $\alpha$, i.e., $f(\text{default})$.

Finsupp.LinearEquiv.finsuppUnique_symm_apply theorem

(m : M) : (LinearEquiv.finsuppUnique R M α).symm m = Finsupp.single default m

Full source

@[simp]
theorem LinearEquiv.finsuppUnique_symm_apply (m : M) :
    (LinearEquiv.finsuppUnique R M α).symm m = Finsupp.single default m := by
  ext; simp [LinearEquiv.finsuppUnique, Equiv.funUnique, single, Pi.single,
    equivFunOnFinite, Function.update]

Inverse of Linear Equivalence Between Finitely Supported Functions on a Unique Type and Their Codomain

Informal description

For any module $M$ over a semiring $R$ and any type $\alpha$ with a unique element, the inverse of the linear equivalence `LinearEquiv.finsuppUnique` maps an element $m \in M$ to the finitely supported function $\alpha \to_{\text{f}} M$ that takes the value $m$ at the default element of $\alpha$ and zero elsewhere. In other words, $(\text{LinearEquiv.finsuppUnique}\, R\, M\, \alpha)^{-1}(m) = \text{single}(\text{default}, m)$.

Finsupp.lcoeFun definition

: (α →₀ M) →ₗ[R] α → M

Full source

/-- Forget that a function is finitely supported.

This is the linear version of `Finsupp.toFun`. -/
@[simps]
def lcoeFun : (α →₀ M) →ₗ[R] α → M where
  toFun := (⇑)
  map_add' x y := by
    ext
    simp
  map_smul' x y := by
    ext
    simp

Linear map from finitely supported functions to functions

Informal description

The linear map that forgets the finitely supported property of a function, sending a finitely supported function $f \colon \alpha \to_{\text{f}} M$ to the underlying function $f \colon \alpha \to M$. This map preserves addition and scalar multiplication.

LinearMap.splittingOfFunOnFintypeSurjective definition

[Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) : (α → R) →ₗ[R] M

Full source

/-- 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

Splitting of a surjective linear map to functions on a finite type

Informal description

Given a finite type $\alpha$, a semiring $R$, and a surjective $R$-linear map $f \colon M \to (\alpha \to R)$, there exists an $R$-linear splitting map $(\alpha \to R) \to M$ that provides a right inverse to $f$. More precisely, the splitting map is constructed by lifting the canonical basis vectors of $\alpha \to R$ (via the linear equivalence with finitely supported functions) and using the surjectivity of $f$ to choose preimages.

LinearMap.splittingOfFunOnFintypeSurjective_splits theorem

 [Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) : f.comp (splittingOfFunOnFintypeSurjective f s) = LinearMap.id

Full source

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]

Splitting of Surjective Linear Maps to Function Spaces on Finite Types Preserves Identity

Informal description

Let $\alpha$ be a finite type, $R$ a semiring, and $M$ an $R$-module. Given a surjective $R$-linear map $f \colon M \to (\alpha \to R)$, the composition of $f$ with its splitting map $\text{splittingOfFunOnFintypeSurjective}\,f\,s$ equals the identity map on $\alpha \to R$. That is, $$f \circ \text{splittingOfFunOnFintypeSurjective}\,f\,s = \text{id}.$$

LinearMap.leftInverse_splittingOfFunOnFintypeSurjective theorem

[Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) : LeftInverse f (splittingOfFunOnFintypeSurjective f s)

Full source

theorem leftInverse_splittingOfFunOnFintypeSurjective [Finite α] (f : M →ₗ[R] α → R)
    (s : Surjective f) : LeftInverse f (splittingOfFunOnFintypeSurjective f s) := fun g =>
  LinearMap.congr_fun (splittingOfFunOnFintypeSurjective_splits f s) g

Splitting Map is Left Inverse of Surjective Linear Map on Finite Function Spaces

Informal description

Let $\alpha$ be a finite type, $R$ a semiring, and $M$ an $R$-module. Given a surjective $R$-linear map $f \colon M \to (\alpha \to R)$, the splitting map $\text{splittingOfFunOnFintypeSurjective}\,f\,s$ is a left inverse of $f$, meaning that for every $g \in \alpha \to R$, we have $f(\text{splittingOfFunOnFintypeSurjective}\,f\,s\,(g)) = g$.

LinearMap.splittingOfFunOnFintypeSurjective_injective theorem

[Finite α] (f : M →ₗ[R] α → R) (s : Surjective f) : Injective (splittingOfFunOnFintypeSurjective f s)

Full source

theorem splittingOfFunOnFintypeSurjective_injective [Finite α] (f : M →ₗ[R] α → R)
    (s : Surjective f) : Injective (splittingOfFunOnFintypeSurjective f s) :=
  (leftInverse_splittingOfFunOnFintypeSurjective f s).injective

Injectivity of the Splitting Map for Surjective Linear Maps to Finite Function Spaces

Informal description

Let $\alpha$ be a finite type, $R$ a semiring, and $M$ an $R$-module. Given a surjective $R$-linear map $f \colon M \to (\alpha \to R)$, the splitting map $\mathrm{splittingOfFunOnFintypeSurjective}\,f\,s \colon (\alpha \to R) \to M$ is injective.

Tags