Documentation

Mathlib.LinearAlgebra.DFinsupp

Properties of the module Π₀ i, M i #

Given an indexed collection of R-modules M i, the R-module structure on Π₀ i, M i is defined in Data.DFinsupp.

In this file we define LinearMap versions of various maps:

Implementation notes #

This file should try to mirror LinearAlgebra.Finsupp where possible. The API of Finsupp is much more developed, but many lemmas in that file should be eligible to copy over.

Tags #

function with finite support, module, linear algebra

source
def DFinsupp.lmk {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (s : Finset ι) :
((i : ↑↑s) → M ↑i) →ₗ[R] Π₀ (i : ι), M i

DFinsupp.mk as a LinearMap.

Equations
source
def DFinsupp.lsingle {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) :
M i →ₗ[R] Π₀ (i : ι), M i

DFinsupp.single as a LinearMap

Equations
source
theorem DFinsupp.lhom_ext {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] ⦃φ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ ⦃ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι) (x : M i), φ (DFinsupp.single i x) = ψ (DFinsupp.single i x)) :
φ = ψ

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

source
theorem DFinsupp.lhom_ext' {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] ⦃φ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ ⦃ψ : (Π₀ (i : ι), M i) →ₗ[R] N⦄ (h : ∀ (i : ι), φ ∘ₗ DFinsupp.lsingle i = ψ ∘ₗ DFinsupp.lsingle i) :
φ = ψ

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

See note [partially-applied ext lemmas]. After apply this lemma, if M = R then it suffices to verify φ (single a 1) = ψ (single a 1).

source
def DFinsupp.lapply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) :
(Π₀ (i : ι), M i) →ₗ[R] M i

Interpret fun (f : Π₀ i, M i) ↦ f i as a linear map.

Equations
  • DFinsupp.lapply i = { toAddHom := { toFun := fun (f : Π₀ (i : ι), M i) => f i, map_add' := ⋯ }, map_smul' := ⋯ }
source
@[simp]
theorem DFinsupp.lmk_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (s : Finset ι) (x : (i : ↑↑s) → M ↑i) :
(DFinsupp.lmk s) x = DFinsupp.mk s x
source
@[simp]
theorem DFinsupp.lsingle_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [DecidableEq ι] (i : ι) (x : M i) :
(DFinsupp.lsingle i) x = DFinsupp.single i x
source
@[simp]
theorem DFinsupp.lapply_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] (i : ι) (f : Π₀ (i : ι), M i) :
(DFinsupp.lapply i) f = f i
source
instance DFinsupp.addCommMonoidOfLinearMap {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] :
AddCommMonoid (Π₀ (i : ι), M i →ₗ[R] N)

Typeclass inference can't find DFinsupp.addCommMonoid without help for this case. This instance allows it to be found where it is needed on the LHS of the colon in DFinsupp.moduleOfLinearMap.

Equations
  • DFinsupp.addCommMonoidOfLinearMap = inferInstance
