Module.Projective.of_lifting_property'
theorem Module.Projective.of_lifting_property' :
∀ {R : Type u} [inst : Semiring R] {P : Type (max u v)} [inst_1 : AddCommMonoid P] [inst_2 : Module R P],
(∀ {M : Type (max v u)} {N : Type (max u v)} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N]
[inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N),
Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g) →
Module.Projective R P
This theorem states that a module is projective if it satisfies the universal property. Specifically, for any semiring `R` and any module `P` over `R` with additive commutative monoid structure, if for any two modules `M` and `N` (also over `R` and with additive commutative monoid structure), given any linear map `f : M →ₗ[R] N` and any other linear map `g : P →ₗ[R] N`, if `f` is surjective, then there exists a linear map `h` such that the composition of `f` and `h` equals `g`, then we can conclude that the module `P` is projective over `R`.
More concisely: A module over a semiring is projective if and only if it satisfies the universal property of projective modules with respect to surjective linear maps.
|
Module.Projective.of_lifting_property''
theorem Module.Projective.of_lifting_property'' :
∀ {R : Type u} [inst : Semiring R] {P : Type v} [inst_1 : AddCommMonoid P] [inst_2 : Module R P],
(∀ (f : (P →₀ R) →ₗ[R] P), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = LinearMap.id) → Module.Projective R P
The theorem `Module.Projective.of_lifting_property''` states that a module `P` over a semiring `R` is projective if it satisfies the universal property. The universal property here is specifically defined as: for every surjective linear map `f` from the module of functions from `P` to `R` to `P`, there exists a linear map `h` which is a left inverse to `f`. In other words, applying `h` after `f` yields the identity map on the module `P`.
More concisely: A module over a semiring is projective if and only if it satisfies the universal property of having a left inverse for every surjective linear map from it to itself.
|
Module.projective_lifting_property
theorem Module.projective_lifting_property :
∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {M : Type u_3}
[inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
[h : Module.Projective R P] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
The theorem `Module.projective_lifting_property` states that for any semiring `R`, and any `R`-modules `P`, `M`, and `N`, if `P` is a projective `R`-module, then given any linear map `f` from `M` to `N` and any linear map `g` from `P` to `N`, if `f` is surjective, then there exists a linear map `h` such that the composition of `f` and `h` equals `g`. This property of lifting maps along surjections is characteristic of projective modules.
More concisely: Given any surjective linear map `f` from an `R`-module `M` to an `R`-module `N`, and any linear map `g` from a projective `R`-module `P` to `N`, there exists a linear map `h` from `P` to `M` such that `g = f ∘ h`.
|
Module.Projective.of_lifting_property
theorem Module.Projective.of_lifting_property :
∀ {R : Type u} [inst : Ring R] {P : Type (max u v)} [inst_1 : AddCommGroup P] [inst_2 : Module R P],
(∀ {M : Type (max v u)} {N : Type (max u v)} [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N]
[inst_5 : Module R M] [inst_6 : Module R N] (f : M →ₗ[R] N) (g : P →ₗ[R] N),
Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g) →
Module.Projective R P
This theorem, `Module.Projective.of_lifting_property`, states that for any type `R` with a `Ring` instance, and any type `P` with an `AddCommGroup` and `Module R P` instances, if for all types `M` and `N` with `AddCommGroup` and `Module R` instances and for all linear maps `f : M →ₗ[R] N` and `g : P →ₗ[R] N`, there is a function `h` such that `f` composed with `h` equals `g` whenever `f` is surjective, then `P` is a projective `R`-module. In other words, it's a characterization of projective modules in terms of a certain lifting property: if every surjective linear map can be lifted along an arbitrary linear map, then the module is projective.
More concisely: If for every surjective linear map from an additive group with an `R`-module structure to another additive group with an `R`-module structure, there exists a lifting function, then the first group is a projective `R`-module.
|
Module.Projective.of_basis
theorem Module.Projective.of_basis :
∀ {R : Type u_1} [inst : Ring R] {P : Type u_2} [inst_1 : AddCommGroup P] [inst_2 : Module R P] {ι : Type u_3},
Basis ι R P → Module.Projective R P
This theorem states that for any ring `R` and any module `P` over `R` with an associated `AddCommGroup` structure, if there exists a basis of `P` indexed by type `ι`, then `P` is a projective module over `R`. In other words, if a module has a basis, then it is projective.
More concisely: If a module `P` over a ring `R` with an associated `AddCommGroup` structure has a basis, then `P` is projective as an `R`-module.
|