Projective finite-dimensional modules

Over a division ring, every finite-dimensional module is free and hence projective. Consequently, every short exact sequence of finite-dimensional modules splits.

Main results

• FGModuleCat.projective: every finite-dimensional module over a division ring is projective.
• FGModuleCat.projective_of_moduleProjective: every finitely generated projective module is a projective object.
• FGModuleCat.projective_biprod: finite projective modules are closed under biproducts.
• FGModuleCat.projective_of_free: every finite free module is projective.
• FGModuleCat.enoughProjectives: every finitely generated module is a quotient of a finite free module.
• FGModuleCat.moduleProjective_of_projective: a projective object of FGModuleCat R is a projective R-module, provided R is small relative to the universe of the modules.
• FGModuleCat.nonempty_splitting_of_shortExact: every short exact sequence of finite-dimensional modules over a division ring splits.

theorem FGModuleCat.projective_biprod (R : Type u) [Ring R] (X Y : FGModuleCat R) [Module.Projective R ↑X] [Module.Projective R ↑Y] : Module.Projective R ↑(X ⊞ Y)

A biproduct of finitely generated projective modules is projective.

theorem FGModuleCat.projective_of_moduleProjective (R : Type u) [Ring R] (X : FGModuleCat R) [Module.Projective R ↑X] : CategoryTheory.Projective X

A finitely generated projective module is a projective object of FGModuleCat R.

theorem FGModuleCat.projective_of_free (R : Type u) [Ring R] (X : FGModuleCat R) [Module.Free R ↑X] : CategoryTheory.Projective X

Every finite free module is a projective object.

theorem FGModuleCat.moduleProjective_of_projective {R : Type u} [Ring R] [Small.{v, u} R] (X : FGModuleCat R) [CategoryTheory.Projective X] : Module.Projective R ↑X

A projective object among the finitely generated modules is projective as an R-module. The smallness hypothesis holds automatically when the modules live in a universe containing R.

instance FGModuleCat.enoughProjectives {R : Type u} [Ring R] [Small.{v, u} R] : CategoryTheory.EnoughProjectives (FGModuleCat R)

FGModuleCat R has enough projectives: every finitely generated module is a quotient of a finite free module. The smallness hypothesis holds automatically when the modules live in a universe containing R.

theorem FGModuleCat.projective (k : Type u) [DivisionRing k] (X : FGModuleCat k) : CategoryTheory.Projective X

Every finite-dimensional vector space over a division ring is a projective object.

theorem FGModuleCat.nonempty_splitting_of_shortExact (k : Type u) [DivisionRing k] {S : CategoryTheory.ShortComplex (FGModuleCat k)} (hS : S.ShortExact) : Nonempty S.Splitting

Every short exact sequence of finite-dimensional vector spaces over a division ring splits.