Basis.ext_multilinear_fin
theorem Basis.ext_multilinear_fin :
∀ {R : Type u_1} {n : ℕ} {M : Fin n → Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
[inst_2 : (i : Fin n) → AddCommMonoid (M i)] [inst_3 : (i : Fin n) → Module R (M i)] [inst_4 : Module R M₂]
{f g : MultilinearMap R M M₂} {ι₁ : Fin n → Type u_6} (e : (i : Fin n) → Basis (ι₁ i) R (M i)),
(∀ (v : (i : Fin n) → ι₁ i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)) → f = g
The theorem `Basis.ext_multilinear_fin` states that for any two multilinear maps `f` and `g` from a finite set `Fin n` to a space `M`, if they are equal when evaluated on all basis vectors of `M`, then `f` and `g` are equal. The conditions required are that the coefficients are from a commutative semiring `R`, the map `M` is an `AddCommMonoid`, each space `M i` is an `AddCommMonoid`, and every `M i` and `M₂` are `R`-modules.
More concisely: If two multilinear maps from a finite set to an additive commutative monoid endowed with an Abelian group structure and an R-module structure, with coefficients from a commutative semiring, agree on all basis vectors, then they are equal.
|
Basis.ext_multilinear
theorem Basis.ext_multilinear :
∀ {R : Type u_1} {ι : Type u_2} {M₂ : Type u_4} {M₃ : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
[inst_2 : AddCommMonoid M₃] [inst_3 : Module R M₂] [inst_4 : Module R M₃] [inst_5 : Finite ι]
{f g : MultilinearMap R (fun x => M₂) M₃} {ι₁ : Type u_6} (e : Basis ι₁ R M₂),
(∀ (v : ι → ι₁), (f fun i => e (v i)) = g fun i => e (v i)) → f = g
The theorem `Basis.ext_multilinear` states that for any commutative semiring `R`, types `ι`, `M₂`, and `M₃`, given two multilinear maps `f` and `g` from `M₂` to `M₃` indexed by a finite set `ι`, and a basis `e` for `M₂`, if `f` and `g` are equal when evaluated at every basis vector of `M₂`, then `f` and `g` are equal. This is a version of `Basis.ext_multilinear_fin` that only uses a single basis; a dependently-typed version would still hold true, but its proof would require a dependently-typed version of `dom_dom_congr`.
More concisely: Given a commutative semiring R, types ι, M₂, and M₃, a finite set ι, a multilinear map f from M₂ to M₃ indexed by ι, a multilinear map g from M₂ to M₃ indexed by ι, and a basis e for M₂, if f and g agree on every basis vector, then f = g.
|