source
instance DFinsupp.moduleOfLinearMap {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [Semiring S] [Module S N] [SMulCommClass R S N] :
Module S (Π₀ (i : ι), M i →ₗ[R] N)

Typeclass inference can't find DFinsupp.module without help for this case. This is needed to define DFinsupp.lsum below.

The cause seems to be an inability to unify the ∀ i, AddCommMonoid (M i →ₗ[R] N) instance that we have with the ∀ i, Zero (M i →ₗ[R] N) instance which appears as a parameter to the DFinsupp type.

Equations
  • DFinsupp.moduleOfLinearMap = DFinsupp.module
source
instance DFinsupp.instEquivLikeLinearEquiv {R : Type u_6} {S : Type u_7} [Semiring R] [Semiring S] (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (M : Type u_8) (M₂ : Type u_9) [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module S M₂] :
EquivLike (M ≃ₛₗ[σ] M₂) M M₂
Equations
source
@[simp]
theorem DFinsupp.lsum_symm_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (Π₀ (i : ι), M i) →ₗ[R] N) (i : ι) :
(LinearEquiv.symm (DFinsupp.lsum S)) F i = LinearMap.comp F (DFinsupp.lsingle i)
source
@[simp]
theorem DFinsupp.lsum_apply_apply {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (a : Π₀ (i : ι), M i) :
((DFinsupp.lsum S) F) a = (DFinsupp.sumAddHom fun (i : ι) => LinearMap.toAddMonoidHom (F i)) a
source
def DFinsupp.lsum {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [Semiring S] [Module S N] [SMulCommClass R S N] :
((i : ι) → M i →ₗ[R] N) ≃ₗ[S] (Π₀ (i : ι), M i) →ₗ[R] N

The DFinsupp version of Finsupp.lsum.

See note [bundled maps over different rings] for why separate R and S semirings are used.

Equations
  • One or more equations did not get rendered due to their size.
source
theorem DFinsupp.lsum_single {ι : Type u_1} {R : Type u_2} (S : Type u_3) {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [Semiring S] [Module S N] [SMulCommClass R S N] (F : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i) :
((DFinsupp.lsum S) F) (DFinsupp.single i x) = (F i) x

While simp can prove this, it is often convenient to avoid unfolding lsum into sumAddHom with DFinsupp.lsum_apply_apply.

Bundled versions of DFinsupp.mapRange #

The names should match the equivalent bundled Finsupp.mapRange definitions.

source
theorem DFinsupp.mapRange_smul {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (r : R) (hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x) (g : Π₀ (i : ι), β₁ i) :
DFinsupp.mapRange f hf (r • g) = r • DFinsupp.mapRange f hf g
source
@[simp]
theorem DFinsupp.mapRange.linearMap_apply {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) :
(DFinsupp.mapRange.linearMap f) x = DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (f i) x) ⋯ x
source
def DFinsupp.mapRange.linearMap {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) :
(Π₀ (i : ι), β₁ i) →ₗ[R] Π₀ (i : ι), β₂ i

DFinsupp.mapRange as a LinearMap.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem DFinsupp.mapRange.linearMap_id {ι : Type u_1} {R : Type u_2} [Semiring R] {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₂ i)] :
(DFinsupp.mapRange.linearMap fun (i : ι) => LinearMap.id) = LinearMap.id
source
theorem DFinsupp.mapRange.linearMap_comp {ι : Type u_1} {R : Type u_2} [Semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β₁ i →ₗ[R] β₂ i) (f₂ : (i : ι) → β i →ₗ[R] β₁ i) :
(DFinsupp.mapRange.linearMap fun (i : ι) => f i ∘ₗ f₂ i) = DFinsupp.mapRange.linearMap f ∘ₗ DFinsupp.mapRange.linearMap f₂
source
theorem DFinsupp.sum_mapRange_index.linearMap {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] [DecidableEq ι] {f : (i : ι) → β₁ i →ₗ[R] β₂ i} {h : (i : ι) → β₂ i →ₗ[R] N} {l : Π₀ (i : ι), β₁ i} :
((DFinsupp.lsum ℕ) h) ((DFinsupp.mapRange.linearMap f) l) = ((DFinsupp.lsum ℕ) fun (i : ι) => h i ∘ₗ f i) l
source
@[simp]
theorem DFinsupp.mapRange.linearEquiv_apply {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) (x : Π₀ (i : ι), β₁ i) :
(DFinsupp.mapRange.linearEquiv e) x = DFinsupp.mapRange (fun (i : ι) (x : β₁ i) => (e i) x) ⋯ x
source
def DFinsupp.mapRange.linearEquiv {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) :
(Π₀ (i : ι), β₁ i) ≃ₗ[R] Π₀ (i : ι), β₂ i

DFinsupp.mapRange.linearMap as a LinearEquiv.

Equations
  • One or more equations did not get rendered due to their size.
source
@[simp]
theorem DFinsupp.mapRange.linearEquiv_refl {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → Module R (β₁ i)] :
(DFinsupp.mapRange.linearEquiv fun (i : ι) => LinearEquiv.refl R (β₁ i)) = LinearEquiv.refl R (Π₀ (i : ι), β₁ i)
source
theorem DFinsupp.mapRange.linearEquiv_trans {ι : Type u_1} {R : Type u_2} [Semiring R] {β : ι → Type u_6} {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β i)] [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (f : (i : ι) → β i ≃ₗ[R] β₁ i) (f₂ : (i : ι) → β₁ i ≃ₗ[R] β₂ i) :
(DFinsupp.mapRange.linearEquiv fun (i : ι) => f i ≪≫ₗ f₂ i) = DFinsupp.mapRange.linearEquiv f ≪≫ₗ DFinsupp.mapRange.linearEquiv f₂
source
@[simp]
theorem DFinsupp.mapRange.linearEquiv_symm {ι : Type u_1} {R : Type u_2} [Semiring R] {β₁ : ι → Type u_7} {β₂ : ι → Type u_8} [(i : ι) → AddCommMonoid (β₁ i)] [(i : ι) → AddCommMonoid (β₂ i)] [(i : ι) → Module R (β₁ i)] [(i : ι) → Module R (β₂ i)] (e : (i : ι) → β₁ i ≃ₗ[R] β₂ i) :
LinearEquiv.symm (DFinsupp.mapRange.linearEquiv e) = DFinsupp.mapRange.linearEquiv fun (i : ι) => LinearEquiv.symm (e i)
source
def DFinsupp.coprodMap {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N) :
(Π₀ (i : ι), M i) →ₗ[R] N

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.

Equations
source
theorem DFinsupp.coprodMap_apply {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] [(x : N) → Decidable (x ≠ 0)] (f : (i : ι) → M i →ₗ[R] N) (x : Π₀ (i : ι), M i) :
(DFinsupp.coprodMap f) x = DFinsupp.sum (DFinsupp.mapRange (fun (i : ι) => ⇑(f i)) ⋯ x) fun (x : ι) => id
source
theorem DFinsupp.coprodMap_apply_single {ι : Type u_1} {R : Type u_2} {M : ι → Type u_4} {N : Type u_5} [Semiring R] [(i : ι) → AddCommMonoid (M i)] [(i : ι) → Module R (M i)] [AddCommMonoid N] [Module R N] [DecidableEq ι] (f : (i : ι) → M i →ₗ[R] N) (i : ι) (x : M i) :
(DFinsupp.coprodMap f) (DFinsupp.single i x) = (f i) x
source
theorem Submodule.dfinsupp_sum_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → Type u_6} [(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) :
DFinsupp.sum f g ∈ S
source
theorem Submodule.dfinsupp_sumAddHom_mem {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] {β : ι → Type u_6} [(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
source
theorem Submodule.iSup_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Submodule R N) :
iSup p = LinearMap.range ((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (p i))

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.

source
theorem Submodule.biSup_eq_range_dfinsupp_lsum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) :
⨆ (i : ι), ⨆ (_ : p i), S i = LinearMap.range (((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (S i)) ∘ₗ DFinsupp.filterLinearMap R (fun (i : ι) => ↥(S i)) p)

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.

source
theorem Submodule.mem_iSup_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Submodule R N) (x : N) :
x ∈ iSup p ↔ ∃ (f : Π₀ (i : ι), ↥(p i)), ((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (p i)) f = x

A characterisation of the span of a family of submodules.

See also Submodule.mem_iSup_iff_exists_finsupp.

source
theorem Submodule.mem_iSup_iff_exists_dfinsupp' {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Submodule R N) [(i : ι) → (x : ↥(p i)) → Decidable (x ≠ 0)] (x : N) :
x ∈ iSup p ↔ ∃ (f : Π₀ (i : ι), ↥(p i)), (DFinsupp.sum f fun (i : ι) (xi : ↥(p i)) => ↑xi) = x

A variant of Submodule.mem_iSup_iff_exists_dfinsupp with the RHS fully unfolded.

See also Submodule.mem_iSup_iff_exists_finsupp.

source
theorem Submodule.mem_biSup_iff_exists_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] [DecidableEq ι] (p : ι → Prop) [DecidablePred p] (S : ι → Submodule R N) (x : N) :
x ∈ ⨆ (i : ι), ⨆ (_ : p i), S i ↔ ∃ (f : Π₀ (i : ι), ↥(S i)), ((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (S i)) (DFinsupp.filter p f) = x
source
theorem Submodule.mem_iSup_iff_exists_finsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) (x : N) :
x ∈ iSup p ↔ ∃ (f : ι →₀ N), (∀ (i : ι), f i ∈ p i) ∧ (Finsupp.sum f fun (_i : ι) (xi : N) => xi) = x
source
theorem Submodule.mem_iSup_finset_iff_exists_sum {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Semiring R] [AddCommMonoid N] [Module R N] {s : Finset ι} (p : ι → Submodule R N) (a : N) :
a ∈ ⨆ i ∈ s, p i ↔ ∃ (μ : (i : ι) → ↥(p i)), (Finset.sum s fun (i : ι) => ↑(μ i)) = a
source
theorem CompleteLattice.independent_iff_forall_dfinsupp {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) :
CompleteLattice.Independent p ↔ ∀ (i : ι) (x : ↥(p i)) (v : Π₀ (i : ι), ↥(p i)), ((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (p i)) (DFinsupp.erase i v) = ↑x → x = 0

Independence of a family of submodules can be expressed as a quantifier over DFinsupps.

This is an intermediate result used to prove CompleteLattice.independent_of_dfinsupp_lsum_injective and CompleteLattice.Independent.dfinsupp_lsum_injective.

source
theorem CompleteLattice.independent_of_dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] (p : ι → Submodule R N) (h : Function.Injective ⇑((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (p i))) :
CompleteLattice.Independent p
source
theorem CompleteLattice.independent_of_dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommMonoid N] (p : ι → AddSubmonoid N) (h : Function.Injective ⇑(DFinsupp.sumAddHom fun (i : ι) => AddSubmonoid.subtype (p i))) :
CompleteLattice.Independent p
source
theorem CompleteLattice.lsum_comp_mapRange_toSpanSingleton {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Semiring R] [AddCommMonoid N] [Module R N] [(m : R) → Decidable (m ≠ 0)] (p : ι → Submodule R N) {v : ι → N} (hv : ∀ (i : ι), v i ∈ p i) :
((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (p i)) ∘ₗ (DFinsupp.mapRange.linearMap fun (i : ι) => LinearMap.toSpanSingleton R ↥(p i) { val := v i, property := ⋯ }) ∘ₗ ↑(finsuppLequivDFinsupp R) = Finsupp.total ι N R v

Combining DFinsupp.lsum with LinearMap.toSpanSingleton is the same as Finsupp.total

source
theorem CompleteLattice.independent_of_dfinsupp_sumAddHom_injective' {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) (h : Function.Injective ⇑(DFinsupp.sumAddHom fun (i : ι) => AddSubgroup.subtype (p i))) :
CompleteLattice.Independent p
source
theorem CompleteLattice.Independent.dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] {p : ι → Submodule R N} (h : CompleteLattice.Independent p) :
Function.Injective ⇑((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (p i))

The canonical map out of a direct sum of a family of submodules is injective when the submodules are CompleteLattice.Independent.

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.

source
theorem CompleteLattice.Independent.dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] {p : ι → AddSubgroup N} (h : CompleteLattice.Independent p) :
Function.Injective ⇑(DFinsupp.sumAddHom fun (i : ι) => AddSubgroup.subtype (p i))

The canonical map out of a direct sum of a family of additive subgroups is injective when the additive subgroups are CompleteLattice.Independent.

source
theorem CompleteLattice.independent_iff_dfinsupp_lsum_injective {ι : Type u_1} {R : Type u_2} {N : Type u_5} [DecidableEq ι] [Ring R] [AddCommGroup N] [Module R N] (p : ι → Submodule R N) :
CompleteLattice.Independent p ↔ Function.Injective ⇑((DFinsupp.lsum ℕ) fun (i : ι) => Submodule.subtype (p i))

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 CompleteLattice.Independent.dfinsupp_lsum_injective for details.

source
theorem CompleteLattice.independent_iff_dfinsupp_sumAddHom_injective {ι : Type u_1} {N : Type u_5} [DecidableEq ι] [AddCommGroup N] (p : ι → AddSubgroup N) :
CompleteLattice.Independent p ↔ Function.Injective ⇑(DFinsupp.sumAddHom fun (i : ι) => AddSubgroup.subtype (p i))

A family of additive subgroups over an additive group are independent if and only if DFinsupp.sumAddHom applied with AddSubgroup.subtype is injective.

source
theorem CompleteLattice.Independent.linearIndependent {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] (p : ι → Submodule R N) (hp : CompleteLattice.Independent p) {v : ι → N} (hv : ∀ (i : ι), v i ∈ p i) (hv' : ∀ (i : ι), v i ≠ 0) :
LinearIndependent R v

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

See also CompleteLattice.Independent.linearIndependent'.

source
theorem CompleteLattice.independent_iff_linearIndependent_of_ne_zero {ι : Type u_1} {R : Type u_2} {N : Type u_5} [Ring R] [AddCommGroup N] [Module R N] [NoZeroSMulDivisors R N] {v : ι → N} (h_ne_zero : ∀ (i : ι), v i ≠ 0) :
(CompleteLattice.Independent fun (i : ι) => Submodule.span R {v i}) ↔ LinearIndependent R v
source
theorem LinearMap.coe_dfinsupp_sum {R : Type u_6} {R₂ : Type u_8} {M : Type u_14} {M₂ : Type u_17} {ι : Type u_22} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_25} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂) :
⇑(DFinsupp.sum t g) = ⇑(DFinsupp.sum t fun (i : ι) (d : γ i) => g i d)
source
@[simp]
theorem LinearMap.dfinsupp_sum_apply {R : Type u_6} {R₂ : Type u_8} {M : Type u_14} {M₂ : Type u_17} {ι : Type u_22} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_25} [DecidableEq ι] [(i : ι) → Zero (γ i)] [(i : ι) → (x : γ i) → Decidable (x ≠ 0)] (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i → M →ₛₗ[σ₁₂] M₂) (b : M) :
(DFinsupp.sum t g) b = DFinsupp.sum t fun (i : ι) (d : γ i) => (g i d) b
source
@[simp]
theorem LinearMap.map_dfinsupp_sumAddHom {R : Type u_6} {R₂ : Type u_8} {M : Type u_14} {M₂ : Type u_17} {ι : Type u_22} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] {σ₁₂ : R →+* R₂} [Module R M] [Module R₂ M₂] {γ : ι → Type u_25} [DecidableEq ι] [(i : ι) → AddZeroClass (γ i)] (f : M →ₛₗ[σ₁₂] M₂) {t : Π₀ (i : ι), γ i} {g : (i : ι) → γ i →+ M} :
f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun (i : ι) => AddMonoidHom.comp (LinearMap.toAddMonoidHom f) (g i)) t
source
@[simp]
theorem LinearEquiv.map_dfinsupp_sumAddHom {R : Type u_6} {R₂ : Type u_7} {M : Type u_8} {M₂ : Type u_9} {ι : Type u_10} [Semiring R] [Semiring R₂] [AddCommMonoid M] [AddCommMonoid M₂] [Module R M] [Module R₂ M₂] {τ₁₂ : R →+* R₂} {τ₂₁ : R₂ →+* R} [RingHomInvPair τ₁₂ τ₂₁] [RingHomInvPair τ₂₁ τ₁₂] {γ : ι → Type u_11} [DecidableEq ι] [(i : ι) → AddZeroClass (γ i)] (f : M ≃ₛₗ[τ₁₂] M₂) (t : Π₀ (i : ι), γ i) (g : (i : ι) → γ i →+ M) :
f ((DFinsupp.sumAddHom g) t) = (DFinsupp.sumAddHom fun (i : ι) => AddMonoidHom.comp (AddEquiv.toAddMonoidHom (LinearEquiv.toAddEquiv f)) (g i)) t