Documentation

Mathlib.RingTheory.Finiteness.Cofinite

Co-finitely generated submodules #

This files defines the notion of a co-finitely generated submodule. A submodule S of a module M is co-finitely generated (or CoFG for short) if the quotient of M by S is finitely generated (i.e. FG).

Main declarations #

source
@[reducible, inline]
abbrev Submodule.CoFG {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] (S : Submodule R M) :
Prop

A submodule S of a module M is co-finitely generated (CoFG) if the quotient space M ⧸ S is finitely generated.

Equations
Instances For
    source
    @[simp]
    theorem Submodule.CoFG.of_finite {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [Module.Finite R M] {S : Submodule R M} :
    S.CoFG

    A submodule of a finite module is CoFG.

    source
    @[simp]
    theorem Submodule.CoFG.top {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] :
    ⊤.CoFG

    The top submodule is CoFG.

    source
    theorem Module.Finite.iff_cofg_bot (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] :
    ⊥.CoFG ↔ Module.Finite R M

    A module is finite if and only if the bottom submodule is CoFG.

    source
    theorem Submodule.CoFG.fg_of_isCompl {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {S T : Submodule R M} (hST : IsCompl S T) (hS : S.CoFG) :
    T.FG

    A complement of a CoFG submodule is FG.

    source
    theorem Submodule.FG.cofg_of_isCompl {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {S T : Submodule R M} (hST : IsCompl S T) (hS : S.FG) :
    T.CoFG

    A complement of an FG submodule is CoFG.

    source
    theorem Submodule.CoFG.of_cofg_le {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {S T : Submodule R M} (hT : S ≤ T) (hS : S.CoFG) :
    T.CoFG

    A submodule that contains a CoFG submodule is CoFG.

    source
    theorem Submodule.range_fg_iff_ker_cofg {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] {f : M →ₗ[R] N} :
    f.range.FG ↔ f.ker.CoFG

    The range of a linear map is FG if and only if the kernel is CoFG.

    source
    theorem Submodule.CoFG.ker {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] {N : Type u_3} [AddCommGroup N] [Module R N] [IsNoetherian R N] (f : M →ₗ[R] N) :
    f.ker.CoFG

    The kernel of a linear map into a noetherian module is CoFG.

    source
    theorem Submodule.CoFG.inf {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsNoetherianRing R] {S T : Submodule R M} (hS : S.CoFG) (hT : T.CoFG) :
    (S ⊓ T).CoFG

    Over a noetherian ring the intersection of two CoFG submodules is CoFG.

    source
    theorem Submodule.CoFG.sInf {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsNoetherianRing R] {s : Finset (Submodule R M)} (hs : ∀ S ∈ s, S.CoFG) :
    (sInf ↑s).CoFG

    Over a noetherian ring the infimum of a finite family of CoFG submodules is CoFG.

    source
    theorem Submodule.CoFG.sInf_of_finite {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsNoetherianRing R] {s : Set (Submodule R M)} (hs : s.Finite) (hcofg : ∀ S ∈ s, S.CoFG) :
    (sInf s).CoFG

    Over a noetherian ring the infimum of a finite family of CoFG submodules is CoFG.