Documentation

TauCeti.RingTheory.SimpleModule.Isotypic

Hom spaces and direct sums of isotypic components #

Mathlib shows that the isotypic components of a module are independent (sSupIndep_isotypicComponents) and, for a semisimple module, span it (sSup_isotypicComponents); it reads off the consequence for endomorphisms (IsSemisimpleModule.endAlgEquiv). This file records the consequence for the module itself: a semisimple module is the internal direct sum of its isotypic components. When there are finitely many components, for instance when the module is Noetherian, composing with DFinsupp.linearEquivFunOnFintype presents it as their product.

Maps from a simple module S into M land in its S-isotypic component. Restricting the codomain therefore gives an equivalence of hom spaces, without any semisimplicity or finiteness assumption on M.

Main definitions #

Main statements #

source
@[simp]
theorem TauCeti.isotypicComponent_self_eq_top {R : Type u_1} {S : Type u_3} [Ring R] [AddCommGroup S] [Module R S] :
isotypicComponent R S S = ⊤

A module is its own isotypic component: the top submodule is isomorphic to the module.

source
theorem LinearMap.apply_mem_isotypicComponent {R : Type u_1} {M : Type u_2} {S : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup S] [Module R S] [IsSimpleModule R S] (f : S →ₗ[R] M) (s : S) :
f s ∈ isotypicComponent R M S

A map out of a simple module takes its values in the isotypic component of that type.

source
def TauCeti.linearMapIsotypicComponentEquiv {R : Type u_1} {M : Type u_2} {S : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup S] [Module R S] [IsSimpleModule R S] (k : Type u_4) [CommSemiring k] [Algebra k R] [Module k M] [IsScalarTower k R M] :
(S →ₗ[R] ↥(isotypicComponent R M S)) ≃ₗ[k] S →ₗ[R] M

Composition with the inclusion of the S-isotypic component is an equivalence of hom spaces out of the simple module S. Its inverse corestricts a map to that component. The equivalence is linear over the scalar semiring acting on the target.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem TauCeti.linearMapIsotypicComponentEquiv_apply {R : Type u_1} {M : Type u_2} {S : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup S] [Module R S] [IsSimpleModule R S] (k : Type u_4) [CommSemiring k] [Algebra k R] [Module k M] [IsScalarTower k R M] (f : S →ₗ[R] ↥(isotypicComponent R M S)) (s : S) :
    ((linearMapIsotypicComponentEquiv k) f) s = ↑(f s)

    The forward equivalence composes a map into the isotypic component with its inclusion into the ambient module.

    source
    @[simp]
    theorem TauCeti.linearMapIsotypicComponentEquiv_symm_apply {R : Type u_1} {M : Type u_2} {S : Type u_3} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup S] [Module R S] [IsSimpleModule R S] (k : Type u_4) [CommSemiring k] [Algebra k R] [Module k M] [IsScalarTower k R M] (f : S →ₗ[R] M) (s : S) :
    ((linearMapIsotypicComponentEquiv k).symm f) s = ⟨f s, ⋯⟩

    The inverse equivalence corestricts a map into the ambient module to its isotypic component, preserving its values.

    source
    noncomputable def TauCeti.IsSemisimpleModule.linearEquivIsotypicComponents (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [DecidableEq ↑(isotypicComponents R M)] :
    M ≃ₗ[R] Π₀ (c : ↑(isotypicComponents R M)), ↥↑c

    A semisimple module is the direct sum of its isotypic components. The equivalence sends an element to its family of components, and its inverse adds the components up. This is the module-level counterpart of IsSemisimpleModule.endAlgEquiv.

    Equations
    Instances For
      source
      @[simp]
      theorem TauCeti.IsSemisimpleModule.linearEquivIsotypicComponents_symm_single {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [DecidableEq ↑(isotypicComponents R M)] (c : ↑(isotypicComponents R M)) (x : ↥↑c) :
      (linearEquivIsotypicComponents R M).symm (DFinsupp.single c x) = ↑x

      The inverse of linearEquivIsotypicComponents sends the family that is x at the isotypic component c and zero elsewhere to x, viewed as an element of M.

      source
      @[simp]
      theorem TauCeti.IsSemisimpleModule.linearEquivIsotypicComponents_apply_coe {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [DecidableEq ↑(isotypicComponents R M)] {c : ↑(isotypicComponents R M)} (x : ↥↑c) :
      (linearEquivIsotypicComponents R M) ↑x = DFinsupp.single c x

      linearEquivIsotypicComponents sends an element x of an isotypic component c, viewed as an element of M, to the family that is x at c and zero elsewhere.

      source
      theorem TauCeti.IsSemisimpleModule.linearEquivIsotypicComponents_apply_of_mem {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [DecidableEq ↑(isotypicComponents R M)] {c : ↑(isotypicComponents R M)} {x : M} (hx : x ∈ ↑c) :
      (linearEquivIsotypicComponents R M) x = DFinsupp.single c ⟨x, hx⟩

      An element x of M lying in an isotypic component c is sent by linearEquivIsotypicComponents to the family that is x at c and zero elsewhere.