IsProjective.iff_projective
theorem IsProjective.iff_projective :
∀ {R : Type u} [inst : Ring R] {P : Type (max u v)} [inst_1 : AddCommGroup P] [inst_2 : Module R P],
Module.Projective R P ↔ CategoryTheory.Projective (ModuleCat.of R P)
This theorem establishes the equivalence between the categorical definition of a projective object and the explicit module-theoretic definition of a projective module. Given a type `R` with ring structure, and a type `P` that is an `R`-module, it asserts that `P` is a projective `R`-module if and only if it is a projective object in the category of `R`-modules. This linkage underpins the alignment of abstract categorical algebra with concrete module theory.
More concisely: A module over a ring is projective if and only if it is a projective object in the category of modules over that ring.
|
ModuleCat.projective_of_free
theorem ModuleCat.projective_of_free :
∀ {R : Type u} [inst : Ring R] {M : ModuleCat R} {ι : Type u'}, Basis ι R ↑M → CategoryTheory.Projective M := by
sorry
This theorem states that for any ring `R` and any module `M` over `R`, if `M` has a basis indexed by some type `ι`, then `M` is a projective module in the category of `R`-modules. In the context of module theory, a projective module is a module that satisfies a certain property concerning its homomorphisms into other modules. This theorem therefore provides a necessary and sufficient condition under which a module is projective.
More concisely: A module over a ring with a basis indexed by some type is projective.
|