LinearMap.ext_basis
theorem LinearMap.ext_basis :
∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {R : Type u_3} {R₂ : Type u_4} {S : Type u_5} {S₂ : Type u_6} {M : Type u_7}
{N : Type u_8} {P : Type u_9} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring R₂]
[inst_3 : Semiring S₂] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
[inst_7 : Module R M] [inst_8 : Module S N] [inst_9 : Module R₂ P] [inst_10 : Module S₂ P]
[inst_11 : SMulCommClass S₂ R₂ P] {ρ₁₂ : R →+* R₂} {σ₁₂ : S →+* S₂} (b₁ : Basis ι₁ R M) (b₂ : Basis ι₂ S N)
{B B' : M →ₛₗ[ρ₁₂] N →ₛₗ[σ₁₂] P}, (∀ (i : ι₁) (j : ι₂), (B (b₁ i)) (b₂ j) = (B' (b₁ i)) (b₂ j)) → B = B'
The theorem `LinearMap.ext_basis` states that if you have two bilinear maps `B` and `B'` from a vector space `M` over a ring `R` to another vector space `N` over a ring `S` and then to a vector space `P` over rings `R₂` and `S₂`, then they are equal if they produce the same result for all combinations of basis vectors from `M` and `N`. Specifically, for every basis vector `i` from `M` and every basis vector `j` from `N`, if `B` at `b₁ i` applied to `b₂ j` is equal to `B'` at `b₁ i` applied to `b₂ j`, then `B` and `B'` are equal.
More concisely: If two bilinear maps from vector spaces over rings to another vector space over rings agree on all basis vector pairs, then they are equal.
|
LinearMap.sum_repr_mul_repr_mul
theorem LinearMap.sum_repr_mul_repr_mul :
∀ {ι₁ : Type u_1} {ι₂ : Type u_2} {Rₗ : Type u_10} {Mₗ : Type u_11} {Nₗ : Type u_12} {Pₗ : Type u_13}
[inst : CommSemiring Rₗ] [inst_1 : AddCommMonoid Mₗ] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ]
[inst_4 : Module Rₗ Mₗ] [inst_5 : Module Rₗ Nₗ] [inst_6 : Module Rₗ Pₗ] (b₁' : Basis ι₁ Rₗ Mₗ)
(b₂' : Basis ι₂ Rₗ Nₗ) {B : Mₗ →ₗ[Rₗ] Nₗ →ₗ[Rₗ] Pₗ} (x : Mₗ) (y : Nₗ),
((b₁'.repr x).sum fun i xi => (b₂'.repr y).sum fun j yj => xi • yj • (B (b₁' i)) (b₂' j)) = (B x) y
The theorem `LinearMap.sum_repr_mul_repr_mul` asserts that for any types `ι₁`, `ι₂`, `Rₗ`, `Mₗ`, `Nₗ`, and `Pₗ`, given that `Rₗ` is a commutative semiring and `Mₗ`, `Nₗ`, and `Pₗ` are additive commutative monoids that are also modules over `Rₗ`, and given bases `b₁'` and `b₂'` for `Mₗ` and `Nₗ` respectively, and a bilinear map `B`, for any elements `x` in `Mₗ` and `y` in `Nₗ`, the result of applying `B` to `x` and `y` is equal to the sum over all elements of the first basis scaled by `x` and elements of the second basis scaled by `y` of the scaled elements of `B` applied to the basis elements. This theorem essentially provides a way to write the result of a bilinear map as a sum over the basis elements.
More concisely: For any commutative semiring `R`, additive commutative monoids `M` and `N` that are `R`-modules, bilinear map `B` between them, and bases `b₁` and `b₂` of `M` and `N` respectively, the application of `B` to any elements `x in M` and `y in N` equals the sum over `i` in the first basis and `j` in the second basis of the product of `x` with the i-th element of the first basis, the product of `y` with the j-th element of the second basis, and the application of `B` to the corresponding basis elements.
|