Finite modules and types with finitely many elements

This file relates Module.Finite and _root_.Finite.

theorem Submodule.fg_iff_exists_fin_linearMap (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} : N.FG ↔ ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), f.range = N

theorem AddSubmonoid.fg_iff_exists_fin_addMonoidHom {M : Type u_3} [AddCommMonoid M] {S : AddSubmonoid M} : S.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = S

theorem AddSubgroup.fg_iff_exists_fin_addMonoidHom {M : Type u_3} [AddCommGroup M] {H : AddSubgroup M} : H.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℤ) →+ M), f.range = H

theorem Module.Finite.exists_fin' (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Function.Surjective ⇑f

A finite module admits a surjective linear map from a finite free module.

theorem Module.Finite.exists_fin_quot_equiv (R : Type u_3) (M : Type u_4) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : ∃ (n : ℕ) (S : Submodule R (Fin n → R)), Nonempty (((Fin n → R) ⧸ S) ≃ₗ[R] M)

A finite module can be realised as a quotient of Fin n → R (i.e. R^n).

theorem Module.finite_of_finite (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] [Module.Finite R M] : Finite M

theorem Module.finite_iff_finite {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] : Module.Finite R M ↔ Finite M

A module over a finite ring has finite dimension iff it is finite.

theorem Set.Finite.submoduleSpan (R : Type u_1) {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Finite R] {s : Set M} (hs : s.Finite) : (↑(Submodule.span R s)).Finite

theorem Module.Finite.finite_basis {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {ι : Type u_3} [Module.Finite R M] (b : Basis ι R M) : Finite ι

If a free module is finite, then any arbitrary basis is finite.

theorem Module.not_finite_of_infinite_basis {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Nontrivial R] {ι : Type u_3} [Infinite ι] (b : Basis ι R M) : ¬Module.Finite R M

noncomputable def Module.Finite.kerRepr (R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Submodule R (Fin ⋯.choose → R)

The kernel of a random surjective linear map from a finite free module to a given finite module.

@[reducible, inline]

abbrev Module.Finite.repr (R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Type u

A representative of a finite module in the same universe as the ring.

noncomputable def Module.Finite.reprEquiv (R : Type u) (M : Type u_1) [Ring R] [AddCommGroup M] [Module R M] [Module.Finite R M] : Finite.repr R M ≃ₗ[R] M

The representative is isomorphic to the original module.

noncomputable def Module.Finite.kerReprₛ (R : Type u) (M : Type u_1) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : ModuleCon R (Fin ⋯.choose → R)

The kernel (as a congruence relation) of a random surjective linear map from a finite free module to a given finite module.

@[reducible, inline]

abbrev Module.Finite.reprₛ (R : Type u) (M : Type u_1) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Type u

A representative of a finite module in the same universe as the semiring.

noncomputable def Module.Finite.reprEquivₛ (R : Type u) (M : Type u_1) [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] : Finite.reprₛ R M ≃ₗ[R] M

The representative is isomorphic to the original module.