AddCommGroup vs Z Modules

Stream: condensed mathematics

[Fabian Glöckle]

I have written down the two step projective resolution of modules over PIDs. Do you need the same for AddCommGroup, and if so, can it be transpored using docs#Module.forget₂_AddCommGroup_full or should I copy it over?

[Fabian Glöckle]

i.e. the things to transport would be

import linear_algebra.free_module.basic
import algebra.homology.homological_complex
import algebra.homology.single
import algebra.category.Module.basic
import algebra.category.Module.projective
import category_theory.abelian.basic
import for_mathlib.projectives
import algebra.category.Module.abelian


open Module category_theory category_theory.limits

universes u v
variables (R : Type u) [comm_ring R] (M : Type (max u v)) [add_comm_group M] [module R M]

include M
def two_step_resolution : chain_complex (Module.{max v u} R) ℕ := sorry
def two_step_resolution_hom : (two_step_resolution R M) ⟶ ((chain_complex.single₀ (Module.{max u v} R)).obj (of R M)) := sorry
lemma two_step_resolution_projective_pid [is_domain R] [is_principal_ideal_ring R] :
  (two_step_resolution R M).is_projective_resolution (of R M) (two_step_resolution_hom R M) := sorry

[Johan Commelin]

Yes, we'll need it for AddCommGroup.