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

• Submodule.CoFG expresses that a submodule is co-finitely generated.

@[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.

@[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.

@[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.

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.

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.

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.

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.

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.

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.

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.

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.

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.