Mathlib.LinearAlgebra.DFinsupp

DFinsupp.lmk definition

(s : Finset ι) : (∀ i : (↑s : Set ι), M i) →ₗ[R] Π₀ i, M i

Full source

/-- `DFinsupp.mk` as a `LinearMap`. -/
def lmk (s : Finset ι) : (∀ i : (↑s : Set ι), M i) →ₗ[R] Π₀ i, M i where
  toFun := mk s
  map_add' _ _ := mk_add
  map_smul' c x := mk_smul c x

Linear map construction of dependent functions with finite support

Informal description

For a finite set $s$ of indices and a family of $R$-modules $M_i$ indexed by $i \in \iota$, the linear map version of `DFinsupp.mk` takes a function $x$ defined on $s$ (where $x_i \in M_i$ for each $i \in s$) and returns the dependent function with finite support in $\Pi_{i} M_i$ that equals $x_i$ for $i \in s$ and is zero elsewhere. This map is $R$-linear, meaning it preserves addition and scalar multiplication.

DFinsupp.lsingle definition

(i) : M i →ₗ[R] Π₀ i, M i

Full source

/-- `DFinsupp.single` as a `LinearMap` -/
def lsingle (i) : M i →ₗ[R] Π₀ i, M i :=
  { DFinsupp.singleAddHom _ _ with
    toFun := single i
    map_smul' := single_smul }

Linear Kronecker delta function for dependent functions with finite support

Informal description

For a given index $i$, the function `DFinsupp.lsingle i` is a linear map from the module $M_i$ to the module of dependent functions with finite support $\Pi₀ i, M_i$. It maps an element $m \in M_i$ to the dependent Kronecker delta function `single i m$, which is zero everywhere except at index $i$ where it takes the value $m$. This map preserves addition and scalar multiplication: 1. `single i (m₁ + m₂) = single i m₁ + single i m₂` for all $m₁, m₂ \in M_i$. 2. `single i (r • m) = r • single i m` for all $r \in R$ and $m \in M_i$.

DFinsupp.lhom_ext theorem

⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ (h : ∀ i x, φ (single i x) = ψ (single i x)) : φ = ψ

Full source

/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere. -/
theorem lhom_ext ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ (h : ∀ i x, φ (single i x) = ψ (single i x)) : φ = ψ :=
  LinearMap.toAddMonoidHom_injective <| addHom_ext h

Extensionality of Linear Maps on Dependent Functions with Finite Support

Informal description

Let $R$ be a semiring, $\{M_i\}_{i \in \iota}$ be a family of $R$-modules, and $N$ be an $R$-module. For any two $R$-linear maps $\varphi, \psi \colon (\Pi_{i \in \iota} M_i) \to N$, if $\varphi(\text{single}_i(x)) = \psi(\text{single}_i(x))$ for every index $i$ and every element $x \in M_i$, then $\varphi = \psi$. Here, $\text{single}_i(x)$ denotes the dependent function with finite support that maps $i$ to $x$ and all other indices to $0$.

DFinsupp.lhom_ext' theorem

⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ (h : ∀ i, φ.comp (lsingle i) = ψ.comp (lsingle i)) : φ = ψ

Full source

/-- Two `R`-linear maps from `Π₀ i, M i` which agree on each `single i x` agree everywhere.

See note [partially-applied ext lemmas].
After applying this lemma, if `M = R` then it suffices to verify
`φ (single a 1) = ψ (single a 1)`. -/
@[ext 1100]
theorem lhom_ext' ⦃φ ψ : (Π₀ i, M i) →ₗ[R] N⦄ (h : ∀ i, φ.comp (lsingle i) = ψ.comp (lsingle i)) :
    φ = ψ :=
  lhom_ext fun i => LinearMap.congr_fun (h i)

Extensionality of Linear Maps via Composition with Kronecker Delta Functions

Informal description

Let $R$ be a semiring, $\{M_i\}_{i \in \iota}$ be a family of $R$-modules, and $N$ be an $R$-module. For any two $R$-linear maps $\varphi, \psi \colon (\Pi_{i \in \iota} M_i) \to N$, if the compositions $\varphi \circ \text{lsingle}_i$ and $\psi \circ \text{lsingle}_i$ are equal for every index $i$, then $\varphi = \psi$. Here, $\text{lsingle}_i$ denotes the linear Kronecker delta function that maps an element of $M_i$ to the corresponding dependent function with finite support in $\Pi₀ i, M_i$.

DFinsupp.lmk_apply theorem

(s : Finset ι) (x) : (lmk s : _ →ₗ[R] Π₀ i, M i) x = mk s x

Full source

theorem lmk_apply (s : Finset ι) (x) : (lmk s : _ →ₗ[R] Π₀ i, M i) x = mk s x :=
  rfl

Equality of Linear Construction and Pointwise Construction for Dependent Functions with Finite Support

Informal description

Let $R$ be a semiring, $\iota$ an index set, and $\{M_i\}_{i \in \iota}$ a family of $R$-modules. For any finite subset $s \subseteq \iota$ and any function $x \colon s \to \bigcup_{i \in s} M_i$ (where $x_i \in M_i$ for each $i \in s$), the linear map `lmk s` applied to $x$ equals the dependent function with finite support `mk s x`, which is the function that agrees with $x$ on $s$ and is zero elsewhere. In mathematical notation: $$(\operatorname{lmk} s)(x) = \operatorname{mk} s x$$

DFinsupp.lsingle_apply theorem

(i : ι) (x : M i) : (lsingle i : (M i) →ₗ[R] _) x = single i x

Full source

@[simp]
theorem lsingle_apply (i : ι) (x : M i) : (lsingle i : (M i) →ₗ[R] _) x = single i x :=
  rfl

Evaluation of Linear Kronecker Delta Function: $\operatorname{lsingle}_i x = \operatorname{single}_i x$

Informal description

For any index $i$ and element $x \in M_i$, the linear map $\operatorname{lsingle}_i$ applied to $x$ equals the dependent Kronecker delta function $\operatorname{single}_i x$ in the module $\Pi_{i, M_i}$ of dependent functions with finite support.

DFinsupp.lapply definition

(i : ι) : (Π₀ i, M i) →ₗ[R] M i

Full source

/-- Interpret `fun (f : Π₀ i, M i) ↦ f i` as a linear map. -/
def lapply (i : ι) : (Π₀ i, M i) →ₗ[R] M i where
  toFun f := f i
  map_add' f g := add_apply f g i
  map_smul' c f := smul_apply c f i

Linear evaluation map for dependent functions with finite support

Informal description

For a given index $i$ in the index set $\iota$, the linear map $\operatorname{lapply}_i$ evaluates a dependent function $f$ with finite support (i.e., $f \in \Pi_{i, M_i}$) at the index $i$, returning the value $f(i) \in M_i$. This map is linear with respect to the module structures on $\Pi_{i, M_i}$ and $M_i$.

DFinsupp.lapply_apply theorem

(i : ι) (f : Π₀ i, M i) : (lapply i : (Π₀ i, M i) →ₗ[R] _) f = f i

Full source

@[simp]
theorem lapply_apply (i : ι) (f : Π₀ i, M i) : (lapply i : (Π₀ i, M i) →ₗ[R] _) f = f i :=
  rfl

Evaluation of Linear Map $\operatorname{lapply}_i$ at $f$ Equals $f(i)$

Informal description

For any index $i$ in the index set $\iota$ and any dependent function $f$ with finite support in $\Pi_{i, M_i}$, the evaluation of the linear map $\operatorname{lapply}_i$ at $f$ equals the value of $f$ at $i$, i.e., $\operatorname{lapply}_i(f) = f(i)$.

DFinsupp.injective_pi_lapply theorem

: Function.Injective (LinearMap.pi (R := R) <| lapply (M := M))

Full source

theorem injective_pi_lapply : Function.Injective (LinearMap.pi (R := R) <| lapply (M := M)) :=
  fun _ _ h ↦ ext fun _ ↦ congr_fun h _

Injectivity of the Linear Map $\operatorname{LinearMap.pi} \circ \operatorname{lapply}$ on Dependent Functions with Finite Support

Informal description

The linear map $\operatorname{LinearMap.pi} (R := R) (\operatorname{lapply} (M := M))$ is injective. In other words, for any two dependent functions $f, g \in \Pi_{i, M_i}$ with finite support, if $\operatorname{lapply}_i(f) = \operatorname{lapply}_i(g)$ for all indices $i$, then $f = g$.

DFinsupp.lapply_comp_lsingle_same theorem

[DecidableEq ι] (i : ι) : lapply i ∘ₗ lsingle i = (.id : M i →ₗ[R] M i)

Full source

@[simp]
theorem lapply_comp_lsingle_same [DecidableEq ι] (i : ι) :
    lapplylapply i ∘ₗ lsingle i = (.id : M i →ₗ[R] M i) := by ext; simp

Composition of Evaluation and Kronecker Delta Maps Yields Identity on $M_i$

Informal description

For any index $i$ in a decidable index set $\iota$, the composition of the linear evaluation map $\operatorname{lapply}_i$ with the linear Kronecker delta map $\operatorname{lsingle}_i$ is equal to the identity linear map on the module $M_i$. That is, \[ \operatorname{lapply}_i \circ \operatorname{lsingle}_i = \operatorname{id}_{M_i}. \]

DFinsupp.lapply_comp_lsingle_of_ne theorem

[DecidableEq ι] (i i' : ι) (h : i ≠ i') : lapply i ∘ₗ lsingle i' = (0 : M i' →ₗ[R] M i)

Full source

@[simp]
theorem lapply_comp_lsingle_of_ne [DecidableEq ι] (i i' : ι) (h : i ≠ i') :
    lapplylapply i ∘ₗ lsingle i' = (0 : M i' →ₗ[R] M i) := by ext; simp [h.symm]

Vanishing of Linear Evaluation on Off-Diagonal Kronecker Delta: $\operatorname{lapply}_i \circ \operatorname{lsingle}_{i'} = 0$ for $i \neq i'$

Informal description

For any distinct indices $i$ and $i'$ in a decidable index set $\iota$, the composition of the linear evaluation map $\operatorname{lapply}_i$ with the linear Kronecker delta map $\operatorname{lsingle}_{i'}$ is the zero linear map from $M_{i'}$ to $M_i$. In other words, if $i \neq i'$, then for any $m \in M_{i'}$, we have $\operatorname{lapply}_i (\operatorname{lsingle}_{i'} m) = 0$.

DFinsupp.instEquivLikeLinearEquiv instance

 {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ']
  [RingHomInvPair σ' σ] (M : Type*) (M₂ : Type*) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
  EquivLike (LinearEquiv σ M M₂) M M₂

Full source

instance {R : Type*} {S : Type*} [Semiring R] [Semiring S] (σ : R →+* S)
    {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type*) (M₂ : Type*)
    [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
    EquivLike (LinearEquiv σ M M₂) M M₂ :=
  inferInstance

Linear Equivalences as Equivalence-like Mappings Between Modules

Informal description

For any semirings $R$ and $S$, ring homomorphisms $\sigma: R \to S$ and $\sigma': S \to R$ that are inverse pairs, and additive commutative monoids $M$ and $M₂$ equipped with module structures over $R$ and $S$ respectively, the type of linear equivalences $\text{LinearEquiv} \, \sigma \, M \, M₂$ forms an equivalence-like class between $M$ and $M₂$. This means that terms of this type can be injectively coerced to bijections between $M$ and $M₂$ that respect the module structures.

DFinsupp.lsum definition

[Semiring S] [Module S N] [SMulCommClass R S N] : (∀ i, M i →ₗ[R] N) ≃ₗ[S] (Π₀ i, M i) →ₗ[R] N

Full source

/-- The `DFinsupp` version of `Finsupp.lsum`.

See note [bundled maps over different rings] for why separate `R` and `S` semirings are used. -/
@[simps]
def lsum [Semiring S] [Module S N] [SMulCommClass R S N] :
    (∀ i, M i →ₗ[R] N) ≃ₗ[S] (Π₀ i, M i) →ₗ[R] N where
  toFun F :=
    { toFun := sumAddHom fun i => (F i).toAddMonoidHom
      map_add' := (DFinsupp.liftAddHom fun (i : ι) => (F i).toAddMonoidHom).map_add
      map_smul' := fun c f => by
        dsimp
        apply DFinsupp.induction f
        · rw [smul_zero, AddMonoidHom.map_zero, smul_zero]
        · intro a b f _ _ hf
          rw [smul_add, AddMonoidHom.map_add, AddMonoidHom.map_add, smul_add, hf, ← single_smul,
            sumAddHom_single, sumAddHom_single, LinearMap.toAddMonoidHom_coe,
            LinearMap.map_smul] }
  invFun F i := F.comp (lsingle i)
  left_inv F := by
    ext
    simp
  right_inv F := by
    refine DFinsupp.lhom_ext' (fun i ↦ ?_)
    ext
    simp
  map_add' F G := by
    refine DFinsupp.lhom_ext' (fun i ↦ ?_)
    ext
    simp
  map_smul' c F := by
    refine DFinsupp.lhom_ext' (fun i ↦ ?_)
    ext
    simp

Linear summation of dependent functions with finite support

Informal description

Given a semiring $S$, an $S$-module $N$, and a family of $R$-linear maps $F_i \colon M_i \to N$ for each index $i$, where $R$ and $S$ act commutatively on $N$, the function `DFinsupp.lsum` constructs an $S$-linear equivalence between the type of families of linear maps $(∀ i, M_i →ₗ[R] N)$ and the type of linear maps from the dependent functions with finite support $Π₀ i, M_i$ to $N$. More explicitly, `DFinsupp.lsum` maps a family of linear maps $F = (F_i)_{i \in ι}$ to the linear map that sums the evaluations of each $F_i$ on the corresponding component of a dependent function with finite support. The inverse operation takes a linear map $G \colon Π₀ i, M_i →ₗ[R] N$ and returns the family of linear maps obtained by precomposing $G$ with the linear Kronecker delta functions `lsingle i`. This construction preserves addition and scalar multiplication in the following sense: 1. For any two families $F$ and $G$, `lsum (F + G) = lsum F + lsum G`. 2. For any scalar $c \in S$ and family $F$, `lsum (c • F) = c • lsum F`.

DFinsupp.lsum_single theorem

 [Semiring S] [Module S N] [SMulCommClass R S N] (F : ∀ i, M i →ₗ[R] N) (i) (x : M i) : lsum S F (single i x) = F i x

Full source

/-- While `simp` can prove this, it is often convenient to avoid unfolding `lsum` into `sumAddHom`
with `DFinsupp.lsum_apply_apply`. -/
theorem lsum_single [Semiring S] [Module S N] [SMulCommClass R S N] (F : ∀ i, M i →ₗ[R] N) (i)
    (x : M i) : lsum S F (single i x) = F i x := by
  simp

Evaluation of Linear Summation on Single-Element Function: $\operatorname{lsum}_S F (\operatorname{single}_i x) = F_i x$

Informal description

Let $R$ and $S$ be semirings, $N$ an $S$-module where $R$ and $S$ act commutatively on $N$, and $(M_i)_{i \in \iota}$ a family of $R$-modules. For any family of $R$-linear maps $F = (F_i \colon M_i \to N)_{i \in \iota}$, the linear summation map $\operatorname{lsum}_S F \colon \Pi_{i \in \iota} M_i \to N$ satisfies \[ \operatorname{lsum}_S F (\operatorname{single}_i x) = F_i x \] for every index $i$ and element $x \in M_i$.

DFinsupp.lsum_lsingle theorem

[Semiring S] [∀ i, Module S (M i)] [∀ i, SMulCommClass R S (M i)] : lsum S (lsingle (R := R) (M := M)) = .id

Full source

theorem lsum_lsingle [Semiring S] [∀ i, Module S (M i)] [∀ i, SMulCommClass R S (M i)] :
    lsum S (lsingle (R := R) (M := M)) = .id :=
  lhom_ext (lsum_single _ _)

Identity Property of Linear Summation with Kronecker Delta Functions

Informal description

Let $R$ and $S$ be semirings, and let $(M_i)_{i \in \iota}$ be a family of $S$-modules where the actions of $R$ and $S$ on each $M_i$ commute. Then the linear summation map $\operatorname{lsum}_S$ applied to the family of linear Kronecker delta functions $(\operatorname{lsingle}_i)_{i \in \iota}$ equals the identity map on $\Pi_{i \in \iota} M_i$. In other words, for any dependent function $f \in \Pi_{i \in \iota} M_i$ with finite support, we have: \[ \operatorname{lsum}_S (\operatorname{lsingle}_i)_{i \in \iota} (f) = f \]

DFinsupp.iSup_range_lsingle theorem

: ⨆ i, LinearMap.range (lsingle (R := R) (M := M) i) = ⊤

Full source

theorem iSup_range_lsingle : ⨆ i, LinearMap.range (lsingle (R := R) (M := M) i) = ⊤ :=
  top_le_iff.mp fun m _ ↦ by
    rw [← LinearMap.id_apply (R := R) m, ← lsum_lsingle ℕ]
    exact dfinsuppSumAddHom_mem _ _ _ fun i _ ↦ Submodule.mem_iSup_of_mem i ⟨_, rfl⟩

Supremum of Ranges of Linear Kronecker Delta Functions is Top Submodule

Informal description

For a family of $R$-modules $(M_i)_{i \in \iota}$, the supremum of the ranges of the linear Kronecker delta functions $\operatorname{lsingle}_i \colon M_i \to \Pi_{i \in \iota} M_i$ over all indices $i$ equals the top submodule of $\Pi_{i \in \iota} M_i$. That is, \[ \bigsqcup_{i \in \iota} \operatorname{range}(\operatorname{lsingle}_i) = \top. \]

DFinsupp.mker_mapRangeAddMonoidHom theorem

 (f : ∀ i, β₁ i →+ β₂ i) :
  AddMonoidHom.mker (mapRange.addMonoidHom f) =
    (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mker (f i))).comap coeFnAddMonoidHom

Full source

lemma mker_mapRangeAddMonoidHom (f : ∀ i, β₁ i →+ β₂ i) :
    AddMonoidHom.mker (mapRange.addMonoidHom f) =
      (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mker (f i))).comap coeFnAddMonoidHom := by
  ext
  simp [AddSubmonoid.pi, DFinsupp.ext_iff]

Kernel of Pointwise Mapping of Additive Monoid Homomorphisms on Dependent Functions with Finite Support

Informal description

Let $\beta_1$ and $\beta_2$ be families of additive monoids indexed by $i$, and let $f_i \colon \beta_1 i \to \beta_2 i$ be a family of additive monoid homomorphisms. The kernel of the induced additive monoid homomorphism $\text{mapRange.addMonoidHom}\, f \colon \Pi_{i} \beta_1 i \to \Pi_{i} \beta_2 i$ is equal to the preimage under the coefficient function homomorphism of the product of the kernels of each $f_i$ over the universal set of indices. More precisely: \[ \ker(\text{mapRange.addMonoidHom}\, f) = \left(\prod_{i} \ker(f_i)\right) \cap \left(\Pi_{i} \beta_1 i\right), \] where the product is taken over all indices $i$ and $\Pi_{i} \beta_1 i$ denotes the space of dependent functions with finite support.

DFinsupp.mrange_mapRangeAddMonoidHom theorem

 (f : ∀ i, β₁ i →+ β₂ i) :
  AddMonoidHom.mrange (mapRange.addMonoidHom f) =
    (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mrange (f i))).comap coeFnAddMonoidHom

Full source

lemma mrange_mapRangeAddMonoidHom (f : ∀ i, β₁ i →+ β₂ i) :
    AddMonoidHom.mrange (mapRange.addMonoidHom f) =
      (AddSubmonoid.pi Set.univ (fun i ↦ AddMonoidHom.mrange (f i))).comap coeFnAddMonoidHom := by
  classical
  ext x
  simp only [AddSubmonoid.mem_comap, mapRange.addMonoidHom_apply, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.not_mem_support_iff.mp mem, mk_of_not_mem mem, map_zero]

Range of Pointwise Mapping of Dependent Functions with Finite Support

Informal description

Given a family of additive monoid homomorphisms $f_i \colon \beta_1 i \to \beta_2 i$ for each index $i$, the range of the induced additive monoid homomorphism $\text{mapRange.addMonoidHom}\, f \colon (\Pi_{i} \beta_1 i) \to (\Pi_{i} \beta_2 i)$ is equal to the preimage under the coefficient function homomorphism of the product of the ranges of the individual $f_i$ homomorphisms over all indices. That is, \[ \text{range}(\text{mapRange.addMonoidHom}\, f) = \left(\prod_{i} \text{range}(f_i)\right) \cap \left(\Pi_{i} \beta_2 i\right)_{\text{fin}}, \] where $(\Pi_{i} \beta_2 i)_{\text{fin}}$ denotes the space of dependent functions with finite support.

DFinsupp.mapRange_smul theorem

 (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (r : R) (hf' : ∀ i x, f i (r • x) = r • f i x) (g : Π₀ i, β₁ i) :
  mapRange f hf (r • g) = r • mapRange f hf g

Full source

theorem mapRange_smul (f : ∀ i, β₁ i → β₂ i) (hf : ∀ i, f i 0 = 0) (r : R)
    (hf' : ∀ i x, f i (r • x) = r • f i x) (g : Π₀ i, β₁ i) :
    mapRange f hf (r • g) = r • mapRange f hf g := by
  ext
  simp only [mapRange_apply f, coe_smul, Pi.smul_apply, hf']

Scalar Multiplication Commutes with Range Mapping in Dependent Functions

Informal description

Let $R$ be a ring, and let $\beta_1, \beta_2$ be families of $R$-modules indexed by $i$. Given a family of functions $f_i \colon \beta_1 i \to \beta_2 i$ such that each $f_i$ maps zero to zero, and a scalar $r \in R$, suppose that each $f_i$ is $R$-linear in the sense that $f_i (r \cdot x) = r \cdot f_i (x)$ for all $x \in \beta_1 i$. Then for any dependent function $g \in \Pi_{i} \beta_1 i$ with finite support, we have \[ \text{mapRange}\, f\, hf\, (r \cdot g) = r \cdot \text{mapRange}\, f\, hf\, g, \] where $\text{mapRange}$ applies each $f_i$ to the corresponding value of $g$.

DFinsupp.mapRange.linearMap definition

(f : ∀ i, β₁ i →ₗ[R] β₂ i) : (Π₀ i, β₁ i) →ₗ[R] Π₀ i, β₂ i

Full source

/-- `DFinsupp.mapRange` as a `LinearMap`. -/
@[simps! apply]
def mapRange.linearMap (f : ∀ i, β₁ i →ₗ[R] β₂ i) : (Π₀ i, β₁ i) →ₗ[R] Π₀ i, β₂ i :=
  { mapRange.addMonoidHom fun i => (f i).toAddMonoidHom with
    toFun := mapRange (fun i x => f i x) fun i => (f i).map_zero
    map_smul' := fun r => mapRange_smul _ (fun i => (f i).map_zero) _ fun i => (f i).map_smul r }

Linear map induced by pointwise mapping of dependent functions with finite support

Informal description

Given a family of $R$-linear maps $f_i \colon \beta_1 i \to \beta_2 i$ for each index $i$, the function `DFinsupp.mapRange.linearMap` constructs an $R$-linear map from the space of dependent functions with finite support $\Pi_{i} \beta_1 i$ to $\Pi_{i} \beta_2 i$. This linear map applies each $f_i$ pointwise to the corresponding value of the input function, preserves the zero function, and respects both addition and scalar multiplication.

DFinsupp.mapRange.linearMap_id theorem

: (mapRange.linearMap fun i => (LinearMap.id : β₂ i →ₗ[R] _)) = LinearMap.id

Full source

@[simp]
theorem mapRange.linearMap_id :
    (mapRange.linearMap fun i => (LinearMap.id : β₂ i →ₗ[R] _)) = LinearMap.id := by
  ext
  simp [linearMap]

Identity Property of `mapRange.linearMap`

Informal description

The linear map `mapRange.linearMap` applied to the family of identity linear maps `(LinearMap.id : β₂ i →ₗ[R] β₂ i)` for each index `i` is equal to the identity linear map on the space of dependent functions with finite support `Π₀ i, β₂ i`. That is, \[ \text{mapRange.linearMap}\, (\lambda i, \text{id}) = \text{id}, \] where `id` denotes the identity linear map.

DFinsupp.mapRange.linearMap_comp theorem

 (f : ∀ i, β₁ i →ₗ[R] β₂ i) (f₂ : ∀ i, β i →ₗ[R] β₁ i) :
  (mapRange.linearMap fun i => (f i).comp (f₂ i)) = (mapRange.linearMap f).comp (mapRange.linearMap f₂)

Full source

theorem mapRange.linearMap_comp (f : ∀ i, β₁ i →ₗ[R] β₂ i) (f₂ : ∀ i, β i →ₗ[R] β₁ i) :
    (mapRange.linearMap fun i => (f i).comp (f₂ i)) =
      (mapRange.linearMap f).comp (mapRange.linearMap f₂) :=
  LinearMap.ext <| mapRange_comp (fun i x => f i x) (fun i x => f₂ i x)
    (fun i => (f i).map_zero) (fun i => (f₂ i).map_zero) (by simp)

Composition of Linear Maps on Dependent Functions with Finite Support

Informal description

Let $R$ be a semiring, and let $\beta$, $\beta_1$, $\beta_2$ be families of $R$-modules indexed by $\iota$. Given families of $R$-linear maps $f_i \colon \beta_1 i \to \beta_2 i$ and $f_{2,i} \colon \beta i \to \beta_1 i$ for each $i \in \iota$, the composition of the induced linear maps on dependent functions with finite support satisfies: \[ \operatorname{mapRange.linearMap} (f \circ f_2) = \operatorname{mapRange.linearMap} f \circ \operatorname{mapRange.linearMap} f_2 \] where $f \circ f_2$ denotes the pointwise composition $(f \circ f_2)_i = f_i \circ f_{2,i}$.

DFinsupp.sum_mapRange_index.linearMap theorem

 [DecidableEq ι] {f : ∀ i, β₁ i →ₗ[R] β₂ i} {h : ∀ i, β₂ i →ₗ[R] N} {l : Π₀ i, β₁ i} :
  DFinsupp.lsum ℕ h (mapRange.linearMap f l) = DFinsupp.lsum ℕ (fun i => (h i).comp (f i)) l

Full source

theorem sum_mapRange_index.linearMap [DecidableEq ι] {f : ∀ i, β₁ i →ₗ[R] β₂ i}
    {h : ∀ i, β₂ i →ₗ[R] N} {l : Π₀ i, β₁ i} :
    DFinsupp.lsum ℕ h (mapRange.linearMap f l) = DFinsupp.lsum ℕ (fun i => (h i).comp (f i)) l := by
  classical simpa [DFinsupp.sumAddHom_apply] using sum_mapRange_index fun i => by simp

Linear Summation Commutes with Pointwise Linear Map Composition

Informal description

Let $R$ be a semiring, $\iota$ an index type with decidable equality, and $\beta_1, \beta_2$ families of $R$-modules indexed by $\iota$. Given a family of $R$-linear maps $f_i \colon \beta_1 i \to \beta_2 i$ for each $i \in \iota$, a family of $R$-linear maps $h_i \colon \beta_2 i \to N$ where $N$ is an $R$-module, and a dependent function $l \in \Pi_{i} \beta_1 i$ with finite support, we have: \[ \sum_{i} h_i(f_i(l(i))) = \sum_{i} (h_i \circ f_i)(l(i)) \] where the sums are taken over the finite support of $l$.

DFinsupp.ker_mapRangeLinearMap theorem

 (f : ∀ i, β₁ i →ₗ[R] β₂ i) :
  LinearMap.ker (mapRange.linearMap f) = (Submodule.pi Set.univ (fun i ↦ LinearMap.ker (f i))).comap (coeFnLinearMap R)

Full source

lemma ker_mapRangeLinearMap (f : ∀ i, β₁ i →ₗ[R] β₂ i) :
    LinearMap.ker (mapRange.linearMap f) =
      (Submodule.pi Set.univ (fun i ↦ LinearMap.ker (f i))).comap (coeFnLinearMap R) :=
  Submodule.toAddSubmonoid_injective <| mker_mapRangeAddMonoidHom (f · |>.toAddMonoidHom)

Kernel of Pointwise Linear Map on Dependent Functions with Finite Support

Informal description

Let $R$ be a semiring, and let $\beta_1$ and $\beta_2$ be families of $R$-modules indexed by $i$. Given a family of $R$-linear maps $f_i \colon \beta_1 i \to \beta_2 i$ for each $i$, the kernel of the induced linear map $\text{mapRange.linearMap}\, f \colon \Pi_{i} \beta_1 i \to \Pi_{i} \beta_2 i$ is equal to the preimage under the coefficient function linear map of the submodule consisting of all functions $g \colon \forall i, \beta_1 i$ such that $g(i) \in \ker(f_i)$ for every $i$. More precisely: \[ \ker(\text{mapRange.linearMap}\, f) = \left\{ g \in \Pi_{i} \beta_1 i \mid \forall i, g(i) \in \ker(f_i) \right\}. \]

DFinsupp.range_mapRangeLinearMap theorem

 (f : ∀ i, β₁ i →ₗ[R] β₂ i) :
  LinearMap.range (mapRange.linearMap f) = (Submodule.pi Set.univ (LinearMap.range <| f ·)).comap (coeFnLinearMap R)

Full source

lemma range_mapRangeLinearMap (f : ∀ i, β₁ i →ₗ[R] β₂ i) :
    LinearMap.range (mapRange.linearMap f) =
      (Submodule.pi Set.univ (LinearMap.range <| f ·)).comap (coeFnLinearMap R) :=
  Submodule.toAddSubmonoid_injective <| mrange_mapRangeAddMonoidHom (f · |>.toAddMonoidHom)

Range of Pointwise Linear Map on Dependent Functions with Finite Support

Informal description

Given a family of $R$-linear maps $f_i \colon \beta_1 i \to \beta_2 i$ for each index $i$, the range of the induced linear map $\text{mapRange.linearMap}\, f \colon (\Pi_{i} \beta_1 i) \to (\Pi_{i} \beta_2 i)$ on dependent functions with finite support is equal to the preimage under the coefficient linear map of the product submodule $\prod_{i} \text{range}(f_i)$. That is, \[ \text{range}(\text{mapRange.linearMap}\, f) = \left(\prod_{i} \text{range}(f_i)\right) \cap \left(\Pi_{i} \beta_2 i\right)_{\text{fin}}, \] where $(\Pi_{i} \beta_2 i)_{\text{fin}}$ denotes the space of dependent functions with finite support.

DFinsupp.mapRange.linearEquiv definition

(e : ∀ i, β₁ i ≃ₗ[R] β₂ i) : (Π₀ i, β₁ i) ≃ₗ[R] Π₀ i, β₂ i

Full source

/-- `DFinsupp.mapRange.linearMap` as a `LinearEquiv`. -/
@[simps apply]
def mapRange.linearEquiv (e : ∀ i, β₁ i ≃ₗ[R] β₂ i) : (Π₀ i, β₁ i) ≃ₗ[R] Π₀ i, β₂ i :=
  { mapRange.addEquiv fun i => (e i).toAddEquiv,
    mapRange.linearMap fun i => (e i).toLinearMap with
    toFun := mapRange (fun i x => e i x) fun i => (e i).map_zero
    invFun := mapRange (fun i x => (e i).symm x) fun i => (e i).symm.map_zero }

Linear equivalence of dependent functions with finite support via pointwise mapping

Informal description

Given a family of $R$-linear equivalences $e_i \colon \beta_1 i \simeq \beta_2 i$ for each index $i$, the function `DFinsupp.mapRange.linearEquiv` constructs an $R$-linear equivalence between the spaces of dependent functions with finite support $\Pi_{i} \beta_1 i$ and $\Pi_{i} \beta_2 i$. This equivalence applies each $e_i$ pointwise to the corresponding value of the input function, preserves the zero function, and respects both addition and scalar multiplication. The inverse function is constructed similarly using the inverses of the $e_i$.

DFinsupp.mapRange.linearEquiv_refl theorem

: (mapRange.linearEquiv fun i => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl _ _

Full source

@[simp]
theorem mapRange.linearEquiv_refl :
    (mapRange.linearEquiv fun i => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl _ _ :=
  LinearEquiv.ext mapRange_id

Identity Pointwise Linear Equivalence Yields Identity on Dependent Functions

Informal description

The linear equivalence obtained by applying the identity linear equivalence pointwise to each component of a dependent function with finite support is equal to the identity linear equivalence on the space of such functions. That is, for any family of $R$-modules $\beta_1 i$, we have: \[ \text{mapRange.linearEquiv} (\lambda i, \text{LinearEquiv.refl}_R (\beta_1 i)) = \text{LinearEquiv.refl}_R (\Pi_{i} \beta_1 i). \]

DFinsupp.mapRange.linearEquiv_trans theorem

 (f : ∀ i, β i ≃ₗ[R] β₁ i) (f₂ : ∀ i, β₁ i ≃ₗ[R] β₂ i) :
  (mapRange.linearEquiv fun i => (f i).trans (f₂ i)) = (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂)

Full source

theorem mapRange.linearEquiv_trans (f : ∀ i, β i ≃ₗ[R] β₁ i) (f₂ : ∀ i, β₁ i ≃ₗ[R] β₂ i) :
    (mapRange.linearEquiv fun i => (f i).trans (f₂ i)) =
      (mapRange.linearEquiv f).trans (mapRange.linearEquiv f₂) :=
  LinearEquiv.ext <| mapRange_comp (fun i x => f₂ i x) (fun i x => f i x)
    (fun i => (f₂ i).map_zero) (fun i => (f i).map_zero) (by simp)

Composition of Linear Equivalences on Dependent Functions with Finite Support

Informal description

Given two families of $R$-linear equivalences $f_i \colon \beta i \simeq \beta_1 i$ and $f_{2,i} \colon \beta_1 i \simeq \beta_2 i$ for each index $i$, the composition of the induced linear equivalences on dependent functions with finite support satisfies: \[ \operatorname{mapRange.linearEquiv} (f \circ f_2) = \operatorname{mapRange.linearEquiv} f \circ \operatorname{mapRange.linearEquiv} f_2 \] where $f \circ f_2$ denotes the pointwise composition $(f \circ f_2)_i = f_i \circ f_{2,i}$.

DFinsupp.mapRange.linearEquiv_symm theorem

(e : ∀ i, β₁ i ≃ₗ[R] β₂ i) : (mapRange.linearEquiv e).symm = mapRange.linearEquiv fun i => (e i).symm

Full source

@[simp]
theorem mapRange.linearEquiv_symm (e : ∀ i, β₁ i ≃ₗ[R] β₂ i) :
    (mapRange.linearEquiv e).symm = mapRange.linearEquiv fun i => (e i).symm :=
  rfl

Inverse of Pointwise Linear Equivalence on Dependent Functions with Finite Support

Informal description

Given a family of $R$-linear equivalences $e_i \colon \beta_1 i \simeq \beta_2 i$ for each index $i$, the inverse of the induced linear equivalence $\text{mapRange.linearEquiv}\, e \colon (\Pi_{i} \beta_1 i) \simeq (\Pi_{i} \beta_2 i)$ is equal to the linear equivalence obtained by applying the inverses $e_i^{-1}$ pointwise. That is, \[ (\text{mapRange.linearEquiv}\, e)^{-1} = \text{mapRange.linearEquiv}\, (\lambda i, e_i^{-1}). \]

DFinsupp.ker_mapRangeAddMonoidHom theorem

 [∀ i, AddCommGroup (β₁ i)] [∀ i, AddCommMonoid (β₂ i)] (f : ∀ i, β₁ i →+ β₂ i) :
  (mapRange.addMonoidHom f).ker = (AddSubgroup.pi Set.univ (f · |>.ker)).comap coeFnAddMonoidHom

Full source

lemma ker_mapRangeAddMonoidHom
    [∀ i, AddCommGroup (β₁ i)] [∀ i, AddCommMonoid (β₂ i)] (f : ∀ i, β₁ i →+ β₂ i) :
    (mapRange.addMonoidHom f).ker =
      (AddSubgroup.pi Set.univ (f · |>.ker)).comap coeFnAddMonoidHom :=
  AddSubgroup.toAddSubmonoid_injective <| mker_mapRangeAddMonoidHom f

Kernel of Pointwise Additive Homomorphism on Dependent Functions with Finite Support

Informal description

Let $\{\beta_1 i\}_{i \in \iota}$ and $\{\beta_2 i\}_{i \in \iota}$ be families of additive groups and additive commutative monoids, respectively, indexed by $\iota$. Given a family of additive group homomorphisms $f_i \colon \beta_1 i \to \beta_2 i$ for each $i \in \iota$, the kernel of the induced homomorphism $\text{mapRange.addMonoidHom}\, f \colon \Pi_{i} \beta_1 i \to \Pi_{i} \beta_2 i$ is equal to the preimage under the coefficient function homomorphism of the product of the kernels of each $f_i$ over the universal set of indices. More precisely: \[ \ker(\text{mapRange.addMonoidHom}\, f) = \left(\prod_{i \in \iota} \ker(f_i)\right) \cap \left(\Pi_{i} \beta_1 i\right), \] where $\Pi_{i} \beta_1 i$ denotes the space of dependent functions with finite support.

DFinsupp.range_mapRangeAddMonoidHom theorem

 [∀ i, AddCommGroup (β₁ i)] [∀ i, AddCommGroup (β₂ i)] (f : ∀ i, β₂ i →+ β₁ i) :
  (mapRange.addMonoidHom f).range = (AddSubgroup.pi Set.univ (f · |>.range)).comap coeFnAddMonoidHom

Full source

lemma range_mapRangeAddMonoidHom
    [∀ i, AddCommGroup (β₁ i)] [∀ i, AddCommGroup (β₂ i)] (f : ∀ i, β₂ i →+ β₁ i) :
    (mapRange.addMonoidHom f).range =
      (AddSubgroup.pi Set.univ (f · |>.range)).comap coeFnAddMonoidHom :=
  AddSubgroup.toAddSubmonoid_injective <| mrange_mapRangeAddMonoidHom f

Range of Pointwise Mapping of Dependent Functions with Finite Support

Informal description

Let $\{β₁_i\}_{i \in I}$ and $\{β₂_i\}_{i \in I}$ be families of additive commutative groups indexed by a set $I$. Given a family of additive group homomorphisms $f_i \colon β₂_i \to β₁_i$ for each $i \in I$, the range of the induced additive group homomorphism $\text{mapRange.addMonoidHom}\, f \colon (\Pi_{i} β₂_i) \to (\Pi_{i} β₁_i)$ is equal to the preimage under the coefficient function homomorphism of the product of the ranges of the individual $f_i$ homomorphisms over all indices. That is, \[ \text{range}(\text{mapRange.addMonoidHom}\, f) = \left(\prod_{i \in I} \text{range}(f_i)\right) \cap \left(\Pi_{i \in I} β₁_i\right)_{\text{fin}}, \] where $(\Pi_{i \in I} β₁_i)_{\text{fin}}$ denotes the space of dependent functions with finite support.

DFinsupp.coprodMap definition

(f : ∀ i : ι, M i →ₗ[R] N) : (Π₀ i, M i) →ₗ[R] N

Full source

/-- Given a family of linear maps `f i : M i →ₗ[R] N`, we can form a linear map
`(Π₀ i, M i) →ₗ[R] N` which sends `x : Π₀ i, M i` to the sum over `i` of `f i` applied to `x i`.
This is the map coming from the universal property of `Π₀ i, M i` as the coproduct of the `M i`.
See also `LinearMap.coprod` for the binary product version. -/
def coprodMap (f : ∀ i : ι, M i →ₗ[R] N) : (Π₀ i, M i) →ₗ[R] N :=
  (DFinsupp.lsum ℕ fun _ : ι => LinearMap.id) ∘ₗ DFinsupp.mapRange.linearMap f

Linear coproduct map of dependent functions with finite support

Informal description

Given a family of $R$-linear maps $f_i \colon M_i \to N$ for each index $i$, the linear map $\text{coprodMap}\, f \colon (\Pi₀ i, M_i) \to N$ is defined as the composition of the linear summation map $\text{DFinsupp.lsum}$ with the pointwise application of the family $f$. More explicitly, for any dependent function $x \in \Pi₀ i, M_i$ with finite support, $\text{coprodMap}\, f\, x$ computes the sum $\sum_{i} f_i (x_i)$, where the sum is taken over the support of $x$. This construction satisfies the following properties: 1. For any $i \in \iota$ and $x \in M_i$, $\text{coprodMap}\, f\, (\text{single}\, i\, x) = f_i x$. 2. The map $\text{coprodMap}\, f$ is $R$-linear, meaning it preserves addition and scalar multiplication.

DFinsupp.coprodMap_apply theorem

 [∀ x : N, Decidable (x ≠ 0)] (f : ∀ i : ι, M i →ₗ[R] N) (x : Π₀ i, M i) :
  coprodMap f x = DFinsupp.sum (mapRange (fun i => f i) (fun _ => LinearMap.map_zero _) x) fun _ => id

Full source

theorem coprodMap_apply [∀ x : N, Decidable (x ≠ 0)] (f : ∀ i : ι, M i →ₗ[R] N) (x : Π₀ i, M i) :
    coprodMap f x =
      DFinsupp.sum (mapRange (fun i => f i) (fun _ => LinearMap.map_zero _) x) fun _ =>
        id :=
  DFinsupp.sumAddHom_apply _ _

Coproduct Map Evaluation for Dependent Functions with Finite Support

Informal description

Let $N$ be an $R$-module with decidable support (i.e., for any $x \in N$, it is decidable whether $x \neq 0$). Given a family of $R$-linear maps $f_i \colon M_i \to N$ for each index $i \in \iota$ and a dependent function $x \in \Pi_{i} M_i$ with finite support, the coproduct map $\text{coprodMap}\, f$ applied to $x$ is equal to the sum of the values $f_i(x_i)$ over all indices $i$ in the support of $x$. More precisely, we have: \[ \text{coprodMap}\, f\, x = \sum_{i \in \text{supp}(x)} f_i(x_i). \]

DFinsupp.coprodMap_apply_single theorem

(f : ∀ i : ι, M i →ₗ[R] N) (i : ι) (x : M i) : coprodMap f (single i x) = f i x

Full source

theorem coprodMap_apply_single (f : ∀ i : ι, M i →ₗ[R] N) (i : ι) (x : M i) :
    coprodMap f (single i x) = f i x := by
  simp [coprodMap]

Evaluation of Linear Coproduct Map on Single-Element Function: $\text{coprodMap}\, f\, (\text{single}_i(x)) = f_i(x)$

Informal description

Given a family of $R$-linear maps $f_i \colon M_i \to N$ for each index $i \in \iota$, the linear coproduct map $\text{coprodMap}\, f$ evaluated at the single-element function $\text{single}_i(x)$ equals $f_i(x)$, i.e., \[ \text{coprodMap}\, f\, (\text{single}_i(x)) = f_i(x). \]

Submodule.dfinsuppSum_mem theorem

 {β : ι → Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)] (S : Submodule R N) (f : Π₀ i, β i)
  (g : ∀ i, β i → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : f.sum g ∈ S

Full source

theorem dfinsuppSum_mem {β : ι → Type*} [∀ i, Zero (β i)] [∀ (i) (x : β i), Decidable (x ≠ 0)]
    (S : Submodule R N) (f : Π₀ i, β i) (g : ∀ i, β i → N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) :
    f.sum g ∈ S :=
  _root_.dfinsuppSum_mem S f g h

Sum of Dependent Functions Preserves Submodule Membership

Informal description

Let $R$ be a ring, $N$ an $R$-module, and $\beta : \iota \to \text{Type}^*$ a family of types each with a zero element and decidable non-zero condition. For any submodule $S$ of $N$, a dependent function $f \in \Pi₀ i, \beta i$ with finite support, and a family of functions $g_i : \beta i \to N$, if for every index $c$ with $f c \neq 0$ we have $g_c (f c) \in S$, then the sum $\sum_{i} g_i (f i)$ belongs to $S$.

Submodule.dfinsuppSumAddHom_mem theorem

 {β : ι → Type*} [∀ i, AddZeroClass (β i)] (S : Submodule R N) (f : Π₀ i, β i) (g : ∀ i, β i →+ N)
  (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) : DFinsupp.sumAddHom g f ∈ S

Full source

theorem dfinsuppSumAddHom_mem {β : ι → Type*} [∀ i, AddZeroClass (β i)] (S : Submodule R N)
    (f : Π₀ i, β i) (g : ∀ i, β i →+ N) (h : ∀ c, f c ≠ 0 → g c (f c) ∈ S) :
    DFinsupp.sumAddHomDFinsupp.sumAddHom g f ∈ S :=
  _root_.dfinsuppSumAddHom_mem S f g h

Submodule Membership Preservation under Summation of Additive Homomorphisms over Finite Support

Informal description

Let $R$ be a ring, $N$ an $R$-module, and $\{\beta_i\}_{i \in \iota}$ a family of types each equipped with an additive zero class structure. Given a submodule $S$ of $N$, a finitely supported dependent function $f \in \Pi_{i \in \iota} \beta_i$, and a family of additive monoid homomorphisms $g_i \colon \beta_i \to N$, if for every index $c$ where $f_c \neq 0$ we have $g_c(f_c) \in S$, then the sum $\sum_{i} g_i(f_i)$ belongs to $S$.

Submodule.iSup_eq_range_dfinsupp_lsum theorem

(p : ι → Submodule R N) : iSup p = LinearMap.range (DFinsupp.lsum ℕ fun i => (p i).subtype)

Full source

/-- The supremum of a family of submodules is equal to the range of `DFinsupp.lsum`; that is
every element in the `iSup` can be produced from taking a finite number of non-zero elements
of `p i`, coercing them to `N`, and summing them. -/
theorem iSup_eq_range_dfinsupp_lsum (p : ι → Submodule R N) :
    iSup p = LinearMap.range (DFinsupp.lsum ℕ fun i => (p i).subtype) := by
  apply le_antisymm
  · apply iSup_le _
    intro i y hy
    simp only [LinearMap.mem_range, lsum_apply_apply]
    exact ⟨DFinsupp.single i ⟨y, hy⟩, DFinsupp.sumAddHom_single _ _ _⟩
  · rintro x ⟨v, rfl⟩
    exact dfinsuppSumAddHom_mem _ v _ fun i _ => (le_iSup p i : p i ≤ _) (v i).2

Supremum of Submodules as Range of Linear Summation Map

Informal description

Let $R$ be a ring and $N$ an $R$-module. Given a family of submodules $(p_i)_{i \in \iota}$ of $N$, the supremum $\bigsqcup_{i \in \iota} p_i$ is equal to the range of the linear map $\operatorname{DFinsupp.lsum}$ applied to the family of inclusion maps $(p_i \hookrightarrow N)_{i \in \iota}$. In other words, every element in the supremum of the submodules $p_i$ can be expressed as a finite sum of elements from the $p_i$'s, where each summand comes from a different $p_i$ via its inclusion map.

Submodule.biSup_eq_range_dfinsupp_lsum theorem

 (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) :
  ⨆ (i) (_ : p i), S i =
    LinearMap.range (LinearMap.comp (DFinsupp.lsum ℕ (fun i => (S i).subtype)) (DFinsupp.filterLinearMap R _ p))

Full source

/-- The bounded supremum of a family of commutative additive submonoids is equal to the range of
`DFinsupp.sumAddHom` composed with `DFinsupp.filter_add_monoid_hom`; that is, every element in the
bounded `iSup` can be produced from taking a finite number of non-zero elements from the `S i` that
satisfy `p i`, coercing them to `γ`, and summing them. -/
theorem biSup_eq_range_dfinsupp_lsum (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) :
    ⨆ (i) (_ : p i), S i =
      LinearMap.range
        (LinearMap.comp
          (DFinsupp.lsum ℕ (fun i => (S i).subtype))
            (DFinsupp.filterLinearMap R _ p)) := by
  apply le_antisymm
  · refine iSup₂_le fun i hi y hy => ⟨DFinsupp.single i ⟨y, hy⟩, ?_⟩
    rw [LinearMap.comp_apply, filterLinearMap_apply, filter_single_pos _ _ hi]
    simp only [lsum_apply_apply, sumAddHom_single, LinearMap.toAddMonoidHom_coe, coe_subtype]
  · rintro x ⟨v, rfl⟩
    refine dfinsuppSumAddHom_mem _ _ _ fun i _ => ?_
    refine mem_iSup_of_mem i ?_
    by_cases hp : p i
    · simp [hp]
    · simp [hp]

Bounded Supremum of Submodules as Range of Filtered Linear Summation

Informal description

Let $R$ be a ring, $N$ an $R$-module, and $p : \iota \to \text{Prop}$ a decidable predicate on the index set $\iota$. Given a family of submodules $S_i \subseteq N$ indexed by $\iota$, the bounded supremum $\bigsqcup_{i \in \iota, p(i)} S_i$ is equal to the range of the linear map obtained by composing: 1. The linear summation map $\text{DFinsupp.lsum}$ applied to the family of inclusion maps $(S_i).\text{subtype} : S_i \to N$, and 2. The linear filter map $\text{DFinsupp.filterLinearMap}$ for the predicate $p$. In other words, the bounded supremum of submodules consists exactly of all elements in $N$ that can be expressed as finite sums of elements from those $S_i$ where $p(i)$ holds.

Submodule.mem_iSup_iff_exists_dfinsupp theorem

 (p : ι → Submodule R N) (x : N) : x ∈ iSup p ↔ ∃ f : Π₀ i, p i, DFinsupp.lsum ℕ (fun i => (p i).subtype) f = x

Full source

/-- A characterisation of the span of a family of submodules.

See also `Submodule.mem_iSup_iff_exists_finsupp`. -/
theorem mem_iSup_iff_exists_dfinsupp (p : ι → Submodule R N) (x : N) :
    x ∈ iSup px ∈ iSup p ↔
      ∃ f : Π₀ i, p i, DFinsupp.lsum ℕ (fun i => (p i).subtype) f = x :=
  SetLike.ext_iff.mp (iSup_eq_range_dfinsupp_lsum p) x

Characterization of Supremum Membership via Finite Sums of Submodules

Informal description

Let $R$ be a ring and $N$ an $R$-module. Given a family of submodules $(p_i)_{i \in \iota}$ of $N$, an element $x \in N$ belongs to the supremum $\bigsqcup_{i \in \iota} p_i$ if and only if there exists a dependent function with finite support $f \in \Pi₀ i, p_i$ such that the linear summation of the inclusion maps $(p_i \hookrightarrow N)_{i \in \iota}$ applied to $f$ equals $x$. In other words, $x$ is in the span of the submodules $p_i$ if and only if it can be expressed as a finite sum of elements from the $p_i$'s.

Submodule.mem_iSup_iff_exists_dfinsupp' theorem

 (p : ι → Submodule R N) [∀ (i) (x : p i), Decidable (x ≠ 0)] (x : N) :
  x ∈ iSup p ↔ ∃ f : Π₀ i, p i, (f.sum fun _ xi => ↑xi) = x

Full source

/-- A variant of `Submodule.mem_iSup_iff_exists_dfinsupp` with the RHS fully unfolded.

See also `Submodule.mem_iSup_iff_exists_finsupp`. -/
theorem mem_iSup_iff_exists_dfinsupp' (p : ι → Submodule R N) [∀ (i) (x : p i), Decidable (x ≠ 0)]
    (x : N) : x ∈ iSup px ∈ iSup p ↔ ∃ f : Π₀ i, p i, (f.sum fun _ xi => ↑xi) = x := by
  rw [mem_iSup_iff_exists_dfinsupp]
  simp_rw [DFinsupp.lsum_apply_apply, DFinsupp.sumAddHom_apply,
    LinearMap.toAddMonoidHom_coe, coe_subtype]

Characterization of Supremum Membership via Finite Sums of Submodules (Decidable Zero Version)

Informal description

Let $R$ be a ring and $N$ an $R$-module. Given a family of submodules $(p_i)_{i \in \iota}$ of $N$ where for each $i$ and $x \in p_i$ it is decidable whether $x \neq 0$, an element $x \in N$ belongs to the supremum $\bigsqcup_{i \in \iota} p_i$ if and only if there exists a dependent function with finite support $f \in \Pi₀ i, p_i$ such that the sum of the projections $\sum_{i} f(i) = x$.

Submodule.mem_biSup_iff_exists_dfinsupp theorem

 (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) (x : N) :
  (x ∈ ⨆ (i) (_ : p i), S i) ↔ ∃ f : Π₀ i, S i, DFinsupp.lsum ℕ (fun i => (S i).subtype) (f.filter p) = x

Full source

theorem mem_biSup_iff_exists_dfinsupp (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N)
    (x : N) :
    (x ∈ ⨆ (i) (_ : p i), S i) ↔
      ∃ f : Π₀ i, S i,
        DFinsupp.lsum ℕ (fun i => (S i).subtype) (f.filter p) = x :=
  SetLike.ext_iff.mp (biSup_eq_range_dfinsupp_lsum p S) x

Characterization of Bounded Supremum Membership via Filtered Dependent Functions

Informal description

Let $R$ be a ring, $N$ an $R$-module, and $p : \iota \to \text{Prop}$ a decidable predicate on the index set $\iota$. Given a family of submodules $S_i \subseteq N$ indexed by $\iota$, an element $x \in N$ belongs to the bounded supremum $\bigsqcup_{i \in \iota, p(i)} S_i$ if and only if there exists a dependent function with finite support $f \in \Pi₀ i, S_i$ such that the linear summation of the inclusion maps $(S_i).\text{subtype}$ applied to $f$ filtered by $p$ equals $x$. More precisely, $x$ is in the bounded supremum if and only if there exists $f \in \Pi₀ i, S_i$ satisfying: \[ \text{DFinsupp.lsum } \mathbb{N} (\lambda i, (S_i).\text{subtype}) (\text{DFinsupp.filter } p \, f) = x \]

Submodule.mem_iSup_iff_exists_finsupp theorem

 (p : ι → Submodule R N) (x : N) : x ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ i, f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x

Full source

lemma mem_iSup_iff_exists_finsupp (p : ι → Submodule R N) (x : N) :
    x ∈ iSup px ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ i, f i ∈ p i) ∧ (f.sum fun _i xi ↦ xi) = x := by
  classical
  rw [mem_iSup_iff_exists_dfinsupp']
  refine ⟨fun ⟨f, hf⟩ ↦ ⟨⟨f.support, fun i ↦ (f i : N), by simp⟩, by simp, hf⟩, ?_⟩
  rintro ⟨f, hf, rfl⟩
  refine ⟨DFinsupp.mk f.support fun i ↦ ⟨f i, hf i⟩, Finset.sum_congr ?_ fun i hi ↦ ?_⟩
  · ext; simp [mk_eq_zero]
  · simp [Finsupp.mem_support_iff.mp hi]

Characterization of Supremum Membership via Finitely Supported Functions

Informal description

Let $R$ be a ring and $N$ an $R$-module. Given a family of submodules $(p_i)_{i \in \iota}$ of $N$, an element $x \in N$ belongs to the supremum $\bigsqcup_{i \in \iota} p_i$ if and only if there exists a finitely supported function $f \colon \iota \to_{\text{f}} N$ such that: 1. For each $i \in \iota$, $f(i) \in p_i$; 2. The sum $\sum_{i} f(i) = x$.

Submodule.mem_iSup_finset_iff_exists_sum theorem

 {s : Finset ι} (p : ι → Submodule R N) (a : N) : (a ∈ ⨆ i ∈ s, p i) ↔ ∃ μ : ∀ i, p i, (∑ i ∈ s, (μ i : N)) = a

Full source

theorem mem_iSup_finset_iff_exists_sum {s : Finset ι} (p : ι → Submodule R N) (a : N) :
    (a ∈ ⨆ i ∈ s, p i) ↔ ∃ μ : ∀ i, p i, (∑ i ∈ s, (μ i : N)) = a := by
  classical
    rw [Submodule.mem_iSup_iff_exists_dfinsupp']
    constructor <;> rintro ⟨μ, hμ⟩
    · use fun i => ⟨μ i, (iSup_const_le : _ ≤ p i) (coe_mem <| μ i)⟩
      rw [← hμ]
      symm
      apply Finset.sum_subset
      · intro x
        contrapose
        intro hx
        rw [mem_support_iff, not_ne_iff]
        ext
        rw [coe_zero, ← mem_bot R]
        suffices ⊥ = ⨆ (_ : x ∈ s), p x from this.symm ▸ coe_mem (μ x)
        exact (iSup_neg hx).symm
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl
    · refine ⟨DFinsupp.mk s ?_, ?_⟩
      · rintro ⟨i, hi⟩
        refine ⟨μ i, ?_⟩
        rw [iSup_pos]
        · exact coe_mem _
        · exact hi
      simp only [DFinsupp.sum]
      rw [Finset.sum_subset support_mk_subset, ← hμ]
      · exact Finset.sum_congr rfl fun x hx => by rw [mk_of_mem hx]
      · intro x _ hx
        rw [mem_support_iff, not_ne_iff] at hx
        rw [hx]
        rfl

Characterization of Supremum Membership via Finite Sums over a Finite Index Set

Informal description

Let $R$ be a ring and $N$ an $R$-module. Given a finite set $s$ of indices and a family of submodules $(p_i)_{i \in \iota}$ of $N$, an element $a \in N$ belongs to the supremum $\bigsqcup_{i \in s} p_i$ if and only if there exists a family of elements $\mu = (\mu_i)_{i \in \iota}$ with $\mu_i \in p_i$ for each $i$, such that the finite sum $\sum_{i \in s} \mu_i$ equals $a$.

iSupIndep_iff_forall_dfinsupp theorem

 (p : ι → Submodule R N) :
  iSupIndep p ↔ ∀ (i) (x : p i) (v : Π₀ i : ι, ↥(p i)), lsum ℕ (fun i => (p i).subtype) (erase i v) = x → x = 0

Full source

/-- Independence of a family of submodules can be expressed as a quantifier over `DFinsupp`s.

This is an intermediate result used to prove
`iSupIndep_of_dfinsupp_lsum_injective` and
`iSupIndep.dfinsupp_lsum_injective`. -/
theorem iSupIndep_iff_forall_dfinsupp (p : ι → Submodule R N) :
    iSupIndepiSupIndep p ↔
      ∀ (i) (x : p i) (v : Π₀ i : ι, ↥(p i)),
        lsum ℕ (fun i => (p i).subtype) (erase i v) = x → x = 0 := by
  simp_rw [iSupIndep_def, Submodule.disjoint_def,
    Submodule.mem_biSup_iff_exists_dfinsupp, exists_imp, filter_ne_eq_erase]
  refine forall_congr' fun i => Subtype.forall'.trans ?_
  simp_rw [Submodule.coe_eq_zero]

Supremum Independence Criterion via Dependent Functions with Finite Support

Informal description

A family of submodules $p : \iota \to \text{Submodule } R N$ is supremum independent if and only if for every index $i$, every element $x \in p_i$, and every dependent function $v \in \Pi₀ i, p_i$ with finite support, the condition that the linear sum of $v$ with its value at $i$ erased equals $x$ implies that $x = 0$. In other words, the family $p$ is supremum independent precisely when the only solution to the equation \[ \sum_{j \neq i} v_j = x \quad \text{for } x \in p_i \] is the trivial solution $x = 0$.

iSupIndep_of_dfinsupp_lsum_injective theorem

(p : ι → Submodule R N) (h : Function.Injective (lsum ℕ fun i => (p i).subtype)) : iSupIndep p

Full source

theorem iSupIndep_of_dfinsupp_lsum_injective (p : ι → Submodule R N)
    (h : Function.Injective (lsum ℕ fun i => (p i).subtype)) :
    iSupIndep p := by
  rw [iSupIndep_iff_forall_dfinsupp]
  intro i x v hv
  replace hv : lsum ℕ (fun i => (p i).subtype) (erase i v) =
      lsum ℕ (fun i => (p i).subtype) (single i x) := by
    simpa only [lsum_single] using hv
  have := DFunLike.ext_iff.mp (h hv) i
  simpa [eq_comm] using this

Supremum Independence via Injectivity of Linear Summation

Informal description

Let $R$ be a semiring and $N$ an $R$-module. Given a family of submodules $p : \iota \to \text{Submodule } R N$, if the linear summation map \[ \operatorname{lsum}_{\mathbb{N}} \left( \lambda i, (p_i).\text{subtype} \right) : \left( \Pi_{i \in \iota} p_i \right) \to N \] is injective, then the family $p$ is supremum independent.

iSupIndep_of_dfinsuppSumAddHom_injective theorem

(p : ι → AddSubmonoid N) (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p

Full source

theorem iSupIndep_of_dfinsuppSumAddHom_injective (p : ι → AddSubmonoid N)
    (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p := by
  rw [← iSupIndep_map_orderIso_iff (AddSubmonoid.toNatSubmodule : AddSubmonoidAddSubmonoid N ≃o _)]
  exact iSupIndep_of_dfinsupp_lsum_injective _ h

Supremum Independence via Injectivity of Additive Summation on Dependent Functions

Informal description

Let $N$ be an additive commutative monoid and $(p_i)_{i \in \iota}$ a family of additive submonoids of $N$. If the summation homomorphism \[ \operatorname{sumAddHom} \left( \lambda i, (p_i).\text{subtype} \right) : \left( \Pi_{i \in \iota} p_i \right) \to N \] is injective, then the family $(p_i)$ is supremum independent. That is, for each $i \in \iota$, the submonoid $p_i$ is disjoint from the supremum of the submonoids $(p_j)_{j \neq i}$.

lsum_comp_mapRange_toSpanSingleton theorem

 [∀ m : R, Decidable (m ≠ 0)] (p : ι → Submodule R N) {v : ι → N} (hv : ∀ i : ι, v i ∈ p i) :
  (lsum ℕ fun i => (p i).subtype : _ →ₗ[R] _).comp
      ((mapRange.linearMap fun i => LinearMap.toSpanSingleton R (↥(p i)) ⟨v i, hv i⟩ : _ →ₗ[R] _).comp
        (finsuppLequivDFinsupp R : (ι →₀ R) ≃ₗ[R] _).toLinearMap) =
    Finsupp.linearCombination R v

Full source

/-- Combining `DFinsupp.lsum` with `LinearMap.toSpanSingleton` is the same as
`Finsupp.linearCombination` -/
theorem lsum_comp_mapRange_toSpanSingleton [∀ m : R, Decidable (m ≠ 0)] (p : ι → Submodule R N)
    {v : ι → N} (hv : ∀ i : ι, v i ∈ p i) :
    (lsum ℕ fun i => (p i).subtype : _ →ₗ[R] _).comp
        ((mapRange.linearMap fun i => LinearMap.toSpanSingleton R (↥(p i)) ⟨v i, hv i⟩ :
              _ →ₗ[R] _).comp
          (finsuppLequivDFinsupp R : (ι →₀ R) ≃ₗ[R] _).toLinearMap) =
      Finsupp.linearCombination R v := by
  ext
  simp

Composition of Linear Maps Yields Linear Combination: $\text{lsum} \circ \text{mapRange} \circ \text{finsuppLequivDFinsupp} = \text{linearCombination}$

Informal description

Let $R$ be a semiring, $N$ an $R$-module, and $\iota$ an index type. Given a family of submodules $p_i \subseteq N$ for each $i \in \iota$, and a family of vectors $v_i \in p_i$, the composition of the following linear maps: 1. The linear equivalence `finsuppLequivDFinsupp` from finitely supported functions $\iota \to_{\text{f}} R$ to dependent functions $\Pi_{i} R$, 2. The linear map `mapRange.linearMap` applying $\text{toSpanSingleton}$ to each $v_i$, 3. The linear summation map `lsum` with the submodule inclusions, is equal to the linear combination map $\text{Finsupp.linearCombination}_R v$ that sends a finitely supported function to the corresponding linear combination of the $v_i$.

iSupIndep_of_dfinsuppSumAddHom_injective' theorem

(p : ι → AddSubgroup N) (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p

Full source

/-- If `DFinsupp.sumAddHom` applied with `AddSubmonoid.subtype` is injective then the additive
subgroups are independent. -/
theorem iSupIndep_of_dfinsuppSumAddHom_injective' (p : ι → AddSubgroup N)
    (h : Function.Injective (sumAddHom fun i => (p i).subtype)) : iSupIndep p := by
  rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroupAddSubgroup N ≃o _)]
  exact iSupIndep_of_dfinsupp_lsum_injective _ h

Supremum Independence of Additive Subgroups via Injectivity of Summation Homomorphism

Informal description

Let $N$ be an additive commutative group and $(p_i)_{i \in \iota}$ a family of additive subgroups of $N$. If the summation homomorphism \[ \sum_{i} (p_i).\text{subtype} \colon \left( \Pi_{i \in \iota} p_i \right) \to N \] is injective, then the family $(p_i)$ is supremum independent. Here, $(p_i).\text{subtype}$ denotes the inclusion map of the subgroup $p_i$ into $N$.

iSupIndep.dfinsupp_lsum_injective theorem

{p : ι → Submodule R N} (h : iSupIndep p) : Function.Injective (lsum ℕ fun i => (p i).subtype)

Full source

/-- The canonical map out of a direct sum of a family of submodules is injective when the submodules
are `iSupIndep`.

Note that this is not generally true for `[Semiring R]`, for instance when `A` is the
`ℕ`-submodules of the positive and negative integers.

See `Counterexamples/DirectSumIsInternal.lean` for a proof of this fact. -/
theorem iSupIndep.dfinsupp_lsum_injective {p : ι → Submodule R N} (h : iSupIndep p) :
    Function.Injective (lsum ℕ fun i => (p i).subtype) := by
  -- simplify everything down to binders over equalities in `N`
  rw [iSupIndep_iff_forall_dfinsupp] at h
  suffices LinearMap.ker (lsum ℕ fun i => (p i).subtype) = ⊥ by
    -- Lean can't find this without our help
    letI thisI : AddCommGroup (Π₀ i, p i) := inferInstance
    rw [LinearMap.ker_eq_bot] at this
    exact this
  rw [LinearMap.ker_eq_bot']
  intro m hm
  ext i : 1
  -- split `m` into the piece at `i` and the pieces elsewhere, to match `h`
  rw [DFinsupp.zero_apply, ← neg_eq_zero]
  refine h i (-m i) m ?_
  rwa [← erase_add_single i m, LinearMap.map_add, lsum_single, Submodule.subtype_apply,
    add_eq_zero_iff_eq_neg, ← Submodule.coe_neg] at hm

Injectivity of Linear Summation for Supremum Independent Submodules

Informal description

Let $R$ be a semiring and $N$ an $R$-module. Given a family of submodules $p : \iota \to \text{Submodule } R N$ that is supremum independent, the linear summation map \[ \operatorname{lsum}_{\mathbb{N}} \left( \lambda i, (p_i).\text{subtype} \right) : \left( \Pi_{i \in \iota} p_i \right) \to N \] is injective. Here, $(p_i).\text{subtype}$ denotes the inclusion map of the submodule $p_i$ into $N$.

iSupIndep.dfinsuppSumAddHom_injective theorem

{p : ι → AddSubgroup N} (h : iSupIndep p) : Function.Injective (sumAddHom fun i => (p i).subtype)

Full source

/-- The canonical map out of a direct sum of a family of additive subgroups is injective when the
additive subgroups are `iSupIndep`. -/
theorem iSupIndep.dfinsuppSumAddHom_injective {p : ι → AddSubgroup N} (h : iSupIndep p) :
    Function.Injective (sumAddHom fun i => (p i).subtype) := by
  rw [← iSupIndep_map_orderIso_iff (AddSubgroup.toIntSubmodule : AddSubgroupAddSubgroup N ≃o _)] at h
  exact h.dfinsupp_lsum_injective

Injectivity of Summation Homomorphism for Supremum Independent Additive Subgroups

Informal description

Let $N$ be an additive commutative group and $(p_i)_{i \in \iota}$ a family of additive subgroups of $N$ that is supremum independent. Then the summation homomorphism \[ \sum_{i \in \iota} (p_i \hookrightarrow N) : \left( \bigoplus_{i \in \iota} p_i \right) \to N \] is injective, where $(p_i \hookrightarrow N)$ denotes the inclusion map of the subgroup $p_i$ into $N$.

iSupIndep_iff_dfinsupp_lsum_injective theorem

(p : ι → Submodule R N) : iSupIndep p ↔ Function.Injective (lsum ℕ fun i => (p i).subtype)

Full source

/-- A family of submodules over an additive group are independent if and only iff `DFinsupp.lsum`
applied with `Submodule.subtype` is injective.

Note that this is not generally true for `[Semiring R]`; see
`iSupIndep.dfinsupp_lsum_injective` for details. -/
theorem iSupIndep_iff_dfinsupp_lsum_injective (p : ι → Submodule R N) :
    iSupIndepiSupIndep p ↔ Function.Injective (lsum ℕ fun i => (p i).subtype) :=
  ⟨iSupIndep.dfinsupp_lsum_injective, iSupIndep_of_dfinsupp_lsum_injective p⟩

Supremum Independence of Submodules is Equivalent to Injectivity of Linear Summation

Informal description

For a family of submodules $p : \iota \to \text{Submodule } R N$ of an $R$-module $N$, the following are equivalent: 1. The family $p$ is supremum independent (i.e., for each $i$, $p_i$ is disjoint from the supremum of the other submodules). 2. The linear summation map \[ \operatorname{lsum}_{\mathbb{N}} \left( \lambda i, (p_i).\text{subtype} \right) : \left( \Pi_{i \in \iota} p_i \right) \to N \] is injective, where $(p_i).\text{subtype}$ denotes the inclusion of $p_i$ into $N$.

iSupIndep_iff_dfinsuppSumAddHom_injective theorem

(p : ι → AddSubgroup N) : iSupIndep p ↔ Function.Injective (sumAddHom fun i => (p i).subtype)

Full source

/-- A family of additive subgroups over an additive group are independent if and only if
`DFinsupp.sumAddHom` applied with `AddSubgroup.subtype` is injective. -/
theorem iSupIndep_iff_dfinsuppSumAddHom_injective (p : ι → AddSubgroup N) :
    iSupIndepiSupIndep p ↔ Function.Injective (sumAddHom fun i => (p i).subtype) :=
  ⟨iSupIndep.dfinsuppSumAddHom_injective, iSupIndep_of_dfinsuppSumAddHom_injective' p⟩

Supremum Independence of Additive Subgroups is Equivalent to Injectivity of Summation Homomorphism

Informal description

Let $N$ be an additive commutative group and $(p_i)_{i \in \iota}$ a family of additive subgroups of $N$. The family $(p_i)$ is supremum independent if and only if the summation homomorphism \[ \sum_{i \in \iota} (p_i \hookrightarrow N) : \left( \bigoplus_{i \in \iota} p_i \right) \to N \] is injective, where $(p_i \hookrightarrow N)$ denotes the inclusion map of the subgroup $p_i$ into $N$.

iSupIndep.linearIndependent theorem

 [NoZeroSMulDivisors R N] {ι} (p : ι → Submodule R N) (hp : iSupIndep p) {v : ι → N} (hv : ∀ i, v i ∈ p i)
  (hv' : ∀ i, v i ≠ 0) : LinearIndependent R v

Full source

/-- If a family of submodules is independent, then a choice of nonzero vector from each submodule
forms a linearly independent family.

See also `iSupIndep.linearIndependent'`. -/
theorem iSupIndep.linearIndependent [NoZeroSMulDivisors R N] {ι} (p : ι → Submodule R N)
    (hp : iSupIndep p) {v : ι → N} (hv : ∀ i, v i ∈ p i) (hv' : ∀ i, v i ≠ 0) :
    LinearIndependent R v := by
  let _ := Classical.decEq ι
  let _ := Classical.decEq R
  rw [linearIndependent_iff]
  intro l hl
  let a :=
    DFinsupp.mapRange.linearMap (fun i => LinearMap.toSpanSingleton R (p i) ⟨v i, hv i⟩)
      l.toDFinsupp
  have ha : a = 0 := by
    apply hp.dfinsupp_lsum_injective
    rwa [← lsum_comp_mapRange_toSpanSingleton _ hv] at hl
  ext i
  apply smul_left_injective R (hv' i)
  have : l i • v i = a i := rfl
  simp only [coe_zero, Pi.zero_apply, ZeroMemClass.coe_zero, smul_eq_zero, ha] at this
  simpa

Supremum Independent Submodules Imply Linear Independence of Nonzero Vectors

Informal description

Let $R$ be a semiring and $N$ an $R$-module with no zero smul divisors. Given an index set $\iota$, a family of submodules $p_i \subseteq N$ that is supremum independent, and a family of vectors $v_i \in p_i$ with each $v_i \neq 0$, then the family $\{v_i\}_{i \in \iota}$ is linearly independent over $R$.

iSupIndep_iff_linearIndependent_of_ne_zero theorem

 [NoZeroSMulDivisors R N] {ι} {v : ι → N} (h_ne_zero : ∀ i, v i ≠ 0) :
  (iSupIndep fun i => R ∙ v i) ↔ LinearIndependent R v

Full source

theorem iSupIndep_iff_linearIndependent_of_ne_zero [NoZeroSMulDivisors R N] {ι} {v : ι → N}
    (h_ne_zero : ∀ i, v i ≠ 0) : (iSupIndep fun i => R ∙ v i) ↔ LinearIndependent R v :=
  let _ := Classical.decEq ι
  ⟨fun hv => hv.linearIndependent _ (fun i => Submodule.mem_span_singleton_self <| v i) h_ne_zero,
    fun hv => hv.iSupIndep_span_singleton⟩

Equivalence of Supremum Independence and Linear Independence for Nonzero Vectors

Informal description

Let $R$ be a semiring and $N$ an $R$-module with no zero smul divisors. Given an index set $\iota$ and a family of nonzero vectors $v_i \in N$ (i.e., $v_i \neq 0$ for all $i \in \iota$), the following are equivalent: 1. The family of cyclic submodules $\{R \cdot v_i\}_{i \in \iota}$ is supremum independent. 2. The family of vectors $\{v_i\}_{i \in \iota}$ is linearly independent over $R$.

LinearMap.coe_dfinsuppSum theorem

(t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) : ⇑(t.sum g) = t.sum fun i d => g i d

Full source

theorem coe_dfinsuppSum (t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) :
    ⇑(t.sum g) = t.sum fun i d => g i d := rfl

Coefficient-wise Sum of Linear Maps on Dependent Functions with Finite Support

Informal description

For any dependent function with finite support $t \in \Pi_{i} \gamma_i$ and any family of linear maps $g_i : \gamma_i \to \text{Hom}_R(M, M₂)$, the underlying function of the sum $\sum_i t_i g_i$ is equal to the pointwise sum $\sum_i t_i (g_i(\cdot))$.

LinearMap.dfinsuppSum_apply theorem

(t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) (b : M) : (t.sum g) b = t.sum fun i d => g i d b

Full source

@[simp]
theorem dfinsuppSum_apply (t : Π₀ i, γ i) (g : ∀ i, γ i → M →ₛₗ[σ₁₂] M₂) (b : M) :
    (t.sum g) b = t.sum fun i d => g i d b :=
  sum_apply _ _ _

Evaluation of Sum of Linear Maps on Dependent Functions with Finite Support

Informal description

For any dependent function with finite support $t \in \Pi_{i} \gamma_i$, any family of linear maps $g_i \colon \gamma_i \to \text{Hom}_R(M, M₂)$, and any element $b \in M$, the evaluation of the sum of linear maps $\sum_i t_i g_i$ at $b$ is equal to the sum $\sum_i t_i (g_i(d_i)(b))$, where $d_i$ is the value of $t$ at index $i$.

LinearMap.map_dfinsuppSumAddHom theorem

 (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ i, γ i} {g : ∀ i, γ i →+ M} :
  f (sumAddHom g t) = sumAddHom (fun i => f.toAddMonoidHom.comp (g i)) t

Full source

@[simp]
theorem map_dfinsuppSumAddHom (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ i, γ i} {g : ∀ i, γ i →+ M} :
    f (sumAddHom g t) = sumAddHom (fun i => f.toAddMonoidHom.comp (g i)) t :=
  f.toAddMonoidHom.map_dfinsuppSumAddHom _ _

Linear Map Commutes with Summation of Finitely Supported Dependent Functions

Informal description

Let $M$ and $M_2$ be modules over rings connected by a ring homomorphism $\sigma_{12}$, and let $f \colon M \to M_2$ be a $\sigma_{12}$-linear map. Given a dependent function with finite support $t \in \Pi_{i} \gamma_i$ and a family of additive monoid homomorphisms $g_i \colon \gamma_i \to M$, the following equality holds: \[ f\left(\sum_{i} g_i(t_i)\right) = \sum_{i} (f \circ g_i)(t_i). \] Here, $\sum$ denotes the summation via `DFinsupp.sumAddHom`, which sums over the support of $t$.

LinearEquiv.map_dfinsuppSumAddHom theorem

 [∀ i, AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ i, γ i) (g : ∀ i, γ i →+ M) :
  f (sumAddHom g t) = sumAddHom (fun i => f.toAddEquiv.toAddMonoidHom.comp (g i)) t

Full source

@[simp]
theorem map_dfinsuppSumAddHom [∀ i, AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ i, γ i)
    (g : ∀ i, γ i →+ M) :
    f (sumAddHom g t) = sumAddHom (fun i => f.toAddEquiv.toAddMonoidHom.comp (g i)) t :=
  f.toAddEquiv.map_dfinsuppSumAddHom _ _

Linear Equivalence Commutes with Summation of Finitely Supported Dependent Functions

Informal description

Let $M$ and $M_2$ be modules over rings connected by a ring homomorphism $\tau_{12}$, and let $f \colon M \simeq M_2$ be a $\tau_{12}$-linear equivalence. Given a dependent function with finite support $t \in \Pi_{i} \gamma_i$ (where each $\gamma_i$ is an additive zero class) and a family of additive monoid homomorphisms $g_i \colon \gamma_i \to M$, the following equality holds: \[ f\left(\sum_{i} g_i(t_i)\right) = \sum_{i} (f \circ g_i)(t_i). \] Here, $\sum$ denotes the summation via `DFinsupp.sumAddHom`, which sums over the support of $t$.

Mathlib.LinearAlgebra.DFinsupp

Implementation notes

Tags