Quotient.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Short exact quotient complexes and biproduct cokernels.

def OAI.Kaplansky.quotientShortComplex line 18
Source documentation
Componentwise cokernels, with the actual induced maps.
```
def quotientShortComplex : ShortComplex C where
…
```
def OAI.Kaplansky.quotientShortComplexProjection line 25
def OAI.Kaplansky.kernelShortComplex line 32
def OAI.Kaplansky.kernelShortComplexInclusion line 39
def OAI.Kaplansky.quotientSnakeInput line 46
theorem OAI.Kaplansky.quotientShortComplex_shortExact line 72
Source documentation
Quotienting two short exact rows by an injective map on their right terms gives a short exact row. This is the algebraic relative gluing step.
```
theorem quotientShortComplex_shortExact (hS : S.ShortExact) (hT : T.ShortExact)
    [Mono f.τ₃] : (quotientShortComplex f).ShortExact := by
…
```
Mentions: OAI.Kaplansky.quotientShortComplex
def OAI.Kaplansky.cokernelBiprodIso line 93
Source documentation
The quotient of a direct sum is the direct sum of the actual quotients.
```
def cokernelBiprodIso : cokernel (biprod.map f g) ≅ cokernel f ⊞ cokernel g where
…
```
theorem OAI.Kaplansky.cokernelBiprodIso_projection line 112