opened
Bolt64
username_0
Added support for homological algebra (though only with abelian groups; general R-modules are not supported yet). Also have a few basic results, including the Four Lemma (the surjective version). If the injective version is added, the five lemma will be an easy consequence.
Added support for homological algebra in the HoTT library
issue
created
fpvandoorn
username_1
Thank you very much for your pull request. The four lemma is nice to have.
We indeed want to do homological algebra in the Lean-HoTT library, and we are also working on it, but in a different repository, namely this one:
https://github.com/cmu-phil/Spectral
In the `algebra` folder we are doing algebra with abelian groups, R-modules and graded R-modules. 

Some comments on your additions:
* You are doing a lot of things which are already in the library. For example `transport_equality_hom` is a special case of `ap` (open namespace `eq`), and many other lemmas in `algebraic_lemmas` and definitions in `chain_complex_abelian_group` are already in the library (see for example the file [`function`](https://github.com/leanprover/lean2/blob/master/hott/function.hlean) or [`init.equiv`](https://github.com/leanprover/lean2/blob/master/hott/init/equiv.hlean); we call injective/bijective maps `is_embedding`/`is_equiv`. Your definition of a surjective homomorphism is actually a split surjective homomorphism, and not generally a proposition.
* You can put arguments before the colon, then they are already introduced in the proof. For example:
```lean
lemma mul_commutative {G : AbGroup} (x y : G) : x*y = y*x :=
  mul.comm x y
```
* We use the design that computational lemmas about groups for `inf_group`, which are groups without the assumption that they are sets. See https://github.com/leanprover/lean2/blob/master/hott/algebra/inf_group.hlean#L157-L334 In this way, we don't need different lemmas for different rings, groups, semigroups, abelian groups, etc. We use type class inference to figure out that we can apply the lemma. This happened in my code above: `mul.comm` is defined for arbitrary `comm_inf_semigroup`, and type class inference shows that `G` is a commutative infinite semigroup.
* I think e.g. `cancelling` is missing from `inf_group`. It is more useful if you add it there (preferably under a name like `inv_mul_eq_one`). A nicer way to prove it is something like this:
```lean
lemma cancelling {G : Type} {x y : G} [inf_group G] (p : x = y) : y⁻¹*x = 1 :=
ap (λz, y⁻¹ * z) p ⬝ mul.left_inv y
```
Here is also a possible proof of your axiom: (note: `this` is the name `Lean` uses for a `have` if you don't give it a name)
```lean
lemma combine_terms {G₁ G₂ : AbGroup} (φ : G₁ →g G₂) {a c : G₁} {b : G₂} (p :  φ(a) = b⁻¹*φ(c)) : b = φ(a⁻¹*c) :=
have b*φ(a) = φ(c), from mul_eq_of_eq_inv_mul p,
have b = (φ(a))⁻¹ * φ(c), from eq_inv_mul_of_mul_eq (mul.comm (φ(a)) b ⬝ this),
this ⬝ ap (λz, z * φ(c)) (to_respect_inv φ a)⁻¹ ⬝ (to_respect_mul φ a⁻¹ c)⁻¹
```
comment
created
fpvandoorn
username_1
I'm closing this PR for now. Feel free to reopen if you make the aforementioned changes.
comment