Documentation

TauCeti.RingTheory.Finiteness.LocallyFinite

Locally finite modules over an algebra #

Let A be an algebra over a commutative ring k. An A-module M is locally finite over k when every vector generates an A-submodule that is finitely generated over k. Over a field this says that every cyclic A-submodule is finite-dimensional. Finite-dimensional modules are locally finite, and so are arbitrary direct sums of them, but a locally finite module may have infinite dimension. For a quantized enveloping algebra at a generic parameter, the locally finite modules are exactly the direct sums of finite-dimensional simple modules.

Over a Noetherian base ring k, a module is locally finite as soon as it is the sum of some family of A-submodules that are finitely generated over k. Local finiteness passes to submodules, along injective linear maps and to direct sums. Every simple submodule of a locally finite module, being generated by any of its nonzero vectors, is finitely generated over k. If the A-submodules of a locally finite module that are finitely generated over k are all semisimple, then the module is semisimple.

Main definitions #

Main results #

source
class TauCeti.IsLocallyFiniteModule (k : Type u_1) (A : Type u_2) (M : Type u_3) [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] :
Prop

An A-module M is locally finite over k when the cyclic A-submodule generated by each vector is a finitely generated k-module.

Instances
    source
    theorem TauCeti.isLocallyFiniteModule_iff {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] :
    IsLocallyFiniteModule k A M ↔ ∀ (v : M), (Submodule.restrictScalars k (A ∙ v)).FG

    Local finiteness, phrased with finitely generated k-submodules.

    source
    theorem TauCeti.IsLocallyFiniteModule.fg_restrictScalars_span_singleton {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsLocallyFiniteModule k A M] (v : M) :
    (Submodule.restrictScalars k (A ∙ v)).FG

    The cyclic submodule generated by a vector of a locally finite module is finitely generated over k.

    source
    instance TauCeti.IsLocallyFiniteModule.of_finite {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsNoetherianRing k] [Module.Finite k M] :
    IsLocallyFiniteModule k A M

    A module that is finitely generated over a Noetherian ring k is locally finite.

    source
    theorem TauCeti.IsLocallyFiniteModule.of_injective {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] {N : Type u_4} [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsLocallyFiniteModule k A M] (f : N →ₗ[A] M) (hf : Function.Injective ⇑f) :
    IsLocallyFiniteModule k A N

    Local finiteness passes to a module that maps injectively into a locally finite one.

    source
    instance TauCeti.IsLocallyFiniteModule.submodule {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsLocallyFiniteModule k A M] (N : Submodule A M) :
    IsLocallyFiniteModule k A ↥N

    A submodule of a locally finite module is locally finite.

    source
    theorem TauCeti.IsLocallyFiniteModule.of_linearEquiv {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] {N : Type u_4} [AddCommGroup N] [Module k N] [Module A N] [IsScalarTower k A N] [IsLocallyFiniteModule k A M] (e : N ≃ₗ[A] M) :
    IsLocallyFiniteModule k A N

    Local finiteness is invariant under linear equivalence.

    source
    theorem TauCeti.IsLocallyFiniteModule.of_iSup_eq_top {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsNoetherianRing k] {ι : Type u_4} {p : ι → Submodule A M} (hp : ∀ (i : ι), Module.Finite k ↥(p i)) (htop : ⨆ (i : ι), p i = ⊤) :
    IsLocallyFiniteModule k A M

    Over a Noetherian ring k, an A-module that is the sum of a family of A-submodules finitely generated over k is locally finite.

    source
    instance TauCeti.IsLocallyFiniteModule.dfinsupp {k : Type u_1} {A : Type u_2} [CommRing k] [Ring A] [Algebra k A] [IsNoetherianRing k] {ι : Type u_4} (N : ι → Type u_5) [(i : ι) → AddCommGroup (N i)] [(i : ι) → Module k (N i)] [(i : ι) → Module A (N i)] [∀ (i : ι), IsScalarTower k A (N i)] [∀ (i : ι), IsLocallyFiniteModule k A (N i)] :
    IsLocallyFiniteModule k A (Π₀ (i : ι), N i)

    A direct sum of locally finite modules is locally finite.

    source
    theorem TauCeti.IsLocallyFiniteModule.finite_of_isSimpleModule {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsLocallyFiniteModule k A M] (N : Submodule A M) [IsSimpleModule A ↥N] :
    Module.Finite k ↥N

    A simple submodule of a locally finite module is finitely generated over k, since it is generated by any of its nonzero vectors.

    source
    theorem TauCeti.IsLocallyFiniteModule.isSemisimpleModule {k : Type u_1} {A : Type u_2} {M : Type u_3} [CommRing k] [Ring A] [Algebra k A] [AddCommGroup M] [Module k M] [Module A M] [IsScalarTower k A M] [IsLocallyFiniteModule k A M] (h : ∀ (N : Submodule A M), Module.Finite k ↥N → IsSemisimpleModule A ↥N) :
    IsSemisimpleModule A M

    A locally finite module whose A-submodules that are finite over k are all semisimple is itself semisimple.