refactor(algebra/module/projective) make is_projective a class (#7830)

Make `is_projective` a class.

src/algebra/category/Module/projective.lean

@@ -23,23 +23,27 @@ 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,
+  module.projective R P ↔ projective (Module.of R P) :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { letI : module.projective R ↥(Module.of R P) := h,
+    exact ⟨λ E X f e epi, module.projective_lifting_property _ _
+      ((Module.epi_iff_surjective _).mp epi)⟩ },
+  { refine module.projective_of_lifting_property _,
+    introsI E X mE mX sE sX f g s,
     haveI : epi ↟f := (Module.epi_iff_surjective ↟f).mpr s,
-    exact ⟨projective.factor_thru ↟g ↟f, projective.factor_thru_comp ↟g ↟f⟩,
-  end)⟩
+    letI : projective (Module.of R P) := h,
+    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`.
+-- We transport the corresponding result from `module.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))
+  ((is_projective.iff_projective).mp (module.projective_of_free b))
 
 /-- The category of modules has enough projectives, since every module is a quotient of a free
     module. -/

src/algebra/module/projective.lean

@@ -68,19 +68,24 @@ universes u v
 /-- An R-module is projective if it is a direct summand of a free module, or equivalently
   if maps from the module lift along surjections. There are several other equivalent
   definitions. -/
-def is_projective
-  (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
+class module.projective (R : Type u) [semiring R] (P : Type (max u v)) [add_comm_monoid P]
+  [module R P] : Prop :=
+(out : ∃ s : P →ₗ[R] (P →₀ R), function.left_inverse (finsupp.total P P R id) s)
 
-namespace is_projective
+namespace module
+
+lemma projective_def {R : Type u} [semiring R] {P : Type (max u v)} [add_comm_monoid P]
+  [module R P] : projective R P ↔
+  (∃ s : P →ₗ[R] (P →₀ R), function.left_inverse (finsupp.total P P R id) s) :=
+⟨λ h, h.1, λ h, ⟨h⟩⟩
 
 section semiring
 
 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)
+theorem projective_lifting_property [h : projective R P] (f : M →ₗ[R] N) (g : P →ₗ[R] N)
   (hf : function.surjective f) : ∃ (h : P →ₗ[R] M), f.comp h = g :=
 begin
   /-
@@ -94,7 +99,7 @@ begin
   -/
   let φ : (P →₀ R) →ₗ[R] M := finsupp.total _ _ _ (λ p, function.surj_inv hf (g p)),
   -- By projectivity we have a map `P →ₗ (P →₀ R)`;
-  cases h with s hs,
+  cases h.out with s hs,
   -- Compose to get `P →ₗ M`. This works.
   use φ.comp s,
   ext p,
@@ -104,7 +109,7 @@ end
 
 /-- A module which satisfies the universal property is projective. Note that the universe variables
 in `huniv` are somewhat restricted. -/
-theorem of_lifting_property'
+theorem projective_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_monoid M] [add_comm_monoid N],
     by exactI
@@ -113,7 +118,7 @@ theorem of_lifting_property'
     ∀ (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 :=
+  projective R P :=
 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),
@@ -135,7 +140,7 @@ variables {R : Type u} [ring R] {P : Type (max u v)} [add_comm_group P] [module
 
 /-- 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
+theorem projective_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
@@ -144,7 +149,7 @@ theorem of_lifting_property
     ∀ (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 :=
+  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.
@@ -161,8 +166,9 @@ begin
     simp },
 end
 
+--TODO: use `module.free`
 /-- Free modules are projective. -/
-theorem of_free {ι : Type*} (b : basis ι R P) : is_projective R P :=
+theorem projective_of_free {ι : Type*} (b : basis ι R P) : projective R P :=
 begin
   -- need P →ₗ (P →₀ R) for definition of projective.
   -- get it from `ι → (P →₀ R)` coming from `b`.
@@ -175,4 +181,4 @@ end
 
 end ring
 
-end is_projective
+end module