Modules over an algebra acting on S as all of End S

Let k be a commutative semiring, S a finite projective k-module, and A a k-algebra acting on S so that the action map Algebra.lsmul k k S : A →ₐ[k] Module.End k S is bijective: A is the endomorphism algebra of S. This is the situation of an irreducible module over a central simple algebra that is split, for instance of the spinor module S of an even-dimensional complex Clifford algebra Cℓ(V) ≃ End(S).

Then every A-module M is S tensored with its multiplicity space S →ₗ[A] M: evaluation

TauCeti.isotypicEval k : S ⊗[k] (S →ₗ[A] M) →ₗ[A] M, s ⊗ T ↦ T s,

is an isomorphism of A-modules (TauCeti.isotypicTensorEquivOfBijective). Nothing is assumed of M: it need not be finite, free or semisimple, and k need not be a field or even a ring. Nor is S asked to be nonzero: for S = 0 the algebra A is zero and so is every A-module. This is one half of the Morita correspondence for S: the counit S ⊗[k] (S →ₗ[A] M) → M is an isomorphism; the unit X → S →ₗ[A] (S ⊗[k] X) is not treated here. When S is also a generator (for instance nonzero over a field), the two functors X ↦ S ⊗[k] X and M ↦ S →ₗ[A] M give a Morita equivalence between k and End_k S.

The inverse is explicit. A linear form φ on S and a vector x : M give the A-linear map TauCeti.homOfDual h φ x : S →ₗ[A] M sending s to a • x, where a ∈ A acts on S as the rank-one endomorphism t ↦ φ t • s. For a basis (eᵢ) of S with coordinate forms (eᵢ*) these are matrix units, and the inverse of evaluation is x ↦ ∑ᵢ eᵢ ⊗ homOfDual h eᵢ* x (TauCeti.isotypicTensorEquivOfBijective_symm_apply_basis). The identity behind both inverse laws is homOfDual h φ (T s) = φ s • T for every A-linear T (TauCeti.homOfDual_apply_map), the matrix-unit relation Eᵢⱼ T(eⱼ) = T(eᵢ).

Main definitions

• TauCeti.homOfDual: the element of the multiplicity space attached to a linear form on S and a vector of M.
• TauCeti.isotypicTensorEquivOfBijective: evaluation S ⊗[k] (S →ₗ[A] M) ≃ₗ[A] M.

Main results

• TauCeti.isotypicEval_bijective_of_bijective_lsmul: evaluation is bijective.
• TauCeti.isotypicTensorEquivOfBijective_symm_apply and TauCeti.isotypicTensorEquivOfBijective_symm_apply_basis: the inverse, for a finite family ∑ᵢ φᵢ(t) vᵢ = t and for a finite basis.
• TauCeti.isotypicTensorEquivOfBijective_symm_apply_map: naturality of the inverse in M; naturality of evaluation itself is TauCeti.isotypicEval_map_apply.
• TauCeti.finrank_eq_finrank_mul_finrank_linearMap_of_bijective_lsmul: over a field, dim M = dim S · dim (S →ₗ[A] M).

Implementation notes

Evaluation is the map TauCeti.isotypicEval already used for isotypic components of semisimple modules, where its injectivity is proved for S simple and finite-dimensional over an algebraically closed field (TauCeti.isotypicEval_injective). Here the hypothesis on A replaces these assumptions, and the inverse is written down directly: a finite projective S has a finite family with ∑ᵢ φᵢ(t) vᵢ = t, because the identity of S lies in the range of Mathlib's dualTensorHom (dualTensorHom_bijective).

References

• T. Y. Lam, Lectures on Modules and Rings, GTM 189 (1999), Chapter 7.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §5.

The matrix units attached to linear forms

@[simp]

theorem TauCeti.ofBijective_lsmul_symm_smul {k : Type u_1} {A : Type u_2} {S : Type u_3} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) (f : Module.End k S) (s : S) : (AlgEquiv.ofBijective (Algebra.lsmul k k S) h).symm f • s = f s

The element of A acting as an endomorphism f of S acts on a vector by f.

noncomputable def TauCeti.homOfDual {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) (φ : Module.Dual k S) : M →ₗ[k] S →ₗ[A] M

For A ≅ End_k S, a linear form φ on S and a vector x : M, the A-linear map S →ₗ[A] M sending s to a • x, where a ∈ A acts on S as the rank-one endomorphism t ↦ φ t • s. For a basis of S and φ a coordinate form, these elements of A are matrix units, and homOfDual assembles the inverse of evaluation.

@[simp]

theorem TauCeti.homOfDual_apply_apply {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) (φ : Module.Dual k S) (x : M) (s : S) : ((homOfDual h φ) x) s = (AlgEquiv.ofBijective (Algebra.lsmul k k S) h).symm (LinearMap.smulRight φ s) • x

