From a617d0a61d6517258d88045c087f2f8c680c753a Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Tue, 25 May 2021 15:58:57 +0000 Subject: [PATCH] feat(algebra/category/Module): R-mod has enough projectives (#7113) Another piece of @TwoFX's `projective` branch, lightly edited. Co-authored-by: Markus Himmel Co-authored-by: Scott Morrison --- src/algebra/category/Module/projective.lean | 55 +++++++++++++++++++++ src/algebra/module/projective.lean | 46 +++++++++++++---- 2 files changed, 92 insertions(+), 9 deletions(-) create mode 100644 src/algebra/category/Module/projective.lean diff --git a/src/algebra/category/Module/projective.lean b/src/algebra/category/Module/projective.lean new file mode 100644 index 0000000000000..439b0b2b98ee8 --- /dev/null +++ b/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 diff --git a/src/algebra/module/projective.lean b/src/algebra/module/projective.lean index ba5cb50609f09..07fc4e721977b 100644 --- a/src/algebra/module/projective.lean +++ b/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 :=