Documentation

Mathlib.LinearAlgebra.Finsupp.Pi

Properties of the module α →₀ M #

Tags #

function with finite support, module, linear algebra

noncomputable def Finsupp.LinearEquiv.finsuppUnique (R : Type u_1) (M : Type u_3) [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] :
(α →₀ M) ≃ₗ[R] M

If α has a unique term, then the type of finitely supported functions α →₀ M is R-linearly equivalent to M.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Finsupp.LinearEquiv.finsuppUnique_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] (α : Type u_4) [Unique α] (f : α →₀ M) :
    (finsuppUnique R M α) f = f default
    @[simp]
    theorem Finsupp.LinearEquiv.finsuppUnique_symm_apply {R : Type u_1} {M : Type u_3} [AddCommMonoid M] [Semiring R] [Module R M] {α : Type u_4} [Unique α] (m : M) :
    def Finsupp.lcoeFun {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] :
    (α →₀ M) →ₗ[R] αM

    Forget that a function is finitely supported.

    This is the linear version of Finsupp.toFun.

    Equations
    Instances For
      @[simp]
      theorem Finsupp.lcoeFun_apply {α : Type u_1} {M : Type u_2} {R : Type u_5} [Semiring R] [AddCommMonoid M] [Module R M] (a✝ : α →₀ M) (a : α) :
      lcoeFun a✝ a = a✝ a
      def LinearMap.splittingOfFunOnFintypeSurjective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} [Finite α] (f : M →ₗ[R] αR) (s : Function.Surjective f) :
      (αR) →ₗ[R] M

      A surjective linear map to functions on a finite type has a splitting.

      Equations
      Instances For
        def Finsupp.submodule {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (S : αSubmodule R M) :
        Submodule R (α →₀ M)

        Given a family Sᵢ of R-submodules of M indexed by a type α, this is the R-submodule of α →₀ M of functions f such that f i ∈ Sᵢ for all i : α.

        Equations
        Instances For
          @[simp]
          theorem Finsupp.mem_submodule_iff {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] {α : Type u_4} (S : αSubmodule R M) (x : α →₀ M) :
          x submodule S ∀ (i : α), x i S i
          theorem Finsupp.ker_mapRange {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (I : Type u_5) :
          theorem Finsupp.range_mapRange_linearMap {R : Type u_1} {M : Type u_2} {N : Type u_3} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (f : M →ₗ[R] N) (hf : LinearMap.ker f = ) (I : Type u_5) :
          noncomputable def FunOnFinite.map {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} [Finite X] [Finite Y] (f : XY) (s : XM) :
          YM

          The map (X → M) → (Y → M) induced by a map X → Y between finite types.

          Equations
          Instances For
            theorem FunOnFinite.map_apply_apply {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} [Fintype X] [Finite Y] [DecidableEq Y] (f : XY) (s : XM) (y : Y) :
            map f s y = x : X with f x = y, s x
            @[simp]
            theorem FunOnFinite.map_piSingle {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : XY) (x : X) (m : M) :
            map f (Pi.single x m) = Pi.single (f x) m
            theorem FunOnFinite.map_id (M : Type u_4) [AddCommMonoid M] {X : Type u_5} [Finite X] :
            theorem FunOnFinite.map_comp {M : Type u_4} [AddCommMonoid M] {X : Type u_5} {Y : Type u_6} {Z : Type u_7} [Finite X] [Finite Y] [Finite Z] (g : YZ) (f : XY) :
            map (g f) = map g map f
            noncomputable def FunOnFinite.linearMap (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} [Finite X] [Finite Y] (f : XY) :
            (XM) →ₗ[R] YM

            The linear map (X → M) →ₗ[R] (Y → M) induced by a map X → Y between finite types.

            Equations
            Instances For
              theorem FunOnFinite.linearMap_apply_apply (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} [Fintype X] [Finite Y] [DecidableEq Y] (f : XY) (s : XM) (y : Y) :
              (linearMap R M f) s y = {x : X | f x = y}.sum s
              @[simp]
              theorem FunOnFinite.linearMap_piSingle (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} [Finite X] [Finite Y] [DecidableEq X] [DecidableEq Y] (f : XY) (x : X) (m : M) :
              (linearMap R M f) (Pi.single x m) = Pi.single (f x) m
              @[simp]
              theorem FunOnFinite.linearMap_id (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] (X : Type u_6) [Finite X] :
              theorem FunOnFinite.linearMap_comp (R : Type u_4) (M : Type u_5) [Semiring R] [AddCommMonoid M] [Module R M] {X : Type u_6} {Y : Type u_7} {Z : Type u_8} [Finite X] [Finite Y] [Finite Z] (f : XY) (g : YZ) :
              linearMap R M (g f) = linearMap R M g ∘ₗ linearMap R M f