# Finite modules and types with finitely many elements #

This file relates `Module.Finite` and `_root_.Finite`.

source
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), LinearMap.range f = N
source
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
source
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
source
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.

source
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`).

source
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
source
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.

source
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
source
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.

source
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
source
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.

Equations

- Module.Finite.kerRepr R M = LinearMap.ker ⋯.choose

Instances For

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

Equations

- Module.Finite.repr R M = ((Fin ⋯.choose → R) ⧸ Module.Finite.kerRepr R M)

Instances For

source
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.

Equations

- Module.Finite.reprEquiv R M = ⋯.choose.quotKerEquivOfSurjective ⋯

Instances For

source
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.

Equations

- Module.Finite.kerReprₛ R M = ModuleCon.ker ⋯.choose.toDistribMulActionHom

Instances For

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

Equations

- Module.Finite.reprₛ R M = ModuleCon.Quotient (Fin ⋯.choose → R) (Module.Finite.kerReprₛ R M)

Instances For

source
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.

Equations

- Module.Finite.reprEquivₛ R M = ModuleCon.quotientKerEquivOfSurjective ⋯.choose ⋯

Instances For