DFinsupp.add_apply
theorem DFinsupp.add_apply :
∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Π₀ (i : ι), β i) (i : ι),
(g₁ + g₂) i = g₁ i + g₂ i
This theorem states that for any type `ι`, a type function `β` from `ι` to another type, and an instance of `AddZeroClass` for `β i` (for any `i` of type `ι`), if `g₁` and `g₂` are two functions from `ι` to `β i` (but with possibly zero values omitted, as indicated by `Π₀`), then applying the addition operation to `g₁` and `g₂` and then applying the result to some `i` gives the same result as applying `g₁` and `g₂` individually to `i` and then summing the resulting values. In other words, it's verifying the expected behavior of addition in this particular context: addition of functions is equivalent to the function of sums.
More concisely: For any type `ι`, function `β : ι →* Type,` and `AddZeroClass` instance for `β i,` if `g₁, g₂ : ι →β i` are functions, then `(∑ i : ι, g₁ i + g₂ i) = (∑ i : ι, g₁ i + β.zero + g₂ i)` where `+` denotes function addition and `+` for types denotes the sum of a list/indexed family of types.
|
AddMonoidHom.map_dfinsupp_sumAddHom
theorem AddMonoidHom.map_dfinsupp_sumAddHom :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {R : Type u_1} {S : Type u_2} [inst_1 : AddCommMonoid R]
[inst_2 : AddCommMonoid S] [inst_3 : (i : ι) → AddZeroClass (β i)] (h : R →+ S) (f : Π₀ (i : ι), β i)
(g : (i : ι) → β i →+ R), h ((DFinsupp.sumAddHom g) f) = (DFinsupp.sumAddHom fun i => h.comp (g i)) f
This theorem states that for any type `ι`, a function `β` from `ι` to another type, a type `R` with addition and commutativity, a type `S` with addition and commutativity, a function `h` that is an additive monoid homomorphism from `R` to `S`, a function `f` from a partially defined function (`DFinsupp`) from `ι` to `β i`, and a function `g` that for each `ι` maps `β i` to `R` through an additive monoid homomorphism, the composition of `h` with the sum (respecting the additive structure) of the partially defined function `f` through `g` is equal to the sum (respecting the additive structure) of `f` through the composition of `h` and `g`. This means that the sum and composition operations involved here are interchangeable, a property often known in mathematics as "commutativity".
More concisely: For any additive monoid homomorphisms h: R → S, functions f: ι → β with values in a type endowed with an additive structure, and g: β → R, the sum of the function composition h ∘ g with the sum of f (respecting additive structures) is equal to the sum of f through the composition h ∘ g.
|
DFinsupp.smul_apply
theorem DFinsupp.smul_apply :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : Monoid γ] [inst_1 : (i : ι) → AddMonoid (β i)]
[inst_2 : (i : ι) → DistribMulAction γ (β i)] (b : γ) (v : Π₀ (i : ι), β i) (i : ι), (b • v) i = b • v i
This theorem states that for any types `ι`, `γ`, and a type `β` which is a function of `ι`, given a monoid structure on `γ`, an add monoid structure on `β i` for each `i : ι`, and a distributive multiplication action of `γ` on `β i` for each `i : ι`, the scalar multiplication (`•`) of a value `b : γ` and a Direct Sum (`Π₀ (i : ι), β i`) applied to `i` is equal to the scalar multiplication of `b` and the function `v i`. In other words, the theorem establishes the property of scalar multiplication in the context of a Direct Sum, meaning scalar multiplication can be interchanged with application of the Direct Sum, a specific form of function application.
More concisely: For any monoid `γ` and a family `β i` of add monoids with distributive `γ`-actions, scalar multiplication by an element `b : γ` in `γ` commutes with application of the direct sum `Π₀ (i : ι), β i`: `b • (∑ i, β i) = ∑ i, b • β i`.
|
DFinsupp.sigmaUncurry_apply
theorem DFinsupp.sigmaUncurry_apply :
∀ {ι : Type u} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : (i : ι) → (j : α i) → Zero (δ i j)]
[inst_1 : (i : ι) → DecidableEq (α i)] [inst_2 : (i : ι) → (j : α i) → (x : δ i j) → Decidable (x ≠ 0)]
(f : Π₀ (i : ι) (j : α i), δ i j) (i : ι) (j : α i), f.sigmaUncurry ⟨i, j⟩ = (f i) j
The theorem `DFinsupp.sigmaUncurry_apply` states that for all types `ι`, a function `α`, a type `δ` that depends on `ι` and `α`, where each `δ` has a zero and where the equality of elements of `α` and non-zero-ness of elements of `δ` is decidable, given a generalized double finitely supported function `f` from `ι` and `α` to `δ`, and given an element of `ι` and an element of `α`, uncurrying `f` with a sigma-type `{fst := i, snd := j}` is equivalent to simply applying `f` to `i` and `j`. In simpler terms, it means that uncurrying a double finitely supported function and then applying it to a pair is the same as applying the function to each element of the pair.
More concisely: For any type ι, function α → δ, and given a generalized double finitely supported function f from ι × α to δ, uncurrying f with sigma-type {fst := i, snd := j} equals applying f to (i, j).
|
DFinsupp.sumAddHom_comp_single
theorem DFinsupp.sumAddHom_comp_single :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
[inst_2 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι),
(DFinsupp.sumAddHom f).comp (DFinsupp.singleAddHom β i) = f i
The theorem `DFinsupp.sumAddHom_comp_single` establishes an important property about the composition of additive monoid homomorphisms and direct sum finitely supported functions (DFinsupp). Given a type `ι`, a type `γ`, a function `β` from `ι` to a Type `v`, a decidable equality on `ι`, an `AddZeroClass` for each `β i`, and an `AddCommMonoid` for `γ`, for any additive monoid homomorphism `f` that maps each `β i` to `γ` and any element `i` of type `ι`, the composition of the sum of `f` (using `DFinsupp.sumAddHom`) and the single element addition homomorphism for `β` at `i` (using `DFinsupp.singleAddHom`) is the same as applying the function `f` at `i`. This asserts that `f` preserves the monoid structure under a specific composition operation involving a direct sum finitely supported function.
More concisely: Given an additive monoid homomorphism `f` and an element `i` of type `ι`, the composition of `f` with the single element addition homomorphism for `β` at `i` is equal to applying `f` directly to `i`, for any type `ι`, type `γ`, function `β : ι → Type v`, decidable equality on `ι`, `AddZeroClass` for each `β i`, and `AddCommMonoid` for `γ`.
|
DFinsupp.single_zero
theorem DFinsupp.single_zero :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] (i : ι),
DFinsupp.single i 0 = 0
This theorem states that, given a type `ι`, a type function `β : ι → Type v`, a decidable equality on `ι`, and a zero value for every `i : ι` in the codomain of `β`, for every `i : ι`, applying the `DFinsupp.single` function to `i` and `0` yields the zero function. In other words, if we create a function using `DFinsupp.single` that sends `i` to `0` and all other points to `0`, we get the zero function.
More concisely: For any type `ι`, decidable equality, type function `β : ι → Type v`, and zero value `z : ∀ i : ι, β i`, the function `DFinsupp.single i z` is equal to the zero function `0 : β i → β i`.
|
DFinsupp.ext
theorem DFinsupp.ext :
∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] {f g : Π₀ (i : ι), β i},
(∀ (i : ι), f i = g i) → f = g
This theorem, `DFinsupp.ext`, states that for any type `ι` and a function `β` mapping `ι` to another type, given the zero element for each instance of type `β i`, if we have two functions `f` and `g` from `ι` to `β i` (represented as `Π₀ (i : ι), β i`), then if for all `i` in `ι`, `f i = g i`, it follows that `f` is equal to `g`. In other words, two functions over possibly different types are equal if they produce the same output for the same input.
More concisely: If `β` is a type and `f` and `g` are functions from `ι` to `β`, then `f = g` if and only if `∀ i ∈ ι, f i = g i`.
|
DFinsupp.single_apply
theorem DFinsupp.single_apply :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {i i' : ι} {b : β i},
(DFinsupp.single i b) i' = if h : i = i' then Eq.recOn h b else 0
This theorem, `DFinsupp.single_apply`, states that for any index set `ι`, any function `β` from `ι` to types, and given a decidable equality on `ι` and a zero element for each `β i`, if `i` and `i'` are elements of `ι` and `b` is an element of `β i`, then applying the function `DFinsupp.single` on `i` and `b` and then applying the result to `i'` equals `b` if `i` equals `i'` (as asserted by hypothesis `h`) and `0` otherwise. The function `Eq.recOn` is used to ensure that `b` has the correct type in the context of the equality `i = i'`.
More concisely: For any indexed family of types `β` over a decidably equalizable index set `ι`, the application of `DFinsupp.single` on an index `i` and an element `b` of `β i` equals `b` if `i` equals `i'`, and `0` otherwise.
|
DFinsupp.comapDomain'_apply
theorem DFinsupp.comapDomain'_apply :
∀ {ι : Type u} {β : ι → Type v} {κ : Type u_1} [inst : (i : ι) → Zero (β i)] (h : κ → ι) {h' : ι → κ}
(hh' : Function.LeftInverse h' h) (f : Π₀ (i : ι), β i) (k : κ), (DFinsupp.comapDomain' h hh' f) k = f (h k)
The theorem `DFinsupp.comapDomain'_apply` states that for every function `h` from a type `κ` to a type `ι`, given an explicit left inverse `h'` of `h` (i.e., `h' ∘ h = id`), and a function `f` from ι to a type `β` that is zero at every index, the application of `DFinsupp.comapDomain' h hh' f` at any `k` in `κ` is equal to the application of `f` at `h k`. In other words, after applying the function `comapDomain'`, which modifies `f` by changing its domain using the function `h`, the value at any point `k` is the same as the original function `f` evaluated at `h k`.
More concisely: For any function `h: κ → ι`, its left inverse `h'`, and function `f: ι → β` that is zero at every index, `DFinsupp.comapDomain' h h' f k = f (h k)` for all `κ` elements `k`.
|
DFinsupp.mapRange_id
theorem DFinsupp.mapRange_id :
∀ {ι : Type u} {β₁ : ι → Type v₁} [inst : (i : ι) → Zero (β₁ i)] (h : optParam (∀ (i : ι), id 0 = 0) ⋯)
(g : Π₀ (i : ι), β₁ i), DFinsupp.mapRange (fun i => id) h g = g
This theorem, `DFinsupp.mapRange_id`, states that for all types ι and β₁ indexed by ι, and for any function `g` from ι to β₁ that takes zero as a default value, applying the identity function to the range of `g` leaves `g` unchanged. This is true under the condition that the identity function applied to zero yields zero, which is supplied as an optional parameter. Essentially, this theorem is saying that the operation of mapping the identity function over the range of `g` doesn't modify `g` itself, it's an identity operation on `g`.
More concisely: For any type ι and function g from ι to β₁ with a default value, applying the identity function to the range of g yields the same function g, under the assumption that the identity function maps 0 to 0.
|
AddSubmonoid.mem_iSup_iff_exists_dfinsupp'
theorem AddSubmonoid.mem_iSup_iff_exists_dfinsupp' :
∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] [inst_1 : AddCommMonoid γ] (S : ι → AddSubmonoid γ)
[inst_2 : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)] (x : γ), x ∈ iSup S ↔ ∃ f, (f.sum fun i xi => ↑xi) = x
This theorem, named `AddSubmonoid.mem_iSup_iff_exists_dfinsupp'`, states that for any types `ι` and `γ`, where equality is decidable in `ι` and `γ` is an additive commutative monoid, given a function `S` that maps each element of `ι` to a respective additive submonoid in `γ`, and a function that decides if each element in the codomain of `S` is non-zero, then for any element `x` of `γ`, `x` is in the indexed supremum of `S` if and only if there exists a function `f` such that the sum of the function `f` applied on each element `i` and a non-zero element `xi` in the additive submonoid `S i`, where the result of the function is lifted to `γ`, is equal to `x`.
More concisely: For any decidably equalifiable types `ι` and additive commutative monoid `γ`, given a function `S : ι → addSubmonoid γ`, and a decidable function `decide_nonzero : ∀ (i : ι), nonempty (S i), Prop`, an element `x` of `γ` belongs to the indexed supremum of `S` if and only if there exists a function `f : ι → γ` such that `sum (map f) (map (λ i, any_nonzero (S i))) = x`.
|
DFinsupp.coe_zero
theorem DFinsupp.coe_zero : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)], ⇑0 = 0
This theorem states that for any type ι and a type family β indexed by ι, if each type in the family β has a zero element, then the zero element of the direct sum of the family β, denoted by 0 (or `DFinsupp.zero`) and its interpretation as a function (obtained by applying the coercion to function, denoted by `⇑`), is also the zero function. In simpler terms, it states that the zero element of a direct sum of types with zero acts like a zero function when interpreted as a function.
More concisely: For any type family β indexed by ι, if each type in β has a zero element, then the zero element of the direct sum of β is the function with type ι → ∏{β i : ι} 0 i.
|
DFinsupp.single_left_injective
theorem DFinsupp.single_left_injective :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {b : (i : ι) → β i},
(∀ (i : ι), b i ≠ 0) → Function.Injective fun i => DFinsupp.single i (b i)
The theorem `DFinsupp.single_left_injective` states that the function `DFinsupp.single a b` is injective in its first argument `a`. In other words, if `DFinsupp.single a b = DFinsupp.single c b` then `a = c`. This applies to all types `ι` and `β`, where `β` is a function of `ι`, and for each `i : ι`, there is a zero element in the codomain of `β`. Additionally, this theorem also requires that for each `i : ι`, the function `b` applied to `i` is not the zero element. For the assertion that the function is also injective in its second argument `b`, there is a separate theorem `DFinsupp.single_injective`.
More concisely: If `DFinsupp.single a b` equals `DFinsupp.single c b` for all types `ι` and functions `β` such that for each `i : ι`, `β(i)` has a zero element and `b(i)` is not zero, then `a = c`.
|
DFinsupp.not_mem_support_iff
theorem DFinsupp.not_mem_support_iff :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
[inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} {i : ι}, i ∉ f.support ↔ f i = 0
The theorem `DFinsupp.not_mem_support_iff` states that for any types `ι` and `β`, given that `ι` has decidable equality, for every `i : ι` the type `β i` has an identified zero, and for every `i : ι` and `x : β i`, the inequality `x ≠ 0` is decidable, if we have a function `f : Π₀ (i : ι), β i` and a term `i : ι`, then `i` is not in the support of `f` (i.e., `i ∉ DFinsupp.support f`) if and only if the value of `f` at `i` is zero (i.e., `f i = 0`). The "support" of `f` is the set of indices `i` where `f i ≠ 0`.
More concisely: For any type `ι` with decidable equality and every function `f : Π₀ (i : ι), β i` over a type `β` with identified zero and decidable inequality, the index `i` is not in the support of `f` if and only if `f i` equals the identified zero.
|
DFinsupp.mem_support_iff
theorem DFinsupp.mem_support_iff :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
[inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i} {i : ι}, i ∈ f.support ↔ f i ≠ 0
The theorem `DFinsupp.mem_support_iff` states that for any types `ι` and `β` where `β` is a function of `ι`, given `ι` has decidable equality, `β i` has a zero element, and whether `β i` is not equal to zero is decidable, for any function `f` from `ι` to `β i` and any element `i` of type `ι`, `i` is in the support of `f` if and only if `f i` is not equal to zero. In other words, the element `i` is in the support set of `f` (which consists of all indices `i` such that `f i` is not zero) if and only if the function `f` at index `i` does not evaluate to zero.
More concisely: For functions from a type `ι` to a type `β` where `β` has a zero element and equality is decidable, an element `i` of `ι` is in the support of the function if and only if the function value at `i` is non-zero.
|
DFinsupp.single_eq_same
theorem DFinsupp.single_eq_same :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {i : ι} {b : β i},
(DFinsupp.single i b) i = b
The theorem `DFinsupp.single_eq_same` states that for any types `ι` and `β` with `β` being a function type over `ι`, given a decidable equality on `ι`, a zero for each `β i`, and any `i` in `ι` and `b` in `β i`, the value of the direct sum of finitely supported functions at point `i` (created by the `DFinsupp.single` function) is equal to `b`. In other words, when we create a direct sum of finitely supported functions that sends `i` to `b` and all other points to `0`, querying this function at `i` will yield `b`.
More concisely: For any types `ι` and `β`, given a decidable equality on `ι`, a zero for each `β i`, and any `i` in `ι` and `b` in `β i`, the function `DFinsupp.single ι β i b` equals the constant function from `ι` to `β` with value `b` at `i` when considered as an element of the direct sum of finitely supported functions `DFinsupp ι β`.
|
DFinsupp.single_eq_of_sigma_eq
theorem DFinsupp.single_eq_of_sigma_eq :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {i j : ι} {xi : β i}
{xj : β j}, ⟨i, xi⟩ = ⟨j, xj⟩ → DFinsupp.single i xi = DFinsupp.single j xj
This theorem states that if two sigma types are equal, then the corresponding `DFinsupp.single` functions are also equal. In particular, for any types `ι` and `β`, where `ι` has a decidable equality and `β` is a function from `ι` to some other type that has a zero element, if we have two elements `i` and `j` of type `ι` and `xi` and `xj` are their corresponding elements in the codomain of `β`, then if the sigma type `⟨i, xi⟩` is equal to `⟨j, xj⟩`, the `DFinsupp.single` function applied to `i` and `xi` is equal to the `DFinsupp.single` function applied to `j` and `xj`.
More concisely: If two sigma types `⟨_, _⟩` over a decidably equal type `ι` with a zero element, and having the same function value type, have equal elements, then their corresponding `DFinsupp.single` functions have equal values.
|
DFinsupp.zipWith_apply
theorem DFinsupp.zipWith_apply :
∀ {ι : Type u} {β : ι → Type v} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β i)]
[inst_1 : (i : ι) → Zero (β₁ i)] [inst_2 : (i : ι) → Zero (β₂ i)] (f : (i : ι) → β₁ i → β₂ i → β i)
(hf : ∀ (i : ι), f i 0 0 = 0) (g₁ : Π₀ (i : ι), β₁ i) (g₂ : Π₀ (i : ι), β₂ i) (i : ι),
(DFinsupp.zipWith f hf g₁ g₂) i = f i (g₁ i) (g₂ i)
This theorem states that for any types `ι`, `β`, `β₁`, and `β₂`, and for any functions `f : (i : ι) → β₁ i → β₂ i → β i` such that `f` maps all `0`s to `0`, and any two Direct Sum Indexed Families with zero `g₁` and `g₂` (denoted as `Π₀ (i : ι), β₁ i` and `Π₀ (i : ι), β₂ i` respectively), the value at `i` of applying `zipWith` operation on `g₁` and `g₂` with function `f` is equal to applying `f` on the values of `g₁` and `g₂` at `i`. In other words, it verifies that `zipWith` operation in the context of Direct Sum Indexed Families behaves as expected, by applying the function `f` to corresponding elements from `g₁` and `g₂`.
More concisely: For any types `ι`, `β₁`, `β₂`, and functions `f : (i : ι) → β₁ i → β₂ i → β i` preserving the zero element, the `zipWith` operation on `Π₀ (i : ι), β₁ i` and `Π₀ (i : ι), β₂ i` with `f` is equal to applying `f` to the corresponding elements.
|
DFinsupp.infinite_of_exists_right
theorem DFinsupp.infinite_of_exists_right :
∀ {ι : Type u_1} {π : ι → Type u_2} (i : ι) [inst : Infinite (π i)] [inst : (i : ι) → Zero (π i)],
Infinite (Π₀ (i : ι), π i)
This theorem, `DFinsupp.infinite_of_exists_right`, states that for any types ι and π, where π is a function from ι to another type, and given an instance of `i` from ι, if π at `i` is infinite and π at `i` can be zero, then the set of all functions from ι to π, denoted as `(Π₀ (i : ι), π i)`, is also infinite. This is essentially saying that if we have a function where at least one of its output types can take on infinitely many values, then the whole function space is infinite.
More concisely: If π: ι -> T is a function such that for some i in ι, π(i) is infinite and can be zero, then the set {f : ι -> π | ∀ i, f(i) = π(i)} of all functions from ι to π is infinite.
|
DFinsupp.mem_support_toFun
theorem DFinsupp.mem_support_toFun :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
[inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι), i ∈ f.support ↔ f i ≠ 0
The theorem `DFinsupp.mem_support_toFun` states that for any type ι, for any function `β` mapping elements of ι to some other types, given that equality is decidable on ι, and that for every `i` in ι, the type `β i` has a zero element and whether `x` (an element of `β i`) is non-zero is decidable, then for any function `f` of type `Π₀ (i : ι), β i` (a direct sum of `β i` as `i` varies over ι) and any `i` in ι, `i` is in the support of `f` if and only if `f(i)` is non-zero. In simpler terms, the theorem states that an index `i` is in the support of the direct sum function `f` if `f` at `i` is non-zero.
More concisely: For any type ι and function β from ι to types with decidable equality and for each i in ι, if β i has a decidably non-zero element, then an index i is in the support of the direct sum function f if and only if f(i) is non-zero.
|
DFinsupp.comp_liftAddHom
theorem DFinsupp.comp_liftAddHom :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] {δ : Type u_1}
[inst_1 : (i : ι) → AddZeroClass (β i)] [inst_2 : AddCommMonoid γ] [inst_3 : AddCommMonoid δ] (g : γ →+ δ)
(f : (i : ι) → β i →+ γ), g.comp (DFinsupp.liftAddHom f) = DFinsupp.liftAddHom fun a => g.comp (f a)
The theorem `DFinsupp.comp_liftAddHom` states that for any types `ι`, `γ`, `β` and `δ`, where `β` is a type function indexed by `ι`, `γ` and `δ` are additive commutative monoids, `β i` for each `i` in `ι` is an additive monoid with zero, and equality between elements of `ι` is decidable, for any additive monoid homomorphism `g` from `γ` to `δ` and any function `f` that for each `i` in `ι` gives an additive monoid homomorphism from `β i` to `γ`, the composition of `g` with the additive monoid homomorphism obtained by lifting `f` to a function from `Π₀ (i : ι), β i` to `γ` (using `DFinsupp.liftAddHom`) is the same as the additive monoid homomorphism obtained by lifting the function that for each `a` in `ι` gives the composition of `g` with `f a` (using the same `DFinsupp.liftAddHom`).
More concisely: For any additive monoid homomorphisms `g : γ → δ` and `f : ι → (β i → γ)` with `β i` additive monoids, the composition of `g` with the lifted homomorphism of `f` is equal to the lifted homomorphism of the composition of `g` and `f`.
|
DFinsupp.mapRange_apply
theorem DFinsupp.mapRange_apply :
∀ {ι : Type u} {β₁ : ι → Type v₁} {β₂ : ι → Type v₂} [inst : (i : ι) → Zero (β₁ i)] [inst_1 : (i : ι) → Zero (β₂ i)]
(f : (i : ι) → β₁ i → β₂ i) (hf : ∀ (i : ι), f i 0 = 0) (g : Π₀ (i : ι), β₁ i) (i : ι),
(DFinsupp.mapRange f hf g) i = f i (g i)
This theorem states that for any types `ι`, `β₁`, and `β₂`, and for a family of functions `f` from `β₁ i` to `β₂ i` such that `f i 0 = 0` for all `i`, and for a function `g` with domain `ι` and values in `β₁ i`, applying the `mapRange` function of the `DFinsupp` (directed finitely-supported function) structure to `f`, `hf` and `g`, and then applying the result to `i`, is the same as applying `f` at `i` to the result of applying `g` to `i`. In other words, it asserts that the `mapRange` function of `DFinsupp` respects the function application operation.
More concisely: For any types `ι`, `β₁`, and `β₂`, and functions `f: β₁ →β₂` and `g: ι → β₁` such that `f 0 = 0`, the application of `f` to `g i` is equal to the application of `mapRange f hf g` to `i`, where `hf` is the function equality witness for `f`.
|
DFinsupp.sigmaCurry_apply
theorem DFinsupp.sigmaCurry_apply :
∀ {ι : Type u} [inst : DecidableEq ι] {α : ι → Type u_2} {δ : (i : ι) → α i → Type v}
[inst_1 : (i : ι) → (j : α i) → Zero (δ i j)] (f : Π₀ (i : (x : ι) × α x), δ i.fst i.snd) (i : ι) (j : α i),
(f.sigmaCurry i) j = f ⟨i, j⟩
The theorem `DFinsupp.sigmaCurry_apply` states that for any type `ι` with decidable equality, any dependent function `α` from `ι` to some type, and any dependent function `δ` from pairs of `ι` and `α i` to some type, given the zero value of `δ i j` for any `i` in `ι` and `j` in `α i`, for any Direct Function (DFinsupp) `f` from pairs of `ι` and `α` to `δ`, and any value `i` of `ι` and `j` of `α i`, the application of `DFinsupp.sigmaCurry f` at `i` and `j` equals the application of `f` at the pair formed by `i` and `j`. In other words, the function `DFinsupp.sigmaCurry` transforms a function of pairs into a curried function.
More concisely: For any type `ι` with decidable equality, dependent functions `α : ι → Type, δ : (ι × α) → Type,` and given `δ (i, j) = 0` for all `i ∈ ι, j ∈ α i,` the curried function `DFinsupp.sigmaCurry f at (i, j) = f (i, j)` for any Dependent Function (DFinsupp) `f : (ι × α) → δ.`
|
DFinsupp.single_injective
theorem DFinsupp.single_injective :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {i : ι},
Function.Injective (DFinsupp.single i)
The theorem `DFinsupp.single_injective` states that for any type ι, a type β dependent on ι, a decision procedure for equality on ι, and a zero element for each type β i, the function `DFinsupp.single i` is injective. In other words, if ι is a type, β is a type dependent on ι, there is a way to decide if two elements of ι are equal, and each type β i has a defined zero element, then for each element i of ι, no two different inputs to the function `DFinsupp.single i` produce the same output.
More concisely: For any type ι, dependent type β, decision procedure for equality on ι, and zero elements for each β i, the function `DFinsupp.single i` maps distinct elements of ι to distinct outputs.
|
AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom
theorem AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom :
∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] (p : ι → Prop) [inst_1 : DecidablePred p]
[inst_2 : AddCommMonoid γ] (S : ι → AddSubmonoid γ),
⨆ i, ⨆ (_ : p i), S i =
AddMonoidHom.mrange
((DFinsupp.sumAddHom fun i => (S i).subtype).comp (DFinsupp.filterAddMonoidHom (fun i => ↥(S i)) p))
The theorem `AddSubmonoid.bsupr_eq_mrange_dfinsupp_sumAddHom` states that for any type `ι`, type `γ` (which is a commutative additive monoid), a property `p` on `ι` (which has decidable truth value for each element of `ι`), and a family `S` of commutative additive submonoids indexed by `ι`, the supremum of the family `S` of submonoids (considering only those indices `i` for which `p i` is true) is equal to the range of the function obtained by first filtering elements of the direct sum `Π₀ (i : ι), ↥(S i)` according to `p`, then summing each non-zero component of the filtered sum into `γ` using `DFinsupp.sumAddHom` applied to the subtype map of each `S i`. This essentially says that any element in the supremum can be obtained by selecting a finite number of elements from submonoids `S i` (where `p i` is true), mapping them into `γ` and then taking their sum.
More concisely: For any commutative additive monoid γ, property p on ι with decidable truth value, and family S of commutative additive submonoids indexed by ι, the supremum of the submonoids S i where pi is true equals the range of the function obtained by summing the non-zero components of the filtered direct sum ⨄(i : ι), ↥(Si) using DFinsupp.sumAddHom applied to the subtype map of each Si.
|
DFinsupp.extendWith_some
theorem DFinsupp.extendWith_some :
∀ {ι : Type u} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)] (f : Π₀ (i : ι), α (some i))
(a : α none) (i : ι), (DFinsupp.extendWith a f) (some i) = f i
The theorem `DFinsupp.extendWith_some` states that for any type `ι`, any function `α` from the option of `ι` to some other type, given that for every `i` which is an option of `ι`, the `α i` is a zero type, and for any `dfinsupp` `f` indexed by `ι` with values in `α (some i)` and any element `a` of type `α none`, if we apply the `DFinsupp.extendWith` function on `a` and `f` and then apply this result to `some i`, we get the original `f i`. In simpler terms, if we extend a dfinsupp `f` indexed by `ι` with an element `a` and then try to retrieve an element at `some i`, we get back the original element at `i` in `f`.
More concisely: For any type `ι`, function `α` from the option of `ι` to a zero type, and `dfinsupp` `f` indexed by `ι` with values in `α (some i)`, `f (some i) = DFinsupp.extendWith some i a (DFinsupp.extendWith a none f)`.
|
DFinsupp.coe_neg
theorem DFinsupp.coe_neg :
∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g : Π₀ (i : ι), β i), ⇑(-g) = -⇑g
This theorem, `DFinsupp.coe_neg`, states that for any type `ι`, any type function `β` from `ι` to some other type, and any `AddGroup` instance for `β i` (for each `i` in `ι`), the negation of a function `g` from `ι` to `β` (where `g` is a direct-sum function, meaning it is zero for almost all input) can be obtained by applying the negation to the function `g` itself. In simpler terms, applying negation to the function is the same as negating each value of the function independently.
More concisely: For any type `ι`, any type function `β` from `ι` to an additive group, and any direct-sum function `g : ι → β`, the negation of `g` is equal to the function that maps each `i` in `ι` to the additive negation of `g i`.
|
AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom
theorem AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom :
∀ {ι : Type u} {γ : Type w} [inst : DecidableEq ι] [inst_1 : AddCommMonoid γ] (S : ι → AddSubmonoid γ),
iSup S = AddMonoidHom.mrange (DFinsupp.sumAddHom fun i => (S i).subtype)
The theorem `AddSubmonoid.iSup_eq_mrange_dfinsupp_sumAddHom` states that for any type `ι`, type `γ` that is a commutative additive monoid, and a function `S` that maps each element of `ι` to an additive submonoid of `γ`, the indexed supremum of these submonoids (`iSup S`) is equal to the range of the additive monoid homomorphism obtained by summing over the function `DFinsupp.sumAddHom`, applied to the subtypes of `S i` for each `i`. In other words, every element in the supremum of the family of submonoids can be generated by summing a finite number of non-zero elements from the submonoids `S i`, after they have been coerced to `γ`.
More concisely: For any commutative additive monoid γ and a function S that maps each index ι to an additive submonoid of γ, the indexed supremum of the submonoids S i is equal to the range of the additive monoid homomorphism obtained by summing over DFinsupp.sumAddHom(S i) for each i.
|
DFinsupp.liftAddHom_singleAddHom
theorem DFinsupp.liftAddHom_singleAddHom :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddCommMonoid (β i)],
DFinsupp.liftAddHom (DFinsupp.singleAddHom β) = AddMonoidHom.id (Π₀ (i : ι), β i)
This theorem, named `DFinsupp.liftAddHom_singleAddHom`, states that for any type `ι` and function `β` mapping `ι` to a type `v`, given that equality on `ι` is decidable and for each `i` in `ι`, the type `β i` forms an additive commutative monoid, using `DFinsupp.singleAddHom` as an argument to `DFinsupp.liftAddHom` results in the identity map on the type of direct sum (`Π₀`) from `ι` to `β i`. In other words, `DFinsupp.liftAddHom` applied to each "singleton" direct sum (created with `DFinsupp.singleAddHom`) gives back the original direct sum space, same as applying identity map on it.
More concisely: Given a decidably-equated type ι and an additive commutative monoid structure on the type β i for each i in ι, the application of `DFinsupp.liftAddHom` to `DFinsupp.singleAddHom` for each i results in the identity function on the direct sum Π₀ i → β i.
|
DFinsupp.addHom_ext
theorem DFinsupp.addHom_ext :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {γ : Type w}
[inst_2 : AddZeroClass γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄,
(∀ (i : ι) (y : β i), f (DFinsupp.single i y) = g (DFinsupp.single i y)) → f = g
This theorem states that for any type `ι`, and a function `β` from `ι` to some type, given a decidable equality on `ι` and an additive zero class on each `β i`, and a third type `γ` that also has an additive zero class, if there are two additive homomorphisms `f` and `g` from `Π₀ i, β i` to `γ` that are equal on each `DFinsupp.single i y`, then these two homomorphisms are equal.
In simpler terms, if you have two homomorphisms that map a direct sum of the types `β i` to `γ` and they agree on each "singleton" direct sum (`DFinsupp.single i y`), then the two homomorphisms are actually the same. The singleton direct sum is a function that sends `i` to `y` and all other points to `0`.
More concisely: Given types `ι`, a function `β : ι → T`, a decidable equality on `ι`, additive zero classes on `β i` and `γ`, and two additive homomorphisms `f` and `g` from `Π₀ i, β i` to `γ`, if `f (DFinsupp.single i y) = g (DFinsupp.single i y)` for all `i` and `y`, then `f = g`.
|
DFinsupp.coe_sub
theorem DFinsupp.coe_sub :
∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddGroup (β i)] (g₁ g₂ : Π₀ (i : ι), β i),
⇑(g₁ - g₂) = ⇑g₁ - ⇑g₂
This theorem states that for any type `ι`, a family of types `β` indexed by `ι`, and an instance of `AddGroup` for each type in the family, if you have two direct sum representations (`g₁` and `g₂`), then the function of subtracting `g₂` from `g₁` is equal to the function of subtracting the corresponding elements of `g₁` and `g₂`. In other words, it is stating that the operation of subtraction commutes with the function application for direct sum representations in the context of additive groups.
More concisely: Given types `ι`, a family of AddGroup types `β` indexed by `ι`, and instances of AddGroup for each `β`, for any `g₁`, `g₂` in the direct sum representation of `β i` for each `i ∈ ι`, the function `x ↦ g₁ x - g₂ x` is equal to the function `x ↦ (g₁ x) - (g₂ x)` from `ι` to `β`.
|
DFinsupp.liftAddHom_apply_single
theorem DFinsupp.liftAddHom_apply_single :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
[inst_2 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι) (x : β i),
(DFinsupp.liftAddHom f) (DFinsupp.single i x) = (f i) x
This theorem, named `DFinsupp.liftAddHom_apply_single`, asserts that for any types `ι`, `γ`, and a type family `β` indexed by `ι`, given a decidable equality on `ι`, additive structures (`AddZeroClass`) on each `β i` for `i : ι` and a commutative additive monoid on `γ`, and a function `f` from each `ι` and `β i` to `γ`, the function `DFinsupp.liftAddHom` applied to `f` and then applied to a single-valued function `DFinsupp.single i x` (which assigns the value `x` to `i` and `0` to all other points) will yield the same result as applying `f` to `i` and `x`. In mathematical terms, this theorem is essentially expressing the fact that `liftAddHom` is an additive homomorphism that respects the "single" operation.
More concisely: Given a decidable equality on `ι`, additive structures on each `β i`, a commutative additive monoid on `γ`, and a function `f` from `ι × β` to `γ`, the function `DFinsupp.liftAddHom f` applied to `DFinsupp.single i x` is equal to `f i x`.
|
DFinsupp.single_eq_of_ne
theorem DFinsupp.single_eq_of_ne :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] {i i' : ι} {b : β i},
i ≠ i' → (DFinsupp.single i b) i' = 0
The theorem `DFinsupp.single_eq_of_ne` asserts that for any types `ι` and `β` where `β` is a function of `ι`, given a decidable equality on `ι` and a zero element for every `β i`, if we have two elements `i` and `i'` from `ι`, and an element `b` from `β i`, if `i` is not equal to `i'` (`i ≠ i'`), then the application of the function `DFinsupp.single i b` to `i'` yields `0`.
In simpler terms, it states that the function `DFinsupp.single i b` maps any element `i'` not equal to `i` to zero.
More concisely: For any types `ι` and `β` where `β` is a function of `ι`, if `DFinsupp.single i b` is defined for `i ≠ i'` in `ι`, then `DFinsupp.single i b i' = 0`.
|
DFinsupp.coe_smul
theorem DFinsupp.coe_smul :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : Monoid γ] [inst_1 : (i : ι) → AddMonoid (β i)]
[inst_2 : (i : ι) → DistribMulAction γ (β i)] (b : γ) (v : Π₀ (i : ι), β i), ⇑(b • v) = b • ⇑v
This theorem states that for any types `ι`, `γ`, and a type function `β` from `ι` to some type, given a `Monoid` structure on `γ` and an `AddMonoid` structure on each `β i` as well as a `DistribMulAction` structure (a distribution law for multiplication over addition) for `γ` acting on each `β i`, if we have a `b` from the `γ` type and a direct sum (DFinsupp) `v` over the `β i`, we can distribute the scalar multiplication of `b` over `v` inside the function application of `v`. In more mathematical terms, for all `b` in `γ` and `v` in the direct sum of `β i` over `ι`, the application of the result of scaling `v` by `b` is equal to scaling the result of applying `v` by `b`. This essentially validates the law of scalar multiplication distribution over function application for this mathematical context.
More concisely: For any Monoid `γ`, AddMonoid `β i`, and a Distribution Law for multiplication over addition `DistribMulAction` on `γ` acting on each `β i`, if `b` is an element of `γ` and `v` is a direct sum over `ι`, then scaling `v` by `b` and applying it is equivalent to applying `v` and scaling the result by `b`.
|
Mathlib.Data.DFinsupp.Basic._auxLemma.16
theorem Mathlib.Data.DFinsupp.Basic._auxLemma.16 :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
[inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (f : Π₀ (i : ι), β i) (i : ι), (i ∈ f.support) = (f i ≠ 0)
The given theorem states that for any types `ι` and `β` mapping `ι` to `β`, given that `ι` has decidable equality, and that every `i` in `ι` maps to a zero of `β` and for each `i` in `ι` and `x` in `β i`, `x ≠ 0` is decidable, then for any function `f` of type `(Π₀ (i : ι), β i)` and any `i` in `ι`, `i` is in the support of `f` if and only if `f i` is not equal to zero. In other words, the support of `f` is exactly the set of `i` in `ι` such that `f i` is not zero.
More concisely: The support of a function `f` from a type `ι` to a type `β`, where `β` maps `ι` to itself and every element of `ι` maps to a non-zero element of `β`, is equal to the subset of `ι` consisting of elements mapping to non-zero values.
|
DFinsupp.sumAddHom_single
theorem DFinsupp.sumAddHom_single :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
[inst_2 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ) (i : ι) (x : β i),
(DFinsupp.sumAddHom φ) (DFinsupp.single i x) = (φ i) x
This theorem, `DFinsupp.sumAddHom_single`, states that for any types `ι`, `γ`, and a type function `β : ι → Type v` with `DecidableEq ι`, `AddZeroClass` on `β i` for each `i : ι`, and `AddCommMonoid γ`, and for any additive homomorphism `φ : (i : ι) → β i →+ γ`, and any `i : ι` and `x : β i`, applying the sum-additive homomorphism `DFinsupp.sumAddHom φ` to the direct sum of `β`'s `DFinsupp.single i x` (which sends `i` to `x` and all other points to `0`) is equivalent to applying `φ i` to `x`. In simpler terms, it's saying that summing over a single-element direct sum (with `DFinsupp.sumAddHom φ`) is the same as just applying the homomorphism directly to the single element (`φ i x`).
More concisely: For any additive homomorphism `φ` and `i : ι`, applying `DFinsupp.sumAddHom φ` to the direct sum of `β i`'s single-element finite support discrete additive monoid element `DFinsupp.single i x` is equal to applying `φ i` to `x`.
|
DFinsupp.sumAddHom_apply
theorem DFinsupp.sumAddHom_apply :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
[inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] (φ : (i : ι) → β i →+ γ)
(f : Π₀ (i : ι), β i), (DFinsupp.sumAddHom φ) f = f.sum fun x => ⇑(φ x)
The theorem `DFinsupp.sumAddHom_apply` states that for any type `ι`, `γ` and a type `β` dependent on `ι`, given a decision procedure for equality on `ι`, an instance of the `AddZeroClass` for each `β i`, a decision procedure for non-equality with zero for each `β i`, and an additive commutative monoid structure on `γ`, if we have a function `φ` mapping each `β i` to `γ` and a function `f` of type `Π₀ (i : ι), β i`, then the application of `DFinsupp.sumAddHom φ` to `f` is equal to the sum of `f` over the support of `f` where each `φ x` is applied to the sum. In other words, while we didn't need decidable instances to define the sum, we do need them to reduce it to a sum.
More concisely: Given a family `f` of additive commutative monoid values indexed by `ι`, the application of `DFinsupp.sumAddHom φ` to `f` equals the sum of `φ (f i)` over the support of `f`, where `φ` maps each index `i` to the additive monoid value `β i`.
|
DFinsupp.support_eq_empty
theorem DFinsupp.support_eq_empty :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
[inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] {f : Π₀ (i : ι), β i}, f.support = ∅ ↔ f = 0
This theorem, `DFinsupp.support_eq_empty`, states that for any types `ι` and `β` where `β` is a function from `ι` to some type, and given instances of decidable equality for `ι`, a zero for each `β i`, and decidable inequality from zero for each `β i`, a function `f` of type `Π₀ (i : ι), β i` (direct product of `β i` over `ι`) has an empty support (i.e., all elements of `f` are zero) if and only if `f` is the zero function. In other words, the support of `f` is empty if and only if `f` maps every element of `ι` to zero.
More concisely: The theorem asserts that a function from a type ι to β has an empty support (i.e., maps every element to zero) if and only if it is the zero function, given decidable equality for ι, and decidable inequality from zero for each β i.
|
DFinsupp.filter_single
theorem DFinsupp.filter_single :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] (p : ι → Prop)
[inst_2 : DecidablePred p] (i : ι) (x : β i),
DFinsupp.filter p (DFinsupp.single i x) = if p i then DFinsupp.single i x else 0
The theorem `DFinsupp.filter_single` states that for any type `ι`, any type family `β` indexed over `ι`, and any predicate `p` on `ι`, provided that `ι` has decidable equality and every type in the family `β` has a zero element, if we have a decidable predicate `p` and elements `i` of type `ι` and `x` of type `β i`, then filtering the function that sends `i` to `x` and all other points to `0` according to the predicate `p` results in either the original function (if `p i` holds) or the constantly zero function (if `p i` does not hold).
More concisely: For any type `ι`, type family `β` indexed over `ι`, decidable equality on `ι`, and a zero element in each `β i`, if `p` is a decidable predicate on `ι` and `x` is an element of `β i`, then the function that maps `i` to `x` and all other points to `0`, filtered by `p`, is equal to the original function if `p(i)` holds, or the constantly zero function otherwise.
|
DFinsupp.extendWith_none
theorem DFinsupp.extendWith_none :
∀ {ι : Type u} {α : Option ι → Type v} [inst : (i : Option ι) → Zero (α i)] (f : Π₀ (i : ι), α (some i))
(a : α none), (DFinsupp.extendWith a f) none = a
The theorem `DFinsupp.extendWith_none` states that for any type `ι`, any function `α` from `Option ι` to a type, a Direct-sum Finite-support function `f` from `ι` to `α (some i)`, and a term `a` of type `α none`, if we extend `f` with the term `a` to get a Direct-sum Finite-support function from `Option ι` to `α i` using the `DFinsupp.extendWith` function, then the value of this extended function at `none` is `a`. In other words, `DFinsupp.extendWith` correctly integrates the term `a` into the direct-sum finite-support function at the index `none`.
More concisely: For any type `ι`, function `α : Option ι → Type`, Direct-sum Finite-support function `f : ι → α (some i)`, and term `a : α none`, `DFinsupp.extendWith f a` is the extension of `f` with `a` as the value at index `none`. Thus, `DFinsupp.extendWith_none f a = a`.
|
DFinsupp.single_smul
theorem DFinsupp.single_smul :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : Monoid γ]
[inst_2 : (i : ι) → AddMonoid (β i)] [inst_3 : (i : ι) → DistribMulAction γ (β i)] {i : ι} (c : γ) (x : β i),
DFinsupp.single i (c • x) = c • DFinsupp.single i x
The theorem `DFinsupp.single_smul` states that given any types `ι`, `γ`, and a type function `β` from `ι` to some type, if `ι` has decidable equality, `γ` is a Monoid, each `β i` (for `i` in `ι`) is an Additive Monoid, and each `β i` is a Distributive Multiplication Action over `γ`, then for any instance `i` of `ι`, scalar `c` of `γ`, and element `x` of `β i`, scaling `x` by `c` and then applying the `DFinsupp.single` function is the same as first applying `DFinsupp.single` to `x` and then scaling the result by `c`. In simple terms, it asserts the commutativity of the scalar multiplication operation with the `DFinsupp.single` operation.
More concisely: Given a type `ι` with decidable equality, a Monoid `γ`, and a type function `β : ι → AddMonoid γ`, if each `β i` is a Distributive Multiplication Action over `γ`, then for all `i ∈ ι`, `c ∈ γ`, and `x ∈ β i`, `DFinsupp.single (c * x) = c * DFinsupp.single x`.
|
DFinsupp.zero_apply
theorem DFinsupp.zero_apply : ∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → Zero (β i)] (i : ι), 0 i = 0
The theorem `DFinsupp.zero_apply` states that for any type `ι`, and a type function `β` mapping `ι` to another type, given that for all `i` in `ι`, `β i` has an associated `Zero` instance, then the application of the zero function (or object) at any index `i` equals to the zero element of the co-domain. In terms of mathematical notation, this theorem is essentially stating that for any index `i`, `0(i) = 0`, where the left-hand side zero is the zero function and the right-hand side zero is the zero element of the co-domain.
More concisely: For any type `ι` and type function `β` from `ι` to a type with a Zero instance, the application of the zero function to any index `i` in `ι` equals the zero element of the co-domain `β i`.
|
DFinsupp.coe_nsmul
theorem DFinsupp.coe_nsmul :
∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddMonoid (β i)] (b : ℕ) (v : Π₀ (i : ι), β i),
⇑(b • v) = b • ⇑v
This theorem states that for any type `ι`, any function `β` mapping elements of `ι` to another type, and for any instance which provides an addition operation for the type returned by `β`, the application of a scalar multiplication (`b • v`) over a direct sum function `v` (denoted as `Π₀ (i : ι), β i`) is equal to scalar multiplication applied to the result of function `v`. In other words, scalar multiplication can be interchanged with function application.
More concisely: For any type `ι`, function `β : ι → T`, and instance of addition on `T`, the scalar multiplication `b • (Π₀ i : ι, β i)` equals the application of scalar multiplication to each component of the product `Π₀ i : ι, b • β i`.
|
DFinsupp.liftAddHom_comp_single
theorem DFinsupp.liftAddHom_comp_single :
∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
[inst_2 : AddCommMonoid γ] (f : (i : ι) → β i →+ γ) (i : ι),
(DFinsupp.liftAddHom f).comp (DFinsupp.singleAddHom β i) = f i
The theorem `DFinsupp.liftAddHom_comp_single` states that for any types `ι`, `γ`, and `β` which is a function from `ι` to some type, given that equality for `ι` is decidable, each `β i` for `i : ι` possesses the structure of an additive group with a zero element (`AddZeroClass`), and `γ` is an additive commutative monoid, then for any additive monoid homomorphism `f : (i : ι) → β i →+ γ` and any `i : ι`, the composition of the `DFinsupp.liftAddHom f` and `DFinsupp.singleAddHom β i` is equal to `f i`. This can be thought of as a statement about the interaction between the lifting operation and the singleton creation operation in the context of finitely supported functions from `ι` to `β`, when these functions are considered as additive homomorphisms.
More concisely: For any decidably equated type `ι`, and given that each `β i` is an additive group with a zero element and `γ` is an additive commutative monoid, the composition of the lifting of an additive monoid homomorphism `f : ι → β →+ γ` with the single additive homomorphism `DFinsupp.singleAddHom β i` equals `f i`.
|
DFinsupp.coe_add
theorem DFinsupp.coe_add :
∀ {ι : Type u} {β : ι → Type v} [inst : (i : ι) → AddZeroClass (β i)] (g₁ g₂ : Π₀ (i : ι), β i),
⇑(g₁ + g₂) = ⇑g₁ + ⇑g₂
This theorem states that for any types `ι` and `β`, and function `β` from `ι` to `Type v`, where each `β i` forms an additive group with zero (`AddZeroClass`), the sum of two direct sum functions `g₁` and `g₂` (of type `Π₀ (i : ι), β i`) can be obtained by separately applying the functions `g₁` and `g₂` and then adding the results. In mathematical terms, this theorem ensures that the addition operation is compatible with the function application operation for direct sum functions.
More concisely: For any types `ι` and `β`, and functions `g₁`, `g₂` : ι → β with each `β i` an additive group, the function `(g₁ + g₂) : ι → β` equals the application of `g₁` and `g₂` followed by the addition of their outputs: `(g₁ + g₂) i = g₁ i + g₂ i`.
|
DFinsupp.comapDomain_apply
theorem DFinsupp.comapDomain_apply :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] {κ : Type u_1} [inst_1 : (i : ι) → Zero (β i)] (h : κ → ι)
(hh : Function.Injective h) (f : Π₀ (i : ι), β i) (k : κ), (DFinsupp.comapDomain h hh f) k = f (h k)
The theorem `DFinsupp.comapDomain_apply` states that for all types `ι` and `κ`, and for all functions from `κ` to `ι` that are injective, and for every function `f` from `ι` to some type `β`, applying the function `DFinsupp.comapDomain` gives a new function such that when this new function is applied to any element `k` of type `κ`, it gives the same result as applying `f` to the image of `k` under the injective function. In a mathematical language, given an injective function `h: κ → ι`, and a direct sum function `f: Π₀ (i : ι), β i`, `DFinsupp.comapDomain h hh f` reindexes (and possibly removes) the terms of `f` according to `h`, such that applying this reindexed function at `k` is same as applying `f` at `h(k)`.
More concisely: Given an injective function `h: κ -> ι` and a function `f: ι -> β`, `DFinsupp.comapDomain h h f` applies `f` to the images of `ι` elements under `h`, resulting in a function that gives the same output as applying `f` directly to the images.
|
DFinsupp.mk_add
theorem DFinsupp.mk_add :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {s : Finset ι}
{x y : (i : ↑↑s) → β ↑i}, DFinsupp.mk s (x + y) = DFinsupp.mk s x + DFinsupp.mk s y
The theorem `DFinsupp.mk_add` asserts the distributivity of the `DFinsupp.mk` function over addition. More specifically, for any given type `ι`, a type family `β` indexed by `ι`, a finite set `s` of type `ι`, and two functions `x` and `y` from the elements of `s` to the corresponding `β` values, the direct sum of the direct finitely supported functions created by `x` and `y` is the same as the direct finitely supported function created by the sum of `x` and `y`. This is under the assumptions that `ι` has decidable equality and each `β i` forms an additive monoid with zero.
More concisely: For any type `ι` with decidable equality and indexed type family `β`, and finite sets `s` with functions `x` and `y` from `s` to `β` such that each `β i` forms an additive monoid with zero, the finite sum of the direct finitely supported functions `DFinsupp.mk x` and `DFinsupp.mk y` equals `DFinsupp.mk (x + y)`.
|
DFinsupp.addHom_ext'
theorem DFinsupp.addHom_ext' :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)] {γ : Type w}
[inst_2 : AddZeroClass γ] ⦃f g : (Π₀ (i : ι), β i) →+ γ⦄,
(∀ (x : ι), f.comp (DFinsupp.singleAddHom β x) = g.comp (DFinsupp.singleAddHom β x)) → f = g
This theorem states that if we have two additive homomorphisms `f` and `g` from the direct sum of a family of additive monoids `β i` (for `i` in some index set `ι`) to another additive monoid `γ`, and if these two homomorphisms are equal when composed with the additive homomorphism corresponding to the `single a b` operation for every `a` in the index set `ι`, then `f` and `g` are equal. Here, the `single a b` operation is defined as inserting an element `b` from `β a` into the direct sum in the position corresponding to `a`. The proof of this theorem relies on the properties of additive homomorphisms and the structure of the direct sum.
More concisely: If two additive homomorphisms from the direct sum of a family of additive monoids to another additive monoid agree on the `single a b` operation for every index `a`, then they are equal.
|
DFinsupp.single_eq_single_iff
theorem DFinsupp.single_eq_single_iff :
∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)] (i j : ι) (xi : β i)
(xj : β j), DFinsupp.single i xi = DFinsupp.single j xj ↔ i = j ∧ HEq xi xj ∨ xi = 0 ∧ xj = 0
The theorem `DFinsupp.single_eq_single_iff` states that for any types `ι` and `β`, where `ι` has decidable equality and each `β i` has a zero element, for any `i, j : ι` and `xi : β i`, `xj : β j`, the dependent function `DFinsupp.single i xi` is equal to `DFinsupp.single j xj` if and only if either `i` is equal to `j` and `xi` is heterogeneously equal to `xj` or `xi` is equal to zero and `xj` is equal to zero. Here, `DFinsupp.single` is a function that sends `i` to `xi` and all other points to `0`, and `HEq` is a heterogeneous equality that allows comparison of values of potentially different types.
More concisely: For any types `ι` with decidable equality and each element `β i` having a zero element, the dependent functions `DFinsupp.single i xi` and `DFinsupp.single j xj` are equal if and only if `i` equals `j` and `xi` is heterogeneously equal to `xj` or both `xi` and `xj` are zero.
|