Module.free_iff_set
theorem Module.free_iff_set :
∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
Module.Free R M ↔ ∃ S, Nonempty (Basis (↑S) R M)
This theorem states that for any type `R` which has a semiring structure, and any type `M` which has an additive commutative monoid structure and a module structure over `R`, the module `M` is free over `R` if and only if there exists a set `S` such that there is a nonempty basis for `M` over `R` indexed by the elements of `S`. In other words, a module `M` over a semiring `R` is free exactly when it has a basis indexed by a set.
More concisely: A module M over a semiring R is free if and only if there exists a basis for M over R indexed by a set.
|
Module.Free.of_basis
theorem Module.Free.of_basis :
∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type w},
Basis ι R M → Module.Free R M
This theorem states that given any semiring `R`, additively commutative monoid `M` and a module `M` over `R`, for any type `ι`, if there exists a basis of `M` indexed by `ι`, then `M` is a free module over `R`. In other words, a module over a semiring is free if and only if it has a basis.
More concisely: A module over a semiring is free if and only if it has a basis. (In other words, a module over a semiring is free if it has a linearly independent set spanning the entire module.)
|
Module.Free.of_equiv
theorem Module.Free.of_equiv :
∀ {R : Type u} {M : Type v} {N : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
[inst_3 : Module.Free R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N], (M ≃ₗ[R] N) → Module.Free R N
The theorem `Module.Free.of_equiv` states that for any semiring `R` and any two types `M` and `N` that have the structure of an `R`-module, if `M` is a free `R`-module and there is a linear equivalence (a bijective, linear map) between `M` and `N`, then `N` is also a free `R`-module. This means that the property of being a free module is preserved under linear equivalences.
More concisely: If `M` and `N` are `R`-modules with `M` free and there exists a linear equivalence between them, then `N` is also a free `R`-module.
|
Module.Free.of_equiv'
theorem Module.Free.of_equiv' :
∀ {R : Type u} {N : Type z} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N] {P : Type v}
[inst_3 : AddCommMonoid P] [inst_4 : Module R P], Module.Free R P → (P ≃ₗ[R] N) → Module.Free R N
This theorem, named `Module.Free.of_equiv'`, states that for any semiring `R`, and types `N` and `P` for which `N` and `P` are respectively an `R`-module and a `R`-module with `P` being free, if there is a linear equivalence between `P` and `N`, then `N` is also a free `R`-module. This is a variation of the `of_equiv` theorem where the freedom of the `R`-module `P` is explicitly given as a hypothesis rather than being implied by the context.
More concisely: For any semiring `R`, if `N` and `P` are `R`-modules with `P` being a free `R`-module and there is a linear equivalence between `N` and `P`, then `N` is also a free `R`-module.
|