TotalAdditive.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

abbrev OAI.DerivedBar.moduleForgetAdd line 9
def OAI.DerivedBar.totalAddDesc line 19
Source documentation
Additive maps out of a module totalization, using its preserved coproduct. This permits unit insertion, which need not be A-linear.
```
def totalAddDesc {n : ℕ} {Y : AddCommGrpCat.{u}}
    (f : ∀ i q (_ : i+q=n), (F).obj ((K.X i).X q) ⟶ Y) :
    (F).obj ((K.total c).X n) ⟶ Y :=
…
```
theorem OAI.DerivedBar.ι_totalAddDesc line 28
theorem OAI.DerivedBar.totalAdd_hom_ext line 35