feat(algebra/category/Module): R-mod has enough projectives (#7113)

Another piece of @TwoFX's `projective` branch, lightly edited.

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/category/Module/projective.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2020 Markus Himmel. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Markus Himmel, Scott Morrison
+-/
+import category_theory.abelian.projective
+import algebra.category.Module.abelian
+import linear_algebra.finsupp_vector_space
+import algebra.module.projective
+
+/-!
+# The category of `R`-modules has enough projectives.
+-/
+
+universes v u
+
+open category_theory
+open category_theory.limits
+open linear_map
+
+open_locale Module
+
+/-- The categorical notion of projective object agrees with the explicit module-theoretic notion. -/
+theorem is_projective.iff_projective {R : Type u} [ring R]
+  {P : Type (max u v)} [add_comm_group P] [module R P] :
+  is_projective R P ↔ projective (Module.of R P) :=
+⟨λ h, { factors := λ E X f e epi, h.lifting_property _ _ ((Module.epi_iff_surjective _).mp epi), },
+  λ h, is_projective.of_lifting_property (λ E X mE mX sE sX f g s,
+  begin
+    resetI,
+    haveI : epi ↟f := (Module.epi_iff_surjective ↟f).mpr s,
+    exact ⟨projective.factor_thru ↟g ↟f, projective.factor_thru_comp ↟g ↟f⟩,
+  end)⟩
+
+namespace Module
+variables {R : Type u} [ring R] {M : Module.{(max u v)} R}
+
+/-- Modules that have a basis are projective. -/
+-- We transport the corresponding result from `is_projective`.
+lemma projective_of_free {ι : Type*} (b : basis ι R M) : projective M :=
+projective.of_iso (Module.of_self_iso _)
+  ((is_projective.iff_projective).mp (is_projective.of_free b))
+
+/-- The category of modules has enough projectives, since every module is a quotient of a free
+    module. -/
+instance Module_enough_projectives : enough_projectives (Module.{max u v} R) :=
+{ presentation :=
+  λ M,
+  ⟨{ P := Module.of R (M →₀ R),
+    projective := projective_of_free finsupp.basis_single_one,
+    f := finsupp.basis_single_one.constr ℕ id,
+    epi := (epi_iff_range_eq_top _).mpr
+      (range_eq_top.2 (λ m, ⟨finsupp.single m (1 : R), by simp [basis.constr]⟩)) }⟩, }
+
+end Module

src/algebra/module/projective.lean

@@ -39,8 +39,9 @@ from the free R-module on the type M down to M splits. This is more convenient
 than certain other definitions which involve quantifying over universes,
 and also universe-polymorphic (the ring and module can be in different universes).
 
-Everything works for semirings and modules except that apparently
-we don't have free modules over semirings, so here we stick to rings.
+We require that the module sits in at least as high a universe as the ring:
+without this, free modules don't even exist,
+and it's unclear if projective modules are even a useful notion.
 
 ## References
 
@@ -68,15 +69,15 @@ universes u v
   if maps from the module lift along surjections. There are several other equivalent
   definitions. -/
 def is_projective
-  (R : Type u) [semiring R] (P : Type v) [add_comm_monoid P] [module R P] : Prop :=
+  (R : Type u) [semiring R] (P : Type (max u v)) [add_comm_monoid P] [module R P] : Prop :=
 ∃ s : P →ₗ[R] (P →₀ R), function.left_inverse (finsupp.total P P R id) s
 
 namespace is_projective
 
 section semiring
 
-variables {R : Type u} [semiring R] {P : Type v} [add_comm_monoid P] [module R P]
-  {M : Type*} [add_comm_group M] [module R M] {N : Type*} [add_comm_group N] [module R N]
+variables {R : Type u} [semiring R] {P : Type (max u v)} [add_comm_monoid P] [module R P]
+  {M : Type (max u v)} [add_comm_group M] [module R M] {N : Type*} [add_comm_group N] [module R N]
 
 /-- A projective R-module has the property that maps from it lift along surjections. -/
 theorem lifting_property (h : is_projective R P) (f : M →ₗ[R] N) (g : P →ₗ[R] N)
@@ -103,10 +104,9 @@ end
 
 /-- A module which satisfies the universal property is projective. Note that the universe variables
 in `huniv` are somewhat restricted. -/
-theorem of_lifting_property {R : Type u} [semiring R]
-  {P : Type v} [add_comm_monoid P] [module R P]
+theorem of_lifting_property'
   -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
-  (huniv : ∀ {M : Type (max v u)} {N : Type v} [add_comm_monoid M] [add_comm_monoid N],
+  (huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [add_comm_monoid M] [add_comm_monoid N],
     by exactI
     ∀ [module R M] [module R N],
     by exactI
@@ -131,7 +131,35 @@ end semiring
 
 section ring
 
-variables {R : Type u} [ring R] {P : Type v} [add_comm_group P] [module R P]
+variables {R : Type u} [ring R] {P : Type (max u v)} [add_comm_group P] [module R P]
+
+/-- A variant of `of_lifting_property'` when we're working over a `[ring R]`,
+which only requires quantifying over modules with an `add_comm_group` instance. -/
+theorem of_lifting_property
+  -- If for all surjections of `R`-modules `M →ₗ N`, all maps `P →ₗ N` lift to `P →ₗ M`,
+  (huniv : ∀ {M : Type (max v u)} {N : Type (max u v)} [add_comm_group M] [add_comm_group N],
+    by exactI
+    ∀ [module R M] [module R N],
+    by exactI
+    ∀ (f : M →ₗ[R] N) (g : P →ₗ[R] N),
+  function.surjective f → ∃ (h : P →ₗ[R] M), f.comp h = g) :
+  -- then `P` is projective.
+  is_projective R P :=
+-- We could try and prove this *using* `of_lifting_property`,
+-- but this quickly leads to typeclass hell,
+-- so we just prove it over again.
+begin
+  -- let `s` be the universal map `(P →₀ R) →ₗ P` coming from the identity map `P →ₗ P`.
+  obtain ⟨s, hs⟩ : ∃ (s : P →ₗ[R] P →₀ R),
+    (finsupp.total P P R id).comp s = linear_map.id :=
+    huniv (finsupp.total P P R (id : P → P)) (linear_map.id : P →ₗ[R] P) _,
+  -- This `s` works.
+  { use s,
+    rwa linear_map.ext_iff at hs },
+  { intro p,
+    use finsupp.single p 1,
+    simp },
+end
 
 /-- Free modules are projective. -/
 theorem of_free {ι : Type*} (b : basis ι R P) : is_projective R P :=