Module.Finite.equiv
theorem Module.Finite.equiv :
∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Module.Finite R M], (M ≃ₗ[R] N) → Module.Finite R N
This theorem states that for any two Types `M` and `N`, if `M` is a finite module over a semiring `R`, then if there's a linear equivalence between `M` and `N` (denoted as `M ≃ₗ[R] N`), `N` must also be a finite module over the same semiring `R`. This theorem essentially captures the concept that the property of being a finite module is preserved under linear equivalence.
More concisely: If `M` and `N` are Types, `M` is a finite module over semiring `R`, and `M ≃ₗ[R] N`, then `N` is also a finite module over semiring `R`.
|
Submodule.fg_of_fg_map_of_fg_inf_ker
theorem Submodule.fg_of_fg_map_of_fg_inf_ker :
∀ {R : Type u_4} {M : Type u_5} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
[inst_3 : AddCommGroup P] [inst_4 : Module R P] (f : M →ₗ[R] P) {s : Submodule R M},
(Submodule.map f s).FG → (s ⊓ LinearMap.ker f).FG → s.FG
This theorem states that if we have an exact sequence 0 → M' → M → M'' → 0 and both M' and M'' are finitely generated then M is also finitely generated. In the context of this theorem, R is a ring, and M and P are modules over R. The theorem takes in a linear map `f` from M to P, and a submodule `s` of M. The theorem asserts that if the image of `s` under `f` is finitely generated, and the intersection of `s` and the kernel of `f` is also finitely generated, then `s` is finitely generated.
More concisely: If `0 → M' → M → M'' → 0` is an exact sequence of finitely generated R-modules, then M is also finitely generated (this is the Baer-Mazur theorem for modules). Moreover, if we have a linear map `f` from M to another module P, and `s` is a submodule of M such that the image of `s` under `f` and the intersection of `s` and the kernel of `f` are finitely generated, then `s` is also finitely generated.
|
Module.Finite.of_surjective
theorem Module.Finite.of_surjective :
∀ {R : Type u_1} {M : Type u_4} {N : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : AddCommMonoid N] [inst_4 : Module R N] [hM : Module.Finite R M] (f : M →ₗ[R] N),
Function.Surjective ⇑f → Module.Finite R N
The theorem `Module.Finite.of_surjective` states that for all types `R`, `M`, and `N`, given that `R` is a semiring, `M` and `N` are additive commutative monoids, and `M` and `N` are modules over `R`, if `M` is a finite module, then if there exists a surjective linear map `f` from `M` to `N`, `N` is also a finite module. Here, a function `f` is surjective if for every element of `N`, there exists an element of `M` such that applying `f` on this element of `M` gives the element of `N`. A finite module means a module that has a finite basis.
More concisely: If `M` is a finite module over a semiring `R`, and there exists a surjective linear map from `M` to an additive commutative monoid `N` making both `M` and `N` `R`-modules, then `N` is also a finite module.
|
Module.Finite.exists_fin
theorem Module.Finite.exists_fin :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Module.Finite R M], ∃ n s, Submodule.span R (Set.range s) = ⊤
The theorem `Module.Finite.exists_fin` states that for any semiring `R` and any additively commutative monoid `M` that is also a module over `R` and is finite, there exists an integer `n` and a function `s` such that the submodule spanned by the range of `s` is the entire module. In other words, it's possible to generate the whole module by taking linear combinations of a finite set of vectors, where these vectors are the images of the function `s`.
More concisely: For any finite, additively commutative `R`-module `M`, there exists an integer `n` and a function `s : Fin n → M` such that the span of `s` is equal to `M`.
|
Module.finite_def
theorem Module.finite_def :
∀ {R : Type u_6} {M : Type u_7} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Module.Finite R M ↔ ⊤.FG
The theorem `Module.finite_def` states that for any semiring `R` and any additive commutative monoid `M` that is also a module over `R`, the module `M` is finite if and only if the top submodule (which includes all elements of `M`) is finitely generated. Here, a module is finite if it's generated by a finite set, and a submodule is finitely generated if it's the span of a finite subset of `M`. In other words, `M` can be expressed as a linear combination of a finite set of elements.
More concisely: A module over a semiring is finite if and only if its top submodule is finitely generated.
|
Submodule.FG.sup
theorem Submodule.FG.sup :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{N₁ N₂ : Submodule R M}, N₁.FG → N₂.FG → (N₁ ⊔ N₂).FG
This theorem states that for any semiring `R` and any additive commutative monoid `M` that is also an `R`-module, given two submodules `N₁` and `N₂` of `M` that are finitely generated (i.e., each can be expressed as the span of a finite subset of `M`), their superset (denoted as `N₁ ⊔ N₂`) is also finitely generated. Essentially, this means that the union of two finitely generated submodules is itself finitely generated.
More concisely: The union of two finitely generated submodules of an `R`-module `M` over a semiring `R` is itself a finitely generated submodule.
|
Submodule.fg_def
theorem Submodule.fg_def :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
{N : Submodule R M}, N.FG ↔ ∃ S, S.Finite ∧ Submodule.span R S = N
The theorem `Submodule.fg_def` states that for any semiring `R`, any additive commutative monoid `M`, and any submodule `N` of `M` over `R`, `N` is finitely generated (i.e., it is the span of a finite subset of `M`) if and only if there exists a set `S` such that `S` is finite and the span of `S` is `N`. The span of a set is defined as the smallest submodule that contains that set. Therefore, a submodule is finitely generated if it can be expressed as the span of a finite set.
More concisely: A submodule of an additive commutative monoid over a semiring is finitely generated if and only if it is the span of a finite set.
|
Submodule.exists_fg_le_eq_rTensor_inclusion
theorem Submodule.exists_fg_le_eq_rTensor_inclusion :
∀ {R : Type u_4} {M : Type u_5} {N : Type u_6} [inst : CommRing R] [inst_1 : AddCommGroup M]
[inst_2 : AddCommGroup N] [inst_3 : Module R M] [inst_4 : Module R N] {I : Submodule R N}
(x : TensorProduct R (↥I) M),
∃ J, ∃ (_ : J.FG) (hle : J ≤ I), ∃ y, x = (LinearMap.rTensor M (Submodule.inclusion hle)) y
The theorem states that for every tensor product `x` of a submodule `I` and a module `M` over a commutative ring `R`, there exists a finitely generated submodule `J` of `I` such that `x` can be obtained as the image of some tensor product `y` of `J` and `M` under the tensor product of the inclusion map from `J` to `I` and the identity map on `M`. This means that `x`, although it is a tensor product over the entire submodule `I`, can be represented using a tensor product over a smaller, finitely generated submodule `J`.
More concisely: For every tensor product of a submodule of a commutative ring and a module, there exists a finitely generated submodule of the submodule such that the tensor product can be represented as the image of their tensor product under the inclusion map and the identity map.
|
Ideal.FG.map
theorem Ideal.FG.map :
∀ {R : Type u_3} {S : Type u_4} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R},
I.FG → ∀ (f : R →+* S), (Ideal.map f I).FG
This theorem states that the image of a finitely generated ideal under a ring homomorphism is also finitely generated. More specifically, if we have a semiring `R` and another semiring `S`, and if `I` is a finitely generated ideal in `R`, then for any ring homomorphism `f` from `R` to `S`, the ideal obtained by mapping `I` under `f` (denoted as `Ideal.map f I` in Lean) is also finitely generated. This theorem is the `Ideal` version of the corresponding theorem for submodules, `Submodule.FG.map`.
More concisely: The image of a finitely generated ideal under a ring homomorphism is a finitely generated ideal.
|
Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul
theorem Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul :
∀ {R : Type u_3} [inst : CommRing R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
(N : Submodule R M), N.FG → N ≤ I • N → ∃ r, r - 1 ∈ I ∧ ∀ n ∈ N, r • n = 0
**Nakayama's Lemma**. Given a commutative ring `R`, an additive commutative group `M` and a module `M` over `R`, along with an ideal `I` of `R` and a submodule `N` of `M` which is finitely generated (`N.FG`), if `N` is contained in or equal to the submodule generated by `I` and `N` (`I • N`), then there exists an element `r` such that `r - 1` is an element of `I` and for all elements `n` in `N`, the scalar multiplication of `r` and `n` equals 0. In mathematical terms, it means there exists `r` in `R` such that `r - 1` is in `I` and `r * n = 0` for all `n` in `N`.
More concisely: If `I` is an ideal of the commutative ring `R`, `N` is a finitely generated submodule of the module `M` over `R`, and `N` is contained in `I • N`, then there exists an element `r` in `R` such that `r - 1` is in `I` and `r * n = 0` for all `n` in `N`.
|
Module.Finite.out
theorem Module.Finite.out :
∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[self : Module.Finite R M], ⊤.FG
This theorem states that for any type `R` denoting a semiring and any type `M` representing a module over `R` (with `R` being a semiring, `M` being an additive commutative monoid, and the operation of `R` on `M` forming a module), if the module `M` is finite (denoted as `Module.Finite R M`), then the entire module (represented as `⊤`) is finitely generated (`⊤.FG`). This theorem does not provide a proof.
More concisely: If `R` is a semiring and `M` is a finite module over `R`, then `M` is finitely generated.
|
Submodule.FG.map
theorem Submodule.FG.map :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {P : Type u_3}
[inst_3 : AddCommMonoid P] [inst_4 : Module R P] (f : M →ₗ[R] P) {N : Submodule R M},
N.FG → (Submodule.map f N).FG
The theorem `Submodule.FG.map` states that for any semiring `R`, two additively commutative monoids `M` and `P` with module structures over `R`, a linear map `f` from `M` to `P`, and a finitely generated submodule `N` of `M`, the image of `N` under `f` (represented by `Submodule.map f N`) is also a finitely generated submodule of `P`. In other words, a finitely generated submodule remains finitely generated when mapped using a linear transformation.
More concisely: Given a semiring R, additively commutative monoids M and P with R-module structures, a linear map f from M to P, and a finitely generated submodule N of M, the image of N under f is also a finitely generated submodule of P.
|
Module.Finite.span_of_finite
theorem Module.Finite.span_of_finite :
∀ (R : Type u_1) {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {A : Set M},
A.Finite → Module.Finite R ↥(Submodule.span R A)
This theorem states that for any semiring `R` and any additive commutative monoid `M` that is also a module over `R`, if a set `A` of elements in `M` is finite, then the submodule of `M` generated by the set `A` (i.e., the smallest submodule of `M` that contains `A`, denoted by `Submodule.span R A`) is `R`-finite. The term "`R`-finite" refers to the property of being finite with respect to the semiring `R`. In other words, if we start with a finite set of elements in a module, the submodule spanned by that set is also finite in the context of the semiring that the module is based upon.
More concisely: For any semiring `R` and additive commutative `R`-module `M` with finite set `A` in `M`, the submodule generated by `A` (`Submodule.span R A`) is `R`-finite.
|
Submodule.fg_bot
theorem Submodule.fg_bot :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M], ⊥.FG := by
sorry
This theorem states that, for any semiring `R` and any additive commutative monoid `M` that is also a module over `R`, the bottom submodule (denoted by `⊥`) is finitely generated. In other words, there exists a finite subset of `M` such that the span of this subset equals the bottom submodule.
More concisely: Given a semiring `R` and an additive commutative `R`-module `M`, the bottom submodule `⊥` is finitely generated.
|
Submodule.fg_iff_compact
theorem Submodule.fg_iff_compact :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(s : Submodule R M), s.FG ↔ CompleteLattice.IsCompactElement s
The theorem states that for any ring `R`, an additive commutative monoid structure `M`, and a module structure of `M` over `R`, a submodule `s` of `M` is finitely generated if and only if it is a compact element in the lattice of submodules. Here, being a compact element means for all subsets of submodules with supremum (greatest element) greater than or equal to `s`, there exists a finite subset whose supremum is also greater than or equal to `s`.
More concisely: A submodule of an `R`-module `M` is finitely generated if and only if it is a compact element in the lattice of submodules.
|
Submodule.fg_ker_comp
theorem Submodule.fg_ker_comp :
∀ {R : Type u_4} {M : Type u_5} {N : Type u_6} {P : Type u_7} [inst : Ring R] [inst_1 : AddCommGroup M]
[inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : AddCommGroup P]
[inst_6 : Module R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P),
(LinearMap.ker f).FG → (LinearMap.ker g).FG → Function.Surjective ⇑f → (LinearMap.ker (g ∘ₗ f)).FG
The theorem states that given a ring `R` and three module types `M`, `N`, and `P` over `R`, alongside two linear maps `f : M →ₗ[R] N` and `g : N →ₗ[R] P`, if the kernel of `f` and the kernel of `g` are both finitely generated and `f` is a surjective function, then the kernel of the composite function `g ∘ₗ f` is also finitely generated. Here, a function `f` is surjective if for every element in the target set there exists at least one element in the domain set such that the function maps this element to the target element.
More concisely: If `R` is a ring, `M`, `N`, and `P` are `R`-module types, `f : M → N` and `g : N → P` are `R`-linear surjective maps with finitely generated kernels, then the kernel of their composite `g ∘ f : M → P` is also finitely generated.
|
Module.Finite.finite_basis
theorem Module.Finite.finite_basis :
∀ {R : Type u_6} {M : Type u_7} [inst : Ring R] [inst_1 : Nontrivial R] [inst_2 : AddCommGroup M]
[inst_3 : Module R M] {ι : Type u_8} [inst_4 : Module.Finite R M], Basis ι R M → Finite ι
This theorem states that if a free module over a ring is finite, then any basis of that module is also finite. In other words, given a ring 'R', a module 'M' over 'R', and an arbitrary basis of this module, if the module 'M' is finite, then this basis is also finite. The theorem holds for any nontrivial ring 'R' and additively commutative group 'M'.
More concisely: If 'M' is a finite free module over the nontrivial ring 'R', then its basis is also finite.
|
Submodule.fg_top
theorem Submodule.fg_top :
∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
(N : Submodule R M), ⊤.FG ↔ N.FG
This theorem states that for any semiring `R`, any additive commutative monoid `M`, and any `R`-module structure on `M`, if `N` is a submodule of `M`, then the top submodule `⊤` is finitely generated if and only if `N` is finitely generated. Here, a submodule is said to be finitely generated if it can be expressed as the span of a finite subset of `M`. The span of a set of vectors is the smallest submodule that contains the set.
More concisely: For any semiring `R`, additive commutative monoid `M` with an `R`-module structure, and submodule `N` of `M`, `⊤` is finitely generated if and only if `N` is.
|
Module.Finite.of_restrictScalars_finite
theorem Module.Finite.of_restrictScalars_finite :
∀ (R : Type u_6) (A : Type u_7) (M : Type u_8) [inst : CommSemiring R] [inst_1 : Semiring A]
[inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : Module A M] [inst_5 : Algebra R A]
[inst_6 : IsScalarTower R A M] [hM : Module.Finite R M], Module.Finite A M
This theorem states that for any types `R`, `A`, and `M` representing a commutative semiring, a semiring, and an add commutative monoid respectively, given that `M` is a module over both `R` and `A`, and `A` is an algebra over `R`, and there is an scalar tower of R, A and M, if `M` is a finitely generated module over `R`, then `M` is also a finitely generated module over `A`. Here, a finitely generated module over a ring is a module that has a finite set of generators.
More concisely: If `R` is a commutative semiring, `A` is a semiring and an algebra over `R`, `M` is an add commutative monoid and an `R`-module as well as an `A`-module with a scalar tower, and `M` is finitely generated as an `R`-module, then `M` is finitely generated as an `A`-module.
|
Submodule.FG.mul
theorem Submodule.FG.mul :
∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
{M N : Submodule R A}, M.FG → N.FG → (M * N).FG
The theorem `Submodule.FG.mul` states that for any commutative semiring `R`, semiring `A`, and an algebra structure on `A` over `R`, if we have two submodules `M` and `N` of `A` that are finitely generated (i.e., each can be expressed as the span of a finite subset of `A`), then the product of `M` and `N` is also a finitely generated submodule of `A`. Essentially, it says that the product of two finitely generated submodules remains finitely generated.
More concisely: If `R` is a commutative semiring, `A` is a semiring with an algebra structure over `R`, and `M` and `N` are finitely generated submodules of `A`, then their product `M ⊥ N` is also a finitely generated submodule of `A`.
|