The value of homOfDual h φ x at s is x acted on by the preimage in A of the rank-one endomorphism t ↦ φ t • s.

@[simp]

theorem TauCeti.homOfDual_apply_map {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) (φ : Module.Dual k S) (T : S →ₗ[A] M) (s : S) : (homOfDual h φ) (T s) = φ s • T

The matrix-unit relation. On a value of an A-linear map T, homOfDual returns T itself, scaled by φ s; for a basis (eᵢ) this is Eᵢⱼ T(eⱼ) = T(eᵢ).

Evaluation is an isomorphism

theorem TauCeti.isotypicEval_bijective_of_bijective_lsmul {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) [Module.Finite k S] [Module.Projective k S] : Function.Bijective ⇑(isotypicEval k)

Evaluation is bijective when A acts on the finite projective module S as the whole endomorphism algebra End_k S: every A-module M is S ⊗[k] (S →ₗ[A] M).

theorem TauCeti.sum_homOfDual_coord_apply {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) {ι : Type u_6} [Fintype ι] (b : Module.Basis ι k S) (x : M) : ∑ i : ι, ((homOfDual h (b.coord i)) x) (b i) = x

A finite basis of S reconstructs every vector of an A-module from its multiplicity components homOfDual h (b.coord i) x.

noncomputable def TauCeti.isotypicTensorEquivOfBijective {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) [Module.Finite k S] [Module.Projective k S] : TensorProduct k S (S →ₗ[A] M) ≃ₗ[A] M

Every module over A ≅ End_k S is S tensored with its multiplicity space. Evaluation s ⊗ T ↦ T s is an isomorphism of A-modules S ⊗[k] (S →ₗ[A] M) ≃ₗ[A] M, with A acting on the left factor.

@[simp]

theorem TauCeti.isotypicTensorEquivOfBijective_apply {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) [Module.Finite k S] [Module.Projective k S] (x : TensorProduct k S (S →ₗ[A] M)) : (isotypicTensorEquivOfBijective h) x = (isotypicEval k) x

The equivalence is evaluation, s ⊗ T ↦ T s.

theorem TauCeti.isotypicTensorEquivOfBijective_symm_apply {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) [Module.Finite k S] [Module.Projective k S] {ι : Type u_6} (s : Finset ι) (φ : ι → Module.Dual k S) (v : ι → S) (hv : ∀ (t : S), ∑ i ∈ s, (φ i) t • v i = t) (x : M) : (isotypicTensorEquivOfBijective h).symm x = ∑ i ∈ s, v i ⊗ₜ[k] (homOfDual h (φ i)) x

The inverse of evaluation, for any finite family with ∑ᵢ φᵢ(t) vᵢ = t.

theorem TauCeti.isotypicTensorEquivOfBijective_symm_apply_basis {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) [Module.Finite k S] [Module.Projective k S] {ι : Type u_6} [Fintype ι] (b : Module.Basis ι k S) (x : M) : (isotypicTensorEquivOfBijective h).symm x = ∑ i : ι, b i ⊗ₜ[k] (homOfDual h (b.coord i)) x

The inverse of evaluation in a basis (eᵢ) of S: x ↦ ∑ᵢ eᵢ ⊗ homOfDual h eᵢ* x.

@[simp]

theorem TauCeti.isotypicTensorEquivOfBijective_symm_apply_map {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [CommSemiring k] [Semiring A] [Algebra k A] [AddCommMonoid S] [Module k S] [Module A S] [IsScalarTower k A S] [AddCommMonoid M] [Module k M] [Module A M] [IsScalarTower k A M] [AddCommMonoid N] [Module k N] [Module A N] [IsScalarTower k A N] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) [Module.Finite k S] [Module.Projective k S] (g : M →ₗ[A] N) (y : M) : (isotypicTensorEquivOfBijective h).symm (g y) = (TensorProduct.AlgebraTensorModule.map LinearMap.id (LinearMap.compRight k g)) ((isotypicTensorEquivOfBijective h).symm y)

Naturality of the inverse: through the decomposition an A-linear map g : M →ₗ[A] N becomes 1 ⊗ (g ∘ ·).

theorem TauCeti.finrank_eq_finrank_mul_finrank_linearMap_of_bijective_lsmul {k : Type u_1} {A : Type u_2} {S : Type u_3} {M : Type u_4} [Field k] [Semiring A] [Algebra k A] [AddCommGroup S] [Module k S] [Module A S] [IsScalarTower k A S] [FiniteDimensional k S] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] (h : Function.Bijective ⇑(Algebra.lsmul k k S)) : Module.finrank k M = Module.finrank k S * Module.finrank k (S →ₗ[A] M)

The dimension of a module over A ≅ End_k S is the dimension of S times that of its multiplicity space.