Minimum Cardinality of generating set of a submodule

In this file, we define the minimum cardinality of a generating set for a submodule, which is implemented as spanFinrank and spanRank. spanFinrank takes value in ℕ and equals 0 when no finite generating set exists. spanRank takes value as a cardinal.

Main Definitions

• spanFinrank: The minimum cardinality of a generating set of a submodule as a natural number. If no finite generating set exists, it is defined to be 0.
• spanRank: The minimum cardinality of a generating set of a submodule as a cardinal.
• FG.generators: For a finitely generated submodule, get a set of generating elements with minimal cardinality.

Main Results

• FG.exists_span_set_card_eq_spanFinrank : Any submodule has a generating set of cardinality equal to spanRank.

• rank_eq_spanRank_of_free : For a ring R (not necessarily commutative) satisfying StrongRankCondition R, if M is a free R-module, then the spanRank of M equals to the rank of M.

• rank_le_spanRank : For a ring R (not necessarily commutative) satisfying StrongRankCondition R, if M is an R-module, then the spanRank of M is less than or equal to the rank of M.

Tags

submodule, generating subset, span rank

Remark

Note that the corresponding API - Module.rank is only defined for a module rather than a submodule, so there is some asymmetry here. Further refactoring might be needed if this difference creates a friction later on.

noncomputable def Submodule.spanRank {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Cardinal.{u}

The minimum cardinality of a generating set of a submodule as a cardinal.

noncomputable def Submodule.spanFinrank {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : ℕ

The minimum cardinality of a generating set of a submodule as a natural number. If no finite generating set exists, the span rank is defined to be 0.

instance Submodule.instNonemptySubtypeSetEqSpan {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Nonempty { s : Set M // span R s = p }

theorem Submodule.spanRank_toENat_eq_iInf_encard {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Cardinal.toENat p.spanRank = ⨅ (s : Set M), ⨅ (_ : span R s = p), s.encard

theorem Submodule.spanRank_toENat_eq_iInf_finset_card {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Cardinal.toENat p.spanRank = ⨅ (s : { s : Finset M // span R ↑s = p }), ↑(↑s).card

theorem Submodule.spanFinrank_eq_iInf {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : p.spanFinrank = ⨅ (s : { s : Finset M // span R ↑s = p }), (↑s).card

@[simp]

theorem Submodule.spanRank_finite_iff_fg {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} : p.spanRank < Cardinal.aleph0 ↔ p.FG

A submodule's spanRank is finite if and only if it is finitely generated.

theorem Submodule.fg_iff_spanRank_eq_spanFinrank {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} : p.spanRank = ↑p.spanFinrank ↔ p.FG

A submodule is finitely generated if and only if its spanRank is equal to its spanFinrank.

theorem Submodule.spanRank_span_le_card {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : (span R s).spanRank ≤ Cardinal.mk ↑s

theorem Submodule.spanFinrank_span_le_ncard_of_finite {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {s : Set M} (hs : s.Finite) : (span R s).spanFinrank ≤ s.ncard

theorem Submodule.exists_span_set_card_eq_spanRank {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : ∃ (s : Set M), Cardinal.mk ↑s = p.spanRank ∧ span R s = p

Constructs a generating set with cardinality equal to the spanRank of the submodule

theorem Submodule.FG.exists_span_set_encard_eq_spanFinrank {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : p.FG) : ∃ (s : Set M), s.encard = ↑p.spanFinrank ∧ span R s = p

Constructs a generating set with cardinality equal to the spanFinrank of the submodule when the submodule is finitely generated.

theorem Submodule.FG.spanRank_le_iff_exists_span_set_card_le {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) {a : Cardinal.{u}} : p.spanRank ≤ a ↔ ∃ (s : Set M), Cardinal.mk ↑s ≤ a ∧ span R s = p

For a finitely generated submodule, its spanRank is less than or equal to a cardinal a if and only if there is a generating subset with cardinality less than or equal to a.

@[simp]

theorem Submodule.spanRank_eq_zero_iff_eq_bot {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {I : Submodule R M} : I.spanRank = 0 ↔ I = ⊥

@[simp]

theorem Submodule.spanRank_bot {R : Type u_1} [Semiring R] : spanRank ⊥ = 0

noncomputable def Submodule.generators {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Set M

Generating elements for the submodule of minimum cardinality.

theorem Submodule.generators_card {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : Cardinal.mk ↑p.generators = p.spanRank

theorem Submodule.FG.generators_ncard {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (h : p.FG) : p.generators.ncard = p.spanFinrank

theorem Submodule.FG.finite_generators {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {p : Submodule R M} (hp : p.FG) : p.generators.Finite

theorem Submodule.span_generators {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : span R p.generators = p

The span of the generators equals the submodule.

theorem Submodule.FG.generators_mem {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] (p : Submodule R M) : p.generators ⊆ ↑p

The elements of the generators are in the submodule.

theorem Submodule.spanRank_sup_le_sum_spanRank {R : Type u_1} {M : Type u} [Semiring R] [AddCommMonoid M] [Module R M] {p q : Submodule R M} : (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank

theorem Module.Basis.mk_eq_spanRank {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [RankCondition R] {ι : Type u_1} (v : Basis ι R M) : Cardinal.mk ↑(Set.range ⇑v) = ⊤.spanRank

theorem Submodule.rank_eq_spanRank_of_free {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [StrongRankCondition R] : Module.rank R M = ⊤.spanRank

theorem Submodule.rank_le_spanRank {R : Type u} {M : Type v} [Semiring R] [AddCommMonoid M] [Module R M] [StrongRankCondition R] : Module.rank R M ≤ ⊤.spanRank