LinearMap.trace_eq_contract_of_basis'
theorem LinearMap.trace_eq_contract_of_basis' :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
[inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Basis ι R M),
LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquivOfBasis b).symm
This theorem states that for any commutative ring `R`, any `AddCommGroup` instance `M`, and any `Module` structure on `R` and `M`, for a finite type `ι` with decidable equality, and a basis `b` of `M` over `R` indexed by `ι`, the trace of a linear map is equal to the composition of the contraction pairing and the inverse of the isomorphism from the dual tensor space to the space of endomorphisms. In other words, this establishes a correspondence between the trace of a linear map and the contraction pairing under the isomorphism between the space of endomorphisms and the tensor product of the dual module and the original module.
More concisely: For any commutative ring `R`, `AddCommGroup` `M`, and `Module` structure on `R` and `M`, given a finite type `ι` with decidable equality, a basis `b` of `M` over `R` indexed by `ι`, and a linear map `f : M → M`, the trace of `f` is equal to the composition of the contraction pairing and the inverse of the isomorphism from `M⊤ ⊗ M` to `End(M)`.
|
LinearMap.trace_eq_contract'
theorem LinearMap.trace_eq_contract' :
∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : Module.Finite R M],
LinearMap.trace R M = contractLeft R M ∘ₗ ↑(dualTensorHomEquiv R M M).symm
The theorem `LinearMap.trace_eq_contract'` states that for a commutative ring `R` and an `R`-module `M` that is both free and finite, the trace of a linear map is equal to the contraction pairing under the isomorphism between the endomorphism ring of `M` and the tensor product of the dual of `M` with `M` itself. In other words, this theorem establishes a connection between the trace of a linear map and the contraction pairing in the context of finite free modules.
More concisely: For a commutative ring R and a finite free R-module M, the trace of a linear map is equal to the contraction pairing under the isomorphism between the endomorphism ring of M and M⊗ⁱⁱ(Mⁱⁱ)⁰.
|
LinearMap.trace_conj
theorem LinearMap.trace_conj :
∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (g : M →ₗ[R] M)
(f : (M →ₗ[R] M)ˣ), (LinearMap.trace R M) (↑f * g * ↑f⁻¹) = (LinearMap.trace R M) g
The theorem `LinearMap.trace_conj` states that for any commutative semiring `R`, any add-commutative monoid `M` which is also a module over `R`, and for any linear maps `g` and `f` from `M` to `M`, where `f` is invertible, the trace of the endomorphism `g` is invariant under conjugation by `f`. This means that conjugating `g` by `f` (i.e., computing `f * g * f⁻¹` where `*` denotes composition of functions and `f⁻¹` is the inverse of `f`) does not change the trace of `g`. This is a property of the trace that is familiar from linear algebra.
More concisely: For any commutative semiring R, add-commutative R-module M, invertible linear map f : M -> M, and linear maps g, f(g)tr(g) = tr(g), where tr denotes the trace function.
|
LinearMap.trace_mul_comm
theorem LinearMap.trace_mul_comm :
∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(f g : M →ₗ[R] M), (LinearMap.trace R M) (f * g) = (LinearMap.trace R M) (g * f)
The theorem `LinearMap.trace_mul_comm` states that for any commutative semiring `R` and any module `M` over `R`, the trace of the product of two linear maps `f` and `g` is the same as the trace of the product of `g` and `f`. In other words, the trace of the composition of two linear maps is commutative. In mathematical terms, this can be written as $\text{Tr}(f \circ g) = \text{Tr}(g \circ f)$, where $\text{Tr}$ denotes the trace of a linear map.
More concisely: For any commutative semiring R and module M over R, the trace of the product of two linear maps f and g is commutative, that is, Tr(fg) = Tr(gf).
|
LinearMap.trace_id
theorem LinearMap.trace_id :
∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : Module.Finite R M],
(LinearMap.trace R M) LinearMap.id = ↑(FiniteDimensional.finrank R M)
This theorem states that for any commutative ring `R` and any free `R`-module `M` that is finitely-generated, the trace of the identity endomorphism on `M` is equal to the rank (as a natural number) of `M`. In other words, the trace of the identity linear map (which is a linear transformation that leaves every element of the module unchanged) is equal to the dimension of the module over the ring. This is an important concept in linear algebra that connects the dimensions of a vector space (or more generally, a module) with the trace of the identity endomorphism.
More concisely: For any commutative ring `R` and finitely-generated free `R`-module `M`, the trace of the identity endomorphism on `M` equals the rank (or dimension) of `M` as a natural number.
|
LinearMap.trace_eq_contract
theorem LinearMap.trace_eq_contract :
∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : Module.Finite R M],
LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
The theorem `LinearMap.trace_eq_contract` states that for any commutative ring `R` and any module `M` over `R` which is both free and finite, the composition of the trace of a linear map and the natural map associating a linear map to the tensor product of two modules is equal to the contraction pairing under the isomorphism `End(M) ≃ M* ⊗ M`. In other words, the trace of a linear endomorphism in a finite free module `M` can be expressed as a contraction pairing under the natural isomorphism between the endomorphisms of `M` and the tensor product of `M` with its dual.
More concisely: For any commutative ring R and a free and finite R-module M, the trace of a linear endomorphism of M equals the contraction pairing under the natural isomorphism of End(M) with M ⊗ M\*.
|
LinearMap.trace_one
theorem LinearMap.trace_one :
∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : Module.Finite R M],
(LinearMap.trace R M) 1 = ↑(FiniteDimensional.finrank R M)
The theorem `LinearMap.trace_one` states that for any commutative ring `R` and any `R`-module `M` that is both free and finite, the trace of the identity endomorphism on `M` is equal to the dimension (rank) of the free module `M`. In essence, this means the trace of the identity map, which essentially counts the number of basis vectors, is equal to the dimension of the vector space or module.
More concisely: For any commutative ring R and free finite R-module M, the trace of the identity endomorphism on M equals the rank (or dimension) of M.
|
LinearMap.trace_eq_contract_of_basis
theorem LinearMap.trace_eq_contract_of_basis :
∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_5}
[inst_3 : Finite ι], Basis ι R M → LinearMap.trace R M ∘ₗ dualTensorHom R M M = contractLeft R M
This theorem states that for any commutative ring `R`, any module `M` over `R`, and any finite type `ι`, if there is a basis of `M` indexed by `ι`, then the composition of the trace of a linear map and the natural map associating a linear map to the tensor product of two modules corresponds to the natural left-handed pairing between a module and its dual. This is realized under the isomorphism between the endomorphisms of `M` and the tensor product of the dual of `M` and `M` itself. In other words, the trace of a linear map can be understood as a contraction pairing in the language of tensor products.
More concisely: For any commutative ring `R`, any `R`-module `M` with a finite basis, and any linear map `f : M → M`, the trace of `f` is equal to the natural pairing between `M` and its dual, realized under the isomorphism between endomorphisms of `M` and `M ⊗ᵢ Mⁱ⁊ᵢ⁇`.
|
LinearMap.trace_eq_matrix_trace_of_finset
theorem LinearMap.trace_eq_matrix_trace_of_finset :
∀ (R : Type u) [inst : CommSemiring R] {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Finset M}
(b : Basis { x // x ∈ s } R M) (f : M →ₗ[R] M), (LinearMap.trace R M) f = ((LinearMap.toMatrix b b) f).trace
This theorem, named `LinearMap.trace_eq_matrix_trace_of_finset`, states that for any commutative semiring `R` and any additive commutative monoid `M` that is also an `R`-module, given a finite set `s` of `M`, a basis `b` for `M` over `R` constructed from elements in `s`, and a linear map `f` from `M` to `M`, the trace of `f` (as defined by `LinearMap.trace`) equals the trace of the matrix representation of `f` with respect to the basis `b` (as given by `(LinearMap.toMatrix b b) f).trace`). Essentially, this theorem establishes the correspondence between the trace of a linear map and the trace of its matrix representation, ensuring that the trace is independent of the chosen basis.
More concisely: For any commutative semiring R, additive commutative monoid M that is an R-module, finite set s of M, basis b for M over R from s, and linear map f from M to M, the trace of f (as a linear map) equals the trace of its matrix representation with respect to basis b.
|