ContinuousAlternatingMap.vecCons_smul
theorem ContinuousAlternatingMap.vecCons_smul :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N]
{n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (c : R) (x : M),
f (Matrix.vecCons (c • x) m) = c • f (Matrix.vecCons x m)
This theorem states that for continuous alternating maps on spaces indexed by `Fin (n+1)`, where one can construct an element of `Π(i : Fin (n+1)), M i` using the `vecCons` function, we can directly express the multiplicative property of an alternating map along the first variable. Specifically, given a semiring `R`, an additively commutative monoid `M` and `N` which are modules over `R`, and for `M` and `N` being topological spaces, a continuous alternating map `f` from the tensor product of `M` over `Fin (n+1)` to `N`, a map `m` from `Fin n` to `M`, a scalar `c` from `R`, and an element `x` from `M`, the theorem states that applying `f` to the vector created by prepending `c • x` to `m` is the same as scaling by `c` the result of applying `f` to the vector created by prepending `x` to `m`. In terms of mathematical notation, it states that `f(vecCons(c • x, m)) = c • f(vecCons(x, m))`.
More concisely: For a continuous alternating map `f` from the tensor product of a semiring `R`-module `M` over `Fin (n+1)` to an `R`-module `N`, and given `x` in `M`, `m` in `M^(Fin n)`, and a scalar `c` in `R`, `f(vecCons(c • x, m)) = c • f(vecCons(x, m))`.
|
ContinuousAlternatingMap.cons_add
theorem ContinuousAlternatingMap.cons_add :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N]
{n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (x y : M),
f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
This theorem, named `ContinuousAlternatingMap.cons_add`, states that for an alternating map `f` defined on a continuous space and with continuous output, when it operates on an `(n+1)`-tuple constructed by `cons` from the sum of two elements `x` and `y` in the continuous space `M` of a semiring `R` and an `n`-tuple `m`, it is equal to the sum of the values of `f` assessed on the `(n+1)`-tuples individually constructed by `cons` from `x` and `y` and the same `n`-tuple `m`. This theorem asserts the direct additivity of an alternating map along the first variable in the specific case of continuous spaces indexed by `Fin (n+1)`.
More concisely: For an alternating map `f` from a continuous space `M` of a semiring `R` with continuous output, `f (x :: y :: m) = f x :: f y :: m` holds for all `x, y in M` and `m in Fin (n+1) -> M`, where `::` denotes the list cons construction.
|
ContinuousAlternatingMap.ext
theorem ContinuousAlternatingMap.ext :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
[inst_6 : TopologicalSpace N] {f g : M [⋀^ι]→L[R] N}, (∀ (x : ι → M), f x = g x) → f = g
This theorem states that for any two continuous alternating maps `f` and `g` from a tensor power of a module `M` over a semiring `R` to a topological module `N` over the same semiring `R`, if these maps are equal for all inputs `x` (from the index set `ι` to `M`), then the maps `f` and `g` are identical.
In other words, two continuous alternating maps are equal if they produce the same output for every possible input.
More concisely: If two continuous alternating maps from the same tensor power of a module to a topological module over a semiring are equal on all inputs, then they are identical.
|
ContinuousAlternatingMap.toContinuousMultilinearMap_injective
theorem ContinuousAlternatingMap.toContinuousMultilinearMap_injective :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
[inst_6 : TopologicalSpace N], Function.Injective ContinuousAlternatingMap.toContinuousMultilinearMap
The theorem `ContinuousAlternatingMap.toContinuousMultilinearMap_injective` asserts that for any semiring `R`, Additive Commutative Monoid `M` and `N` and any types `ι` with `M` and `N` being topological spaces and modules over `R`, the function `toContinuousMultilinearMap` from `ContinuousAlternatingMap` is injective. This means that if two continuous alternating maps have the same corresponding continuous multilinear map, then these two continuous alternating maps were originally identical.
More concisely: For any semiring `R`, given continuous alternating maps `f` and `g` from a topological space `X` to the module `M` over `R`, if their corresponding continuous multilinear maps have equal functions, then `f` and `g` are identical.
|
ContinuousAlternatingMap.map_sum
theorem ContinuousAlternatingMap.map_sum :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
[inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {α : ι → Type u_7} [inst_7 : Fintype ι]
[inst_8 : DecidableEq ι] (g' : (i : ι) → α i → M) [inst_9 : (i : ι) → Fintype (α i)],
(f fun i => Finset.univ.sum fun j => g' i j) = Finset.univ.sum fun r => f fun i => g' i (r i)
The theorem `ContinuousAlternatingMap.map_sum` states that for a continuous alternating function `f`, the value of `f` applied to the tuple of sums `(Σ_{j₁} g₁ j₁, ..., Σ_{jₙ} gₙ jₙ)` is equal to the sum of `f` applied to tuples `(g₁ (r 1), ..., gₙ (r n))` as `r` ranges over all functions. Here, `R`, `M`, `N`, and `ι` are types representing a semiring, two modules over `R`, and an index set respectively. The operations on the modules are assumed to be continuous. The function `g'` maps each index `i` in `ι` and each element of `α i` to an element in `M`. The types `α i` are finitely enumerable for each `i` in `ι` and `ι` itself also has decidable equality.
In simpler terms, this theorem is about redistributing the continuous alternating operation `f` over a sum of terms, similar to the distributive property of multiplication over addition. The sum is taken over all elements in the finite sets `α i`, for each `i` in `ι`.
More concisely: For a continuous alternating function `f` and continuous operations on a semiring `R`, given functions `g'_i : ι × M → M` with `α i` finite and decidably equal, the application of `f` to the tuple of sums `(Σj₁ gi j₁, ..., Σjₙ gi jₙ)` is equal to the sum of `f` applied to tuples `(g'_i r i)` as `r` ranges over all functions.
|
ContinuousAlternatingMap.vecCons_add
theorem ContinuousAlternatingMap.vecCons_add :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N]
{n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (x y : M),
f (Matrix.vecCons (x + y) m) = f (Matrix.vecCons x m) + f (Matrix.vecCons y m)
This theorem states that for continuous alternating maps on spaces indexed by `Fin (n+1)`, if you build an element of `Π(i : Fin (n+1)), M i` using `cons`, you can directly express the additivity of an alternating map along the first variable. More specifically, for any semiring `R`, add-commutative monoids `M` and `N`, an `R`-module structure on `M` and `N`, topological spaces on `M` and `N`, a natural number `n`, a continuous alternating map `f`, a map from `Fin n` to `M`, and two elements `x` and `y` of `M`, it holds that the value of `f` after prepending `x + y` to `m` is equal to the sum of the value of `f` after prepending `x` to `m` and the value of `f` after prepending `y` to `m`.
More concisely: For any continuous alternating map `f` on topological spaces indexed by `Fin (n+1)`, and any `x, y \in M` and `m : \Pi i, Fin (n+1), M i`, the equality `f (x + y :: m) = f (x :: m) + f (y :: m)` holds, where `+` denotes the additions in `M` and `\Pi` denotes the product type in Lean.
|
ContinuousAlternatingMap.map_add_univ
theorem ContinuousAlternatingMap.map_add_univ :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
[inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : DecidableEq ι] [inst_8 : Fintype ι] (m m' : ι → M),
f (m + m') = Finset.univ.sum fun s => f (s.piecewise m m')
This theorem, `ContinuousAlternatingMap.map_add_univ`, states that for all semirings `R`, additive commutative monoids `M` and `N`, an index type `ι`, and given certain conditions including `M` and `N` being modules over `R` and topological spaces, a continuous alternating map `f` from `M` tensor-powered by `ι` to `N` (linear over `R`), a decidable equality on `ι`, and the finiteness of `ι`, the map applied to the sum of two functions `m` and `m'` (from `ι` to `M`) is equal to the sum (over all subsets of the universe of the finite type `ι`) of the map applied to a function that is piecewise defined as `m` and `m'` depending on the subset. In summary, it's about expressing the additivity of a continuous alternating map in terms of a sum over all subsets of an index set.
More concisely: For a continuous alternating map `f` from the product of an index type `ι`, a semiring `R`, and additive commutative monoids `M` and `N`, where `M` and `N` are modules over `R` and topological spaces, if `f` is linear over `R`, `ι` is decidable and finite, and `m`, `m'` are functions from `ι` to `M`, then `∑ i: ι, f(m i ⊕ m' i) = ∑ s: Set ι, ∑ i ∈ s, f(i ↔ m i ⊕ m' i)` where `i ↔ j` is the swap function on `ι`.
|
ContinuousAlternatingMap.cons_smul
theorem ContinuousAlternatingMap.cons_smul :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N]
{n : ℕ} (f : M [⋀^Fin (n + 1)]→L[R] N) (m : Fin n → M) (c : R) (x : M),
f (Fin.cons (c • x) m) = c • f (Fin.cons x m)
This theorem describes the property of continuous alternating maps on spaces indexed by a finite set of size `n+1` (denoted by `Fin (n+1)`). More specifically, it states that given a semiring `R`, types `M` and `N` equipped with the structure of `R`-modules and topological spaces, a continuous alternating map `f` from the tensor product of `M` indexed by `Fin (n+1)` to `N`, a mapping `m` from `Fin n` to `M`, a scalar `c` from `R`, and an element `x` of `M`, the map `f` applied to an `(n+1)`-tuple of `M` constructed by prepending the scalar multiplication of `c` and `x` to `m` (represented as `Fin.cons (c • x) m`) is equal to the scalar multiplication of `c` and `f` applied to an `(n+1)`-tuple constructed by prepending `x` to `m` (represented as `c • f (Fin.cons x m)`). In other words, the continuous alternating map `f` preserves the scalar multiplication along the first variable in an `(n+1)`-tuple.
More concisely: Given a continuous alternating map `f` from the tensor product of an `R`-module and topological space `M` indexed by `Fin (n+1)` to an `R`-module and topological space `N`, and given an `R`-module `M`, an `R`-scalar `c`, and an element `x` in `M`, we have `f (Fin.cons (c • x) m) = c • f (Fin.cons x m)`, where `m` is an `n`-tuple in `M`.
|
ContinuousAlternatingMap.map_eq_zero_of_eq'
theorem ContinuousAlternatingMap.map_eq_zero_of_eq' :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
[inst_6 : TopologicalSpace N] (self : M [⋀^ι]→L[R] N) (v : ι → M) (i j : ι),
v i = v j → i ≠ j → self.toFun v = 0
This theorem, `ContinuousAlternatingMap.map_eq_zero_of_eq'`, states that for any given semiring `R`, additive commutative monoid `M`, module `M` over `R`, topological space `M`, additive commutative monoid `N`, module `N` over `R`, and topological space `N`, a continuous alternating map (represented as `self` of type `M [⋀^ι]→L[R] N`) applied to a function `v : ι → M` will yield zero if there exist two different elements (`i` and `j`) in the domain of `v` such that `v i = v j`. In other words, if the function `v` has two equal values for different inputs, the continuous alternating map will map `v` to zero.
More concisely: For any continuous alternating map `f : (ι → M) → L[R] N`, if there exist distinct indices `i` and `j` in the domain of `f(x)` such that `f(i)(x) = f(j)(x)` for all `x` in `M`, then `f(v) = 0`.
|
ContinuousAlternatingMap.map_smul_univ
theorem ContinuousAlternatingMap.map_smul_univ :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
[inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) [inst_7 : Fintype ι] (c : ι → R) (m : ι → M),
(f fun i => c i • m i) = (Finset.univ.prod fun i => c i) • f m
This theorem states that for a continuous alternating map `f` from a module `M` over a commutative semiring `R` to another module `N`, the map's value at each element `i` of a finite set `ι`, where each element is scaled by a factor `c i`, is equal to the product of all scale factors times the map's value at `m`. In more mathematical terms, it translates to the following: for any `f : M [⋀^ι]→L[R] N`, `f(∑ i, c(i) * m(i)) = (∏ i, c(i)) * f(m)`, where the sums and product are taken over all elements of `ι`, assuming `ι` is a finite set.
More concisely: For a continuous alternating map $f$ from a finite-dimensional module $M$ over a commutative semiring $R$ to another module $N$, the value of $f$ at the weighted sum $\sum\_{i \in \gamma} c\_i \cdot x\_i$ is equal to the product of all scale factors times the value of $f$ at $(x\_1, \dots, x\_n)$, where $n = \text{card}(\gamma)$.
|
ContinuousAlternatingMap.map_sum_finset
theorem ContinuousAlternatingMap.map_sum_finset :
∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
[inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
[inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N) {α : ι → Type u_7} [inst_7 : Fintype ι]
[inst_8 : DecidableEq ι] (g' : (i : ι) → α i → M) (A : (i : ι) → Finset (α i)),
(f fun i => (A i).sum fun j => g' i j) = (Fintype.piFinset A).sum fun r => f fun i => g' i (r i)
This theorem states that for a continuous alternating map `f`, the value of `f` at the sum of terms `g_i(j_i)` (where `j_i` ranges over a finite set `A_i` for each `i`), is equal to the sum of the values of `f` at `(g_1(r 1), ..., g_n(r n))`, where `r` ranges over all functions such that `r i` is in `A_i` for each `i`. This property is a consequence of multilinearity, and it involves expanding successively with respect to each coordinate.
Here, `f` is a map from the tensor product of a module `M` over a semiring `R` (indexed by type `ι`) to a module `N` over the same semiring. The functions `g_i` map elements of some type `α i` to `M`. The sets `A_i` are finite sets of elements of type `α i`. The theorem involves notions from ring theory, module theory, and topology.
More concisely: For a continuous alternating map `f` from the tensor product of a module over a semiring to another module, the value of `f` at the finite sum of images of functions `g_i` is equal to the sum of the values of `f` at the images of functions `g_i` for all functions `r` mapping each domain `A_i` into `A_i`.
|