SnakeLemma

📁 Source: Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean

Statistics

Metric	Count
Definitions `SnakeInput`, `comp`, `f₀`, `f₁`, `f₂`, `f₃`, `id`, `L₀`, `L₀'`, `L₀X₂ToP`, `L₁`, `L₁'`, `L₂`, `L₂'`, `L₂'OpIso`, `L₃`, `P`, `P'`, `P'IsoUnopOpP`, `PIsoUnopOpP'`, `composableArrows`, `composableArrowsFunctor`, `functorL₀`, `functorL₁`, `functorL₁'`, `functorL₂`, `functorL₂'`, `functorL₃`, `functorP`, `h₀`, `h₀τ₁`, `h₀τ₂`, `h₀τ₃`, `h₃`, `h₃τ₁`, `h₃τ₂`, `h₃τ₃`, `instCategory`, `op`, `v₀₁`, `v₁₂`, `v₂₃`, `δ`, `δIso`, `φ₁`, `φ₂`	46
Theorems `comm₀₁`, `comm₀₁_assoc`, `comm₁₂`, `comm₁₂_assoc`, `comm₂₃`, `comm₂₃_assoc`, `comp_f₀`, `comp_f₁`, `comp_f₂`, `comp_f₃`, `ext`, `ext_iff`, `id_f₀`, `id_f₁`, `id_f₂`, `id_f₃`, `L₀'_exact`, `L₀X₂ToP_comp_pullback_snd`, `L₀X₂ToP_comp_pullback_snd_assoc`, `L₀X₂ToP_comp_φ₁`, `L₀X₂ToP_comp_φ₁_assoc`, `L₀_exact`, `L₀_g_δ`, `L₁'_X₁`, `L₁'_X₂`, `L₁'_X₃`, `L₁'_exact`, `L₁'_f`, `L₁'_g`, `L₁_exact`, `L₁_f_φ₁`, `L₁_f_φ₁_assoc`, `L₂'_X₁`, `L₂'_X₂`, `L₂'_X₃`, `L₂'_exact`, `L₂'_f`, `L₂'_g`, `L₂_exact`, `L₃_exact`, `comp_f₀`, `comp_f₀_assoc`, `comp_f₁`, `comp_f₁_assoc`, `comp_f₂`, `comp_f₂_assoc`, `comp_f₃`, `comp_f₃_assoc`, `composableArrowsFunctor_map`, `composableArrowsFunctor_obj`, `epi_L₁_g`, `epi_L₃_g`, `epi_v₂₃_τ₁`, `epi_v₂₃_τ₂`, `epi_v₂₃_τ₃`, `epi_δ`, `exact_C₁_down`, `exact_C₁_up`, `exact_C₂_down`, `exact_C₂_up`, `exact_C₃_down`, `exact_C₃_up`, `functorL₀_map`, `functorL₀_obj`, `functorL₁'_map_τ₁`, `functorL₁'_map_τ₂`, `functorL₁'_map_τ₃`, `functorL₁'_obj`, `functorL₁_map`, `functorL₁_obj`, `functorL₂'_map_τ₁`, `functorL₂'_map_τ₂`, `functorL₂'_map_τ₃`, `functorL₂'_obj`, `functorL₂_map`, `functorL₂_obj`, `functorL₃_map`, `functorL₃_obj`, `functorP_map`, `functorP_obj`, `id_f₀`, `id_f₁`, `id_f₂`, `id_f₃`, `instEpiGL₀'`, `instMonoFL₀'OfL₁`, `isIso_δ`, `lift_φ₂`, `lift_φ₂_assoc`, `mono_L₀_f`, `mono_L₂_f`, `mono_v₀₁_τ₁`, `mono_v₀₁_τ₂`, `mono_v₀₁_τ₃`, `mono_δ`, `naturality_δ`, `naturality_δ_assoc`, `naturality_φ₁`, `naturality_φ₁_assoc`, `naturality_φ₂`, `naturality_φ₂_assoc`, `op_L₀`, `op_L₁`, `op_L₂`, `op_L₃`, `op_v₀₁`, `op_v₁₂`, `op_v₂₃`, `op_δ`, `snake_lemma`, `snd_δ`, `snd_δ_assoc`, `snd_δ_inr`, `w₀₂`, `w₀₂_assoc`, `w₀₂_τ₁`, `w₀₂_τ₁_assoc`, `w₀₂_τ₂`, `w₀₂_τ₂_assoc`, `w₀₂_τ₃`, `w₀₂_τ₃_assoc`, `w₁₃`, `w₁₃_assoc`, `w₁₃_τ₁`, `w₁₃_τ₁_assoc`, `w₁₃_τ₂`, `w₁₃_τ₂_assoc`, `w₁₃_τ₃`, `w₁₃_τ₃_assoc`, `δ_L₃_f`, `δ_eq`, `φ₁_L₂_f`, `φ₁_L₂_f_assoc`	133
Total	179

CategoryTheory.ShortComplex

Definitions

Name	Category	Theorems
`SnakeInput` 📖	CompData	36 math math: `SnakeInput.naturality_φ₁`, `SnakeInput.comp_f₃_assoc`, `SnakeInput.functorL₁_obj`, `SnakeInput.functorL₁'_map_τ₃`, `SnakeInput.functorL₁'_map_τ₁`, `SnakeInput.id_f₂`, `SnakeInput.comp_f₀`, `SnakeInput.functorP_obj`, `SnakeInput.naturality_φ₁_assoc`, `SnakeInput.functorL₀_map`, `SnakeInput.functorL₁'_obj`, `SnakeInput.functorL₁'_map_τ₂`, `SnakeInput.composableArrowsFunctor_map`, `SnakeInput.functorL₀_obj`, `SnakeInput.functorL₂_obj`, `SnakeInput.functorL₁_map`, `SnakeInput.comp_f₂`, `SnakeInput.functorP_map`, `SnakeInput.functorL₃_obj`, `SnakeInput.comp_f₀_assoc`, `SnakeInput.id_f₁`, `SnakeInput.functorL₃_map`, `SnakeInput.id_f₀`, `SnakeInput.comp_f₁_assoc`, `SnakeInput.comp_f₃`, `SnakeInput.id_f₃`, `SnakeInput.functorL₂'_obj`, `SnakeInput.composableArrowsFunctor_obj`, `SnakeInput.functorL₂'_map_τ₃`, `SnakeInput.comp_f₂_assoc`, `SnakeInput.naturality_φ₂`, `SnakeInput.functorL₂'_map_τ₂`, `SnakeInput.naturality_φ₂_assoc`, `SnakeInput.comp_f₁`, `SnakeInput.functorL₂'_map_τ₁`, `SnakeInput.functorL₂_map`

CategoryTheory.ShortComplex.SnakeInput

Definitions

Name	Category	Theorems
`L₀` 📖	CompOp	55 math math: `exact_C₃_up`, `w₀₂_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₁`, `op_δ`, `naturality_δ`, `mono_v₀₁_τ₂`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₂`, `exact_C₁_up`, `functorL₁'_map_τ₁`, `mono_v₀₁_τ₃`, `w₀₂_τ₁`, `w₀₂_τ₃_assoc`, `L₀X₂ToP_comp_pullback_snd`, `comp_f₀`, `δ_L₃_f`, `mono_L₀_f`, `L₁'_f`, `functorL₁'_map_τ₂`, `snd_δ`, `snd_δ_inr`, `composableArrowsFunctor_map`, `L₀X₂ToP_comp_φ₁`, `functorL₀_obj`, `L₀_exact`, `op_L₀`, `L₁'_X₂`, `L₂'_X₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_g`, `w₀₂_τ₂`, `functorP_map`, `exact_C₂_up`, `L₀_g_δ`, `snd_δ_assoc`, `w₀₂_τ₁_assoc`, `w₀₂`, `comp_f₀_assoc`, `naturality_δ_assoc`, `L₁'_X₁`, `op_L₃`, `L₀X₂ToP_comp_φ₁_assoc`, `id_f₀`, `HomologicalComplex.HomologySequence.snakeInput_L₀`, `op_v₂₃`, `Hom.id_f₀`, `w₀₂_τ₂_assoc`, `mono_v₀₁_τ₁`, `Hom.comm₀₁`, `epi_δ`, `L₀X₂ToP_comp_pullback_snd_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_f`, `Hom.comm₀₁_assoc`, `w₀₂_τ₃`, `functorL₂'_map_τ₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₀_X₃`, `Hom.comp_f₀`
`L₀'` 📖	CompOp	5 math math: `L₀'_exact`, `instEpiGL₀'`, `L₁_f_φ₁_assoc`, `L₁_f_φ₁`, `instMonoFL₀'OfL₁`
`L₀X₂ToP` 📖	CompOp	4 math math: `L₀X₂ToP_comp_pullback_snd`, `L₀X₂ToP_comp_φ₁`, `L₀X₂ToP_comp_φ₁_assoc`, `L₀X₂ToP_comp_pullback_snd_assoc`
`L₁` 📖	CompOp	55 math math: `exact_C₃_up`, `w₀₂_assoc`, `functorL₁_obj`, `mono_v₀₁_τ₂`, `exact_C₁_up`, `L₁_exact`, `mono_v₀₁_τ₃`, `Hom.comp_f₁`, `w₀₂_τ₁`, `w₀₂_τ₃_assoc`, `op_L₂`, `w₁₃_τ₃`, `L₀X₂ToP_comp_pullback_snd`, `op_v₁₂`, `w₁₃_τ₂`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_g`, `exact_C₂_down`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₃`, `w₁₃_τ₃_assoc`, `HomologicalComplex.HomologySequence.snakeInput_L₁`, `Hom.comm₁₂`, `w₁₃_τ₂_assoc`, `snd_δ`, `snd_δ_inr`, `L₁_f_φ₁_assoc`, `w₁₃_τ₁_assoc`, `Hom.comm₁₂_assoc`, `w₀₂_τ₂`, `w₁₃_assoc`, `functorP_map`, `exact_C₂_up`, `snd_δ_assoc`, `w₀₂_τ₁_assoc`, `w₀₂`, `L₁_f_φ₁`, `id_f₁`, `op_v₂₃`, `comp_f₁_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₂`, `w₀₂_τ₂_assoc`, `Hom.id_f₁`, `mono_v₀₁_τ₁`, `Hom.comm₀₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_f`, `op_L₁`, `L₀X₂ToP_comp_pullback_snd_assoc`, `exact_C₃_down`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₁_X₁`, `Hom.comm₀₁_assoc`, `w₀₂_τ₃`, `w₁₃_τ₁`, `exact_C₁_down`, `epi_L₁_g`, `comp_f₁`, `w₁₃`
`L₁'` 📖	CompOp	10 math math: `functorL₁'_map_τ₃`, `functorL₁'_map_τ₁`, `functorL₁'_obj`, `L₁'_f`, `functorL₁'_map_τ₂`, `L₁'_g`, `L₁'_X₂`, `L₁'_exact`, `L₁'_X₁`, `L₁'_X₃`
`L₂` 📖	CompOp	62 math math: `exact_C₃_up`, `w₀₂_assoc`, `naturality_φ₁`, `Hom.comm₂₃`, `exact_C₁_up`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₃`, `w₀₂_τ₁`, `w₀₂_τ₃_assoc`, `op_L₂`, `w₁₃_τ₃`, `op_v₁₂`, `id_f₂`, `w₁₃_τ₂`, `exact_C₂_down`, `w₁₃_τ₃_assoc`, `Hom.comm₁₂`, `naturality_φ₁_assoc`, `w₁₃_τ₂_assoc`, `Hom.comm₂₃_assoc`, `snd_δ`, `lift_φ₂`, `snd_δ_inr`, `L₁_f_φ₁_assoc`, `φ₁_L₂_f_assoc`, `L₀X₂ToP_comp_φ₁`, `w₁₃_τ₁_assoc`, `Hom.comm₁₂_assoc`, `epi_v₂₃_τ₂`, `functorL₂_obj`, `w₀₂_τ₂`, `comp_f₂`, `w₁₃_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₂`, `exact_C₂_up`, `snd_δ_assoc`, `w₀₂_τ₁_assoc`, `w₀₂`, `L₁_f_φ₁`, `lift_φ₂_assoc`, `φ₁_L₂_f`, `L₀X₂ToP_comp_φ₁_assoc`, `epi_v₂₃_τ₃`, `op_v₀₁`, `HomologicalComplex.HomologySequence.snakeInput_L₂`, `w₀₂_τ₂_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_g`, `mono_L₂_f`, `comp_f₂_assoc`, `naturality_φ₂`, `op_L₁`, `exact_C₃_down`, `w₀₂_τ₃`, `naturality_φ₂_assoc`, `L₂_exact`, `Hom.comp_f₂`, `w₁₃_τ₁`, `exact_C₁_down`, `Hom.id_f₂`, `w₁₃`, `epi_v₂₃_τ₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_X₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₂_f`
`L₂'` 📖	CompOp	10 math math: `L₂'_g`, `L₂'_X₃`, `L₂'_X₁`, `L₂'_exact`, `functorL₂'_obj`, `functorL₂'_map_τ₃`, `L₂'_X₂`, `L₂'_f`, `functorL₂'_map_τ₂`, `functorL₂'_map_τ₁`
`L₂'OpIso` 📖	CompOp	—
`L₃` 📖	CompOp	53 math math: `epi_L₃_g`, `op_δ`, `comp_f₃_assoc`, `naturality_δ`, `Hom.comm₂₃`, `L₃_exact`, `functorL₁'_map_τ₃`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_g`, `w₁₃_τ₃`, `w₁₃_τ₂`, `exact_C₂_down`, `w₁₃_τ₃_assoc`, `δ_L₃_f`, `L₂'_g`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_f`, `w₁₃_τ₂_assoc`, `Hom.comm₂₃_assoc`, `snd_δ`, `snd_δ_inr`, `composableArrowsFunctor_map`, `mono_δ`, `Hom.id_f₃`, `L₂'_X₃`, `w₁₃_τ₁_assoc`, `epi_v₂₃_τ₂`, `op_L₀`, `w₁₃_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₃`, `L₀_g_δ`, `snd_δ_assoc`, `functorL₃_obj`, `naturality_δ_assoc`, `op_L₃`, `L₁'_X₃`, `epi_v₂₃_τ₃`, `op_v₀₁`, `comp_f₃`, `δ_apply'`, `HomologicalComplex.HomologySequence.snakeInput_L₃`, `id_f₃`, `δ_apply`, `functorL₂'_map_τ₃`, `L₂'_X₂`, `exact_C₃_down`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₁`, `functorL₂'_map_τ₂`, `Hom.comp_f₃`, `w₁₃_τ₁`, `exact_C₁_down`, `δ_eq`, `w₁₃`, `epi_v₂₃_τ₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_L₃_X₂`
`P` 📖	CompOp	12 math math: `naturality_φ₁`, `L₀X₂ToP_comp_pullback_snd`, `functorP_obj`, `naturality_φ₁_assoc`, `snd_δ`, `φ₁_L₂_f_assoc`, `L₀X₂ToP_comp_φ₁`, `φ₁_L₂_f`, `L₀X₂ToP_comp_φ₁_assoc`, `naturality_φ₂`, `L₀X₂ToP_comp_pullback_snd_assoc`, `naturality_φ₂_assoc`
`P'` 📖	CompOp	—
`P'IsoUnopOpP` 📖	CompOp	—
`PIsoUnopOpP'` 📖	CompOp	—
`composableArrows` 📖	CompOp	3 math math: `composableArrowsFunctor_map`, `snake_lemma`, `composableArrowsFunctor_obj`
`composableArrowsFunctor` 📖	CompOp	2 math math: `composableArrowsFunctor_map`, `composableArrowsFunctor_obj`
`functorL₀` 📖	CompOp	2 math math: `functorL₀_map`, `functorL₀_obj`
`functorL₁` 📖	CompOp	2 math math: `functorL₁_obj`, `functorL₁_map`
`functorL₁'` 📖	CompOp	4 math math: `functorL₁'_map_τ₃`, `functorL₁'_map_τ₁`, `functorL₁'_obj`, `functorL₁'_map_τ₂`
`functorL₂` 📖	CompOp	2 math math: `functorL₂_obj`, `functorL₂_map`
`functorL₂'` 📖	CompOp	4 math math: `functorL₂'_obj`, `functorL₂'_map_τ₃`, `functorL₂'_map_τ₂`, `functorL₂'_map_τ₁`
`functorL₃` 📖	CompOp	2 math math: `functorL₃_obj`, `functorL₃_map`
`functorP` 📖	CompOp	6 math math: `naturality_φ₁`, `functorP_obj`, `naturality_φ₁_assoc`, `functorP_map`, `naturality_φ₂`, `naturality_φ₂_assoc`
`h₀` 📖	CompOp	—
`h₀τ₁` 📖	CompOp	—
`h₀τ₂` 📖	CompOp	—
`h₀τ₃` 📖	CompOp	—
`h₃` 📖	CompOp	—
`h₃τ₁` 📖	CompOp	—
`h₃τ₂` 📖	CompOp	—
`h₃τ₃` 📖	CompOp	—
`instCategory` 📖	CompOp	36 math math: `naturality_φ₁`, `comp_f₃_assoc`, `functorL₁_obj`, `functorL₁'_map_τ₃`, `functorL₁'_map_τ₁`, `id_f₂`, `comp_f₀`, `functorP_obj`, `naturality_φ₁_assoc`, `functorL₀_map`, `functorL₁'_obj`, `functorL₁'_map_τ₂`, `composableArrowsFunctor_map`, `functorL₀_obj`, `functorL₂_obj`, `functorL₁_map`, `comp_f₂`, `functorP_map`, `functorL₃_obj`, `comp_f₀_assoc`, `id_f₁`, `functorL₃_map`, `id_f₀`, `comp_f₁_assoc`, `comp_f₃`, `id_f₃`, `functorL₂'_obj`, `composableArrowsFunctor_obj`, `functorL₂'_map_τ₃`, `comp_f₂_assoc`, `naturality_φ₂`, `functorL₂'_map_τ₂`, `naturality_φ₂_assoc`, `comp_f₁`, `functorL₂'_map_τ₁`, `functorL₂_map`
`op` 📖	CompOp	8 math math: `op_δ`, `op_L₂`, `op_v₁₂`, `op_L₀`, `op_L₃`, `op_v₂₃`, `op_v₀₁`, `op_L₁`
`v₀₁` 📖	CompOp	28 math math: `exact_C₃_up`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₂`, `w₀₂_assoc`, `mono_v₀₁_τ₂`, `exact_C₁_up`, `mono_v₀₁_τ₃`, `w₀₂_τ₁`, `w₀₂_τ₃_assoc`, `L₀X₂ToP_comp_pullback_snd`, `snd_δ`, `snd_δ_inr`, `HomologicalComplex.HomologySequence.snakeInput_v₀₁`, `w₀₂_τ₂`, `functorP_map`, `exact_C₂_up`, `snd_δ_assoc`, `w₀₂_τ₁_assoc`, `w₀₂`, `op_v₂₃`, `op_v₀₁`, `w₀₂_τ₂_assoc`, `mono_v₀₁_τ₁`, `Hom.comm₀₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₀₁_τ₃`, `L₀X₂ToP_comp_pullback_snd_assoc`, `Hom.comm₀₁_assoc`, `w₀₂_τ₃`
`v₁₂` 📖	CompOp	34 math math: `exact_C₃_up`, `w₀₂_assoc`, `exact_C₁_up`, `w₀₂_τ₁`, `w₀₂_τ₃_assoc`, `w₁₃_τ₃`, `op_v₁₂`, `w₁₃_τ₂`, `exact_C₂_down`, `w₁₃_τ₃_assoc`, `Hom.comm₁₂`, `w₁₃_τ₂_assoc`, `lift_φ₂`, `snd_δ_inr`, `L₁_f_φ₁_assoc`, `w₁₃_τ₁_assoc`, `Hom.comm₁₂_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₂`, `w₀₂_τ₂`, `w₁₃_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₃`, `exact_C₂_up`, `w₀₂_τ₁_assoc`, `w₀₂`, `L₁_f_φ₁`, `lift_φ₂_assoc`, `w₀₂_τ₂_assoc`, `HomologicalComplex.HomologySequence.snakeInput_v₁₂`, `exact_C₃_down`, `w₀₂_τ₃`, `w₁₃_τ₁`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₁₂_τ₁`, `exact_C₁_down`, `w₁₃`
`v₂₃` 📖	CompOp	28 math math: `Hom.comm₂₃`, `w₁₃_τ₃`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₃`, `w₁₃_τ₂`, `exact_C₂_down`, `w₁₃_τ₃_assoc`, `HomologicalComplex.HomologySequence.snakeInput_v₂₃`, `w₁₃_τ₂_assoc`, `Hom.comm₂₃_assoc`, `snd_δ`, `snd_δ_inr`, `w₁₃_τ₁_assoc`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₂`, `epi_v₂₃_τ₂`, `w₁₃_assoc`, `snd_δ_assoc`, `epi_v₂₃_τ₃`, `op_v₂₃`, `op_v₀₁`, `δ_apply'`, `δ_apply`, `exact_C₃_down`, `CategoryTheory.kernelCokernelCompSequence.snakeInput_v₂₃_τ₁`, `w₁₃_τ₁`, `exact_C₁_down`, `δ_eq`, `w₁₃`, `epi_v₂₃_τ₁`
`δ` 📖	CompOp	16 math math: `op_δ`, `naturality_δ`, `δ_L₃_f`, `snd_δ`, `snd_δ_inr`, `mono_δ`, `L₁'_g`, `isIso_δ`, `L₀_g_δ`, `snd_δ_assoc`, `naturality_δ_assoc`, `δ_apply'`, `δ_apply`, `epi_δ`, `L₂'_f`, `δ_eq`
`δIso` 📖	CompOp	—
`φ₁` 📖	CompOp	10 math math: `naturality_φ₁`, `naturality_φ₁_assoc`, `snd_δ`, `L₁_f_φ₁_assoc`, `φ₁_L₂_f_assoc`, `L₀X₂ToP_comp_φ₁`, `snd_δ_assoc`, `L₁_f_φ₁`, `φ₁_L₂_f`, `L₀X₂ToP_comp_φ₁_assoc`
`φ₂` 📖	CompOp	6 math math: `lift_φ₂`, `φ₁_L₂_f_assoc`, `lift_φ₂_assoc`, `φ₁_L₂_f`, `naturality_φ₂`, `naturality_φ₂_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`L₀'_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀'`	—	`CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements` `CategoryTheory.ShortComplex.Exact.exact_up_to_refinements` `L₁_exact` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.condition` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Limits.zero_comp` `CategoryTheory.Limits.pullback.hom_ext` `CategoryTheory.Limits.limit.lift_π` `CategoryTheory.Limits.comp_zero`
`L₀X₂ToP_comp_pullback_snd` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `P` `CategoryTheory.ShortComplex.X₃` `L₀X₂ToP` `CategoryTheory.Limits.pullback.snd` `L₁` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁`	—	`CategoryTheory.Limits.limit.lift_π`
`L₀X₂ToP_comp_pullback_snd_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `P` `L₀X₂ToP` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Limits.pullback.snd` `L₁` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `L₀X₂ToP_comp_pullback_snd`
`L₀X₂ToP_comp_φ₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `P` `CategoryTheory.ShortComplex.X₁` `L₂` `L₀X₂ToP` `φ₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.cancel_mono` `mono_L₂_f` `CategoryTheory.Category.assoc` `φ₁_L₂_f` `CategoryTheory.Limits.pullback.lift_fst_assoc` `w₀₂_τ₂` `CategoryTheory.Limits.zero_comp`
`L₀X₂ToP_comp_φ₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `P` `L₀X₂ToP` `CategoryTheory.ShortComplex.X₁` `L₂` `φ₁` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `L₀X₂ToP_comp_φ₁`
`L₀_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀`	—	`CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements` `CategoryTheory.ShortComplex.Exact.exact_up_to_refinements` `L₁_exact` `CategoryTheory.Category.assoc` `CategoryTheory.ShortComplex.Hom.comm₂₃` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Limits.zero_comp` `CategoryTheory.cancel_mono` `mono_L₂_f` `CategoryTheory.ShortComplex.Hom.comm₁₂` `w₀₂_τ₂` `CategoryTheory.Limits.comp_zero` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `exact_C₁_up` `mono_v₀₁_τ₁` `CategoryTheory.ShortComplex.Exact.lift_f` `mono_v₀₁_τ₂`
`L₀_g_δ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `L₃` `CategoryTheory.ShortComplex.g` `δ` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`L₀X₂ToP_comp_pullback_snd` `CategoryTheory.Category.assoc` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `L₀'_exact` `instEpiGL₀'` `CategoryTheory.ShortComplex.Exact.g_desc` `L₀X₂ToP_comp_φ₁_assoc` `CategoryTheory.Limits.zero_comp`
`L₁'_X₁` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `CategoryTheory.ShortComplex.X₂` `L₀`	—	—
`L₁'_X₂` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `CategoryTheory.ShortComplex.X₃` `L₀`	—	—
`L₁'_X₃` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `CategoryTheory.ShortComplex.X₁` `L₃`	—	—
`L₁'_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'`	—	`CategoryTheory.ShortComplex.exact_iff_exact_up_to_refinements` `CategoryTheory.surjective_up_to_refinements_of_epi` `instEpiGL₀'` `CategoryTheory.Category.assoc` `snd_δ` `Mathlib.Tactic.Reassoc.eq_whisker'` `CategoryTheory.Limits.comp_zero` `CategoryTheory.ShortComplex.Exact.exact_up_to_refinements` `exact_C₁_down` `CategoryTheory.Preadditive.sub_comp` `CategoryTheory.ShortComplex.Hom.comm₁₂` `φ₁_L₂_f` `sub_self` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `exact_C₂_up` `mono_v₀₁_τ₂` `CategoryTheory.ShortComplex.Exact.lift_f` `CategoryTheory.cancel_mono` `mono_v₀₁_τ₃` `CategoryTheory.ShortComplex.Hom.comm₂₃` `CategoryTheory.Limits.pullback.condition` `CategoryTheory.ShortComplex.zero` `sub_zero` `CategoryTheory.epi_comp`
`L₁'_f` 📖	mathematical	—	`CategoryTheory.ShortComplex.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `CategoryTheory.ShortComplex.g` `L₀`	—	—
`L₁'_g` 📖	mathematical	—	`CategoryTheory.ShortComplex.g` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `δ`	—	—
`L₁_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁`	—	—
`L₁_f_φ₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀'` `CategoryTheory.ShortComplex.X₂` `L₂` `CategoryTheory.ShortComplex.f` `φ₁` `CategoryTheory.ShortComplex.Hom.τ₁` `L₁` `v₁₂`	—	`CategoryTheory.cancel_mono` `mono_L₂_f` `CategoryTheory.Category.assoc` `φ₁_L₂_f` `CategoryTheory.Limits.pullback.lift_fst_assoc` `CategoryTheory.ShortComplex.Hom.comm₁₂`
`L₁_f_φ₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀'` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f` `L₂` `φ₁` `CategoryTheory.ShortComplex.Hom.τ₁` `L₁` `v₁₂`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `L₁_f_φ₁`
`L₂'_X₁` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `CategoryTheory.ShortComplex.X₃` `L₀`	—	—
`L₂'_X₂` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `CategoryTheory.ShortComplex.X₁` `L₃`	—	—
`L₂'_X₃` 📖	mathematical	—	`CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `CategoryTheory.ShortComplex.X₂` `L₃`	—	—
`L₂'_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'`	—	`CategoryTheory.ShortComplex.exact_op_iff` `CategoryTheory.ShortComplex.exact_iff_of_iso` `L₁'_exact`
`L₂'_f` 📖	mathematical	—	`CategoryTheory.ShortComplex.f` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `δ`	—	—
`L₂'_g` 📖	mathematical	—	`CategoryTheory.ShortComplex.g` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `CategoryTheory.ShortComplex.f` `L₃`	—	—
`L₂_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂`	—	—
`L₃_exact` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₃`	—	`CategoryTheory.ShortComplex.Exact.unop` `L₀_exact`
`comp_f₀` 📖	mathematical	—	`Hom.f₀` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₀`	—	—
`comp_f₀_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₀` `Hom.f₀` `CategoryTheory.ShortComplex.SnakeInput` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_f₀`
`comp_f₁` 📖	mathematical	—	`Hom.f₁` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₁`	—	—
`comp_f₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₁` `Hom.f₁` `CategoryTheory.ShortComplex.SnakeInput` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_f₁`
`comp_f₂` 📖	mathematical	—	`Hom.f₂` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₂`	—	—
`comp_f₂_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₂` `Hom.f₂` `CategoryTheory.ShortComplex.SnakeInput` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_f₂`
`comp_f₃` 📖	mathematical	—	`Hom.f₃` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₃`	—	—
`comp_f₃_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₃` `Hom.f₃` `CategoryTheory.ShortComplex.SnakeInput` `instCategory`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comp_f₃`
`composableArrowsFunctor_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `composableArrowsFunctor` `CategoryTheory.ComposableArrows.homMk₅` `composableArrows` `CategoryTheory.ShortComplex.Hom.τ₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `Hom.f₀` `CategoryTheory.ShortComplex.Hom.τ₂` `CategoryTheory.ShortComplex.Hom.τ₃` `L₃` `Hom.f₃` `naturality_δ`	—	—
`composableArrowsFunctor_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ComposableArrows` `CategoryTheory.Functor.category` `Preorder.smallCategory` `PartialOrder.toPreorder` `Fin.instPartialOrder` `composableArrowsFunctor` `composableArrows`	—	—
`epi_L₁_g` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	—
`epi_L₃_g` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₃` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	`CategoryTheory.ShortComplex.Hom.comm₂₃` `CategoryTheory.epi_comp` `epi_v₂₃_τ₃` `CategoryTheory.epi_of_epi`
`epi_v₂₃_τ₁` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₁` `v₂₃`	—	`CategoryTheory.Limits.epi_of_isColimit_cofork` `w₁₃_τ₁`
`epi_v₂₃_τ₂` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₂` `v₂₃`	—	`CategoryTheory.Limits.epi_of_isColimit_cofork` `w₁₃_τ₂`
`epi_v₂₃_τ₃` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₃` `v₂₃`	—	`CategoryTheory.Limits.epi_of_isColimit_cofork` `w₁₃_τ₃`
`epi_δ` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₃`	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₃` `L₀` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.ShortComplex.exact_iff_epi` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Limits.IsZero.eq_zero_of_tgt` `L₂'_exact`
`exact_C₁_down` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₁` `L₁` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₁` `v₁₂` `v₂₃`	—	`CategoryTheory.ShortComplex.exact_of_g_is_cokernel` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`exact_C₁_up` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₁` `L₀` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₁` `v₀₁` `v₁₂`	—	`CategoryTheory.ShortComplex.exact_of_f_is_kernel` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`exact_C₂_down` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₂` `L₁` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂` `v₂₃`	—	`CategoryTheory.ShortComplex.exact_of_g_is_cokernel` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`exact_C₂_up` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₂` `L₀` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₂` `v₀₁` `v₁₂`	—	`CategoryTheory.ShortComplex.exact_of_f_is_kernel` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`exact_C₃_down` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₃` `L₁` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₃` `v₁₂` `v₂₃`	—	`CategoryTheory.ShortComplex.exact_of_g_is_cokernel` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`exact_C₃_up` 📖	mathematical	—	`CategoryTheory.ShortComplex.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.X₃` `L₀` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `v₁₂`	—	`CategoryTheory.ShortComplex.exact_of_f_is_kernel` `CategoryTheory.CategoryWithHomology.hasHomology` `CategoryTheory.categoryWithHomology_of_abelian`
`functorL₀_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₀` `Hom.f₀`	—	—
`functorL₀_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₀` `L₀`	—	—
`functorL₁'_map_τ₁` 📖	mathematical	—	`CategoryTheory.ShortComplex.Hom.τ₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `functorL₁'` `CategoryTheory.ShortComplex.Hom.τ₂` `L₀` `Hom.f₀`	—	—
`functorL₁'_map_τ₂` 📖	mathematical	—	`CategoryTheory.ShortComplex.Hom.τ₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `functorL₁'` `CategoryTheory.ShortComplex.Hom.τ₃` `L₀` `Hom.f₀`	—	—
`functorL₁'_map_τ₃` 📖	mathematical	—	`CategoryTheory.ShortComplex.Hom.τ₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁'` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `functorL₁'` `CategoryTheory.ShortComplex.Hom.τ₁` `L₃` `Hom.f₃`	—	—
`functorL₁'_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₁'` `L₁'`	—	—
`functorL₁_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₁` `Hom.f₁`	—	—
`functorL₁_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₁` `L₁`	—	—
`functorL₂'_map_τ₁` 📖	mathematical	—	`CategoryTheory.ShortComplex.Hom.τ₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `functorL₂'` `CategoryTheory.ShortComplex.Hom.τ₃` `L₀` `Hom.f₀`	—	—
`functorL₂'_map_τ₂` 📖	mathematical	—	`CategoryTheory.ShortComplex.Hom.τ₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `functorL₂'` `CategoryTheory.ShortComplex.Hom.τ₁` `L₃` `Hom.f₃`	—	—
`functorL₂'_map_τ₃` 📖	mathematical	—	`CategoryTheory.ShortComplex.Hom.τ₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂'` `CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.ShortComplex.instCategory` `functorL₂'` `CategoryTheory.ShortComplex.Hom.τ₂` `L₃` `Hom.f₃`	—	—
`functorL₂'_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₂'` `L₂'`	—	—
`functorL₂_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₂` `Hom.f₂`	—	—
`functorL₂_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₂` `L₂`	—	—
`functorL₃_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₃` `Hom.f₃`	—	—
`functorL₃_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `functorL₃` `L₃`	—	—
`functorP_map` 📖	mathematical	—	`CategoryTheory.Functor.map` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `functorP` `CategoryTheory.Limits.pullback.map` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `L₀` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `CategoryTheory.ShortComplex.Hom.τ₂` `Hom.f₁` `Hom.f₀`	—	—
`functorP_obj` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `functorP` `P`	—	—
`id_f₀` 📖	mathematical	—	`Hom.f₀` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₀`	—	—
`id_f₁` 📖	mathematical	—	`Hom.f₁` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₁`	—	—
`id_f₂` 📖	mathematical	—	`Hom.f₂` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₂`	—	—
`id_f₃` 📖	mathematical	—	`Hom.f₃` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex.SnakeInput` `CategoryTheory.Category.toCategoryStruct` `instCategory` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.ShortComplex.instCategory` `L₃`	—	—
`instEpiGL₀'` 📖	mathematical	—	`CategoryTheory.Epi` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀'` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g`	—	`CategoryTheory.Abelian.epi_pullback_of_epi_f` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `epi_L₁_g`
`instMonoFL₀'OfL₁` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀'` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	`CategoryTheory.mono_of_mono_fac` `CategoryTheory.Limits.limit.lift_π`
`isIso_δ` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₃`	`CategoryTheory.IsIso` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `δ`	—	`CategoryTheory.Balanced.isIso_of_mono_of_epi` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `mono_δ` `epi_δ`
`lift_φ₂` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g` `L₀` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁`	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.cospan` `L₂` `CategoryTheory.Limits.pullback.lift` `φ₂` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.limit.lift_π_assoc`
`lift_φ₂_assoc` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g` `L₀` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁`	`CategoryTheory.Limits.pullback` `CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.WalkingCospan` `CategoryTheory.Limits.WidePullbackShape.category` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.fintypeWalkingPair` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Limits.cospan` `CategoryTheory.Limits.pullback.lift` `L₂` `φ₂` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `lift_φ₂`
`mono_L₀_f` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	`CategoryTheory.ShortComplex.Hom.comm₁₂` `CategoryTheory.mono_comp` `mono_v₀₁_τ₁` `CategoryTheory.mono_of_mono`
`mono_L₂_f` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f`	—	—
`mono_v₀₁_τ₁` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `CategoryTheory.ShortComplex.Hom.τ₁` `v₀₁`	—	`CategoryTheory.Limits.mono_of_isLimit_fork` `w₀₂_τ₁`
`mono_v₀₁_τ₂` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `CategoryTheory.ShortComplex.Hom.τ₂` `v₀₁`	—	`CategoryTheory.Limits.mono_of_isLimit_fork` `w₀₂_τ₂`
`mono_v₀₁_τ₃` 📖	mathematical	—	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁`	—	`CategoryTheory.Limits.mono_of_isLimit_fork` `w₀₂_τ₃`
`mono_δ` 📖	mathematical	`CategoryTheory.Limits.IsZero` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀`	`CategoryTheory.Mono` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.X₁` `L₃` `δ`	—	`CategoryTheory.ShortComplex.exact_iff_mono` `CategoryTheory.Abelian.hasZeroObject` `CategoryTheory.Limits.IsZero.eq_zero_of_src` `L₁'_exact`
`naturality_δ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `CategoryTheory.ShortComplex.X₁` `L₃` `δ` `CategoryTheory.ShortComplex.Hom.τ₁` `Hom.f₃` `CategoryTheory.ShortComplex.Hom.τ₃` `Hom.f₀`	—	`CategoryTheory.cancel_epi` `CategoryTheory.Abelian.epi_pullback_of_epi_f` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `epi_L₁_g` `snd_δ_assoc` `CategoryTheory.ShortComplex.comp_τ₁` `Hom.comm₂₃` `naturality_φ₁_assoc` `snd_δ` `functorP_map` `CategoryTheory.Limits.pullback.lift_snd_assoc` `CategoryTheory.Category.assoc`
`naturality_δ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `CategoryTheory.ShortComplex.X₁` `L₃` `δ` `CategoryTheory.ShortComplex.Hom.τ₁` `Hom.f₃` `CategoryTheory.ShortComplex.Hom.τ₃` `Hom.f₀`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality_δ`
`naturality_φ₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `P` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `φ₁` `CategoryTheory.ShortComplex.Hom.τ₁` `Hom.f₂` `CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `functorP` `CategoryTheory.Functor.map`	—	`CategoryTheory.cancel_mono` `mono_L₂_f` `CategoryTheory.Category.assoc` `CategoryTheory.ShortComplex.Hom.comm₁₂` `φ₁_L₂_f_assoc` `φ₁_L₂_f`
`naturality_φ₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `P` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `φ₁` `CategoryTheory.ShortComplex.Hom.τ₁` `Hom.f₂` `CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `functorP` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality_φ₁`
`naturality_φ₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `P` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `φ₂` `CategoryTheory.ShortComplex.Hom.τ₂` `Hom.f₂` `CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `functorP` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Limits.pullback.lift_fst_assoc` `Hom.comm₁₂`
`naturality_φ₂_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `P` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `φ₂` `CategoryTheory.ShortComplex.Hom.τ₂` `Hom.f₂` `CategoryTheory.Functor.obj` `CategoryTheory.ShortComplex.SnakeInput` `instCategory` `functorP` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `naturality_φ₂`
`op_L₀` 📖	mathematical	—	`L₀` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `CategoryTheory.ShortComplex.op` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₃`	—	—
`op_L₁` 📖	mathematical	—	`L₁` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `CategoryTheory.ShortComplex.op` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂`	—	—
`op_L₂` 📖	mathematical	—	`L₂` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `CategoryTheory.ShortComplex.op` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁`	—	—
`op_L₃` 📖	mathematical	—	`L₃` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `CategoryTheory.ShortComplex.op` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀`	—	—
`op_v₀₁` 📖	mathematical	—	`v₀₁` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `CategoryTheory.ShortComplex.opMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `L₃` `v₂₃`	—	—
`op_v₁₂` 📖	mathematical	—	`v₁₂` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `CategoryTheory.ShortComplex.opMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `L₂`	—	—
`op_v₂₃` 📖	mathematical	—	`v₂₃` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `CategoryTheory.ShortComplex.opMap` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `v₀₁`	—	—
`op_δ` 📖	mathematical	—	`δ` `Opposite` `CategoryTheory.Category.opposite` `CategoryTheory.instAbelianOpposite` `op` `Quiver.Hom.op` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `CategoryTheory.ShortComplex.X₁` `L₃`	—	`Quiver.Hom.unop_op` `CategoryTheory.cancel_mono` `CategoryTheory.Abelian.mono_pushout_of_mono_f` `CategoryTheory.Limits.hasColimitsOfShape_widePushoutShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePushouts_of_has_finite_limits` `CategoryTheory.Abelian.hasFiniteColimits` `mono_L₂_f` `CategoryTheory.cancel_epi` `CategoryTheory.Abelian.epi_pullback_of_epi_f` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `epi_L₁_g` `snd_δ_inr` `CategoryTheory.mono_of_strongMono` `CategoryTheory.instStrongMonoOfIsRegularMono` `CategoryTheory.instIsRegularMonoOfIsSplitMono` `CategoryTheory.IsSplitMono.of_iso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.epi_of_effectiveEpi` `CategoryTheory.instEffectiveEpiOfIsIso` `CategoryTheory.Iso.isIso_inv` `P'IsoUnopOpP.eq_1` `PIsoUnopOpP'.eq_1` `CategoryTheory.Category.assoc` `CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom` `CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd_assoc` `CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom` `CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst_assoc`
`snake_lemma` 📖	mathematical	—	`CategoryTheory.ComposableArrows.Exact` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `composableArrows`	—	`CategoryTheory.ComposableArrows.exact_of_δ₀` `CategoryTheory.ShortComplex.Exact.exact_toComposableArrows` `L₀_exact` `L₁'_exact` `L₂'_exact` `L₃_exact`
`snd_δ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `L₀` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `CategoryTheory.ShortComplex.X₁` `L₃` `CategoryTheory.Limits.pullback.snd` `δ` `P` `L₂` `φ₁` `CategoryTheory.ShortComplex.Hom.τ₁` `v₂₃`	—	`CategoryTheory.ShortComplex.Exact.g_desc` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `L₀'_exact` `instEpiGL₀'`
`snd_δ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `L₀` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `CategoryTheory.Limits.pullback.snd` `CategoryTheory.ShortComplex.X₁` `L₃` `δ` `L₂` `φ₁` `CategoryTheory.ShortComplex.Hom.τ₁` `v₂₃`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `snd_δ`
`snd_δ_inr` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Limits.pullback` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `L₀` `CategoryTheory.ShortComplex.g` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `CategoryTheory.Limits.pushout` `CategoryTheory.ShortComplex.X₁` `L₂` `L₃` `CategoryTheory.ShortComplex.f` `CategoryTheory.ShortComplex.Hom.τ₁` `v₂₃` `CategoryTheory.Limits.pullback.snd` `δ` `CategoryTheory.Limits.pushout.inr` `CategoryTheory.Limits.pullback.fst` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂` `CategoryTheory.Limits.pushout.inl`	—	`snd_δ_assoc` `φ₁_L₂_f_assoc` `CategoryTheory.Category.assoc`
`w₀₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₀` `L₁` `L₂` `v₀₁` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.ShortComplex.instZeroHom`	—	—
`w₀₂_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₀` `L₁` `v₀₁` `L₂` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.ShortComplex.instZeroHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₀₂`
`w₀₂_τ₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₁` `v₀₁` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.ShortComplex.comp_τ₁` `w₀₂` `CategoryTheory.ShortComplex.zero_τ₁`
`w₀₂_τ₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `CategoryTheory.ShortComplex.Hom.τ₁` `v₀₁` `L₂` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₀₂_τ₁`
`w₀₂_τ₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₂` `v₀₁` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.ShortComplex.comp_τ₂` `w₀₂` `CategoryTheory.ShortComplex.zero_τ₂`
`w₀₂_τ₂_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `CategoryTheory.ShortComplex.Hom.τ₂` `v₀₁` `L₂` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₀₂_τ₂`
`w₀₂_τ₃` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.ShortComplex.comp_τ₃` `w₀₂` `CategoryTheory.ShortComplex.zero_τ₃`
`w₀₂_τ₃_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `L₁` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `L₂` `v₁₂` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₀₂_τ₃`
`w₁₃` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₁` `L₂` `L₃` `v₁₂` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.ShortComplex.instZeroHom`	—	—
`w₁₃_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `L₁` `L₂` `v₁₂` `L₃` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.ShortComplex.instZeroHom`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₁₃`
`w₁₃_τ₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₁` `v₁₂` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.ShortComplex.comp_τ₁` `w₁₃` `CategoryTheory.ShortComplex.zero_τ₁`
`w₁₃_τ₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₁` `v₁₂` `L₃` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₁₃_τ₁`
`w₁₃_τ₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.ShortComplex.comp_τ₂` `w₁₃` `CategoryTheory.ShortComplex.zero_τ₂`
`w₁₃_τ₂_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂` `L₃` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₁₃_τ₂`
`w₁₃_τ₃` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `L₂` `L₃` `CategoryTheory.ShortComplex.Hom.τ₃` `v₁₂` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.ShortComplex.comp_τ₃` `w₁₃` `CategoryTheory.ShortComplex.zero_τ₃`
`w₁₃_τ₃_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `L₂` `CategoryTheory.ShortComplex.Hom.τ₃` `v₁₂` `L₃` `v₂₃` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `w₁₃_τ₃`
`δ_L₃_f` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₀` `CategoryTheory.ShortComplex.X₁` `L₃` `CategoryTheory.ShortComplex.X₂` `δ` `CategoryTheory.ShortComplex.f` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.cancel_epi` `instEpiGL₀'` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `L₀'_exact` `CategoryTheory.ShortComplex.Exact.g_desc_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.ShortComplex.Hom.comm₁₂` `φ₁_L₂_f_assoc` `w₁₃_τ₂` `CategoryTheory.Limits.comp_zero`
`δ_eq` 📖	mathematical	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₁` `CategoryTheory.ShortComplex.X₃` `CategoryTheory.ShortComplex.g` `L₀` `CategoryTheory.ShortComplex.Hom.τ₃` `v₀₁` `CategoryTheory.ShortComplex.X₁` `L₂` `CategoryTheory.ShortComplex.f` `CategoryTheory.ShortComplex.Hom.τ₂` `v₁₂`	`L₃` `δ` `CategoryTheory.ShortComplex.Hom.τ₁` `v₂₃`	—	`CategoryTheory.Limits.hasLimitOfHasLimitsOfShape` `CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape` `Finite.of_fintype` `CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits` `CategoryTheory.Abelian.hasFiniteLimits` `CategoryTheory.whisker_eq` `snd_δ` `CategoryTheory.Limits.pullback.lift_snd_assoc` `CategoryTheory.Category.assoc` `CategoryTheory.cancel_mono` `mono_L₂_f` `φ₁_L₂_f` `lift_φ₂`
`φ₁_L₂_f` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `P` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `CategoryTheory.ShortComplex.X₂` `φ₁` `CategoryTheory.ShortComplex.f` `φ₂`	—	`CategoryTheory.ShortComplex.Exact.lift_f` `CategoryTheory.balanced_of_strongMonoCategory` `CategoryTheory.strongMonoCategory_of_regularMonoCategory` `CategoryTheory.regularMonoCategoryOfNormalMonoCategory` `CategoryTheory.Abelian.toIsNormalMonoCategory` `L₂_exact` `mono_L₂_f`
`φ₁_L₂_f_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `P` `CategoryTheory.ShortComplex.X₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `L₂` `φ₁` `CategoryTheory.ShortComplex.X₂` `CategoryTheory.ShortComplex.f` `φ₂`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `φ₁_L₂_f`

CategoryTheory.ShortComplex.SnakeInput.Hom

Definitions

Name	Category	Theorems
`comp` 📖	CompOp	4 math math: `comp_f₁`, `comp_f₃`, `comp_f₂`, `comp_f₀`
`f₀` 📖	CompOp	17 math math: `CategoryTheory.ShortComplex.SnakeInput.naturality_δ`, `CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₁`, `CategoryTheory.ShortComplex.SnakeInput.comp_f₀`, `CategoryTheory.ShortComplex.SnakeInput.functorL₀_map`, `CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₂`, `CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map`, `CategoryTheory.ShortComplex.SnakeInput.functorP_map`, `CategoryTheory.ShortComplex.SnakeInput.comp_f₀_assoc`, `CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc`, `CategoryTheory.ShortComplex.SnakeInput.id_f₀`, `id_f₀`, `comm₀₁`, `ext_iff`, `comm₀₁_assoc`, `CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₁`, `comp_f₀`, `HomologicalComplex.HomologySequence.mapSnakeInput_f₀`
`f₁` 📖	CompOp	13 math math: `comp_f₁`, `comm₁₂`, `comm₁₂_assoc`, `CategoryTheory.ShortComplex.SnakeInput.functorL₁_map`, `CategoryTheory.ShortComplex.SnakeInput.functorP_map`, `HomologicalComplex.HomologySequence.mapSnakeInput_f₁`, `CategoryTheory.ShortComplex.SnakeInput.id_f₁`, `CategoryTheory.ShortComplex.SnakeInput.comp_f₁_assoc`, `id_f₁`, `comm₀₁`, `ext_iff`, `comm₀₁_assoc`, `CategoryTheory.ShortComplex.SnakeInput.comp_f₁`
`f₂` 📖	CompOp	16 math math: `CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁`, `comm₂₃`, `CategoryTheory.ShortComplex.SnakeInput.id_f₂`, `comm₁₂`, `CategoryTheory.ShortComplex.SnakeInput.naturality_φ₁_assoc`, `comm₂₃_assoc`, `comm₁₂_assoc`, `CategoryTheory.ShortComplex.SnakeInput.comp_f₂`, `ext_iff`, `CategoryTheory.ShortComplex.SnakeInput.comp_f₂_assoc`, `CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂`, `HomologicalComplex.HomologySequence.mapSnakeInput_f₂`, `CategoryTheory.ShortComplex.SnakeInput.naturality_φ₂_assoc`, `comp_f₂`, `id_f₂`, `CategoryTheory.ShortComplex.SnakeInput.functorL₂_map`
`f₃` 📖	CompOp	16 math math: `CategoryTheory.ShortComplex.SnakeInput.comp_f₃_assoc`, `CategoryTheory.ShortComplex.SnakeInput.naturality_δ`, `comm₂₃`, `CategoryTheory.ShortComplex.SnakeInput.functorL₁'_map_τ₃`, `HomologicalComplex.HomologySequence.mapSnakeInput_f₃`, `comm₂₃_assoc`, `CategoryTheory.ShortComplex.SnakeInput.composableArrowsFunctor_map`, `id_f₃`, `CategoryTheory.ShortComplex.SnakeInput.naturality_δ_assoc`, `CategoryTheory.ShortComplex.SnakeInput.functorL₃_map`, `CategoryTheory.ShortComplex.SnakeInput.comp_f₃`, `CategoryTheory.ShortComplex.SnakeInput.id_f₃`, `ext_iff`, `CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₃`, `CategoryTheory.ShortComplex.SnakeInput.functorL₂'_map_τ₂`, `comp_f₃`
`id` 📖	CompOp	4 math math: `id_f₃`, `id_f₀`, `id_f₁`, `id_f₂`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm₀₁` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₀` `CategoryTheory.ShortComplex.SnakeInput.L₁` `f₀` `CategoryTheory.ShortComplex.SnakeInput.v₀₁` `f₁`	—	—
`comm₀₁_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₀` `f₀` `CategoryTheory.ShortComplex.SnakeInput.L₁` `CategoryTheory.ShortComplex.SnakeInput.v₀₁` `f₁`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm₀₁`
`comm₁₂` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₁` `CategoryTheory.ShortComplex.SnakeInput.L₂` `f₁` `CategoryTheory.ShortComplex.SnakeInput.v₁₂` `f₂`	—	—
`comm₁₂_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₁` `f₁` `CategoryTheory.ShortComplex.SnakeInput.L₂` `CategoryTheory.ShortComplex.SnakeInput.v₁₂` `f₂`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm₁₂`
`comm₂₃` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₂` `CategoryTheory.ShortComplex.SnakeInput.L₃` `f₂` `CategoryTheory.ShortComplex.SnakeInput.v₂₃` `f₃`	—	—
`comm₂₃_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₂` `f₂` `CategoryTheory.ShortComplex.SnakeInput.L₃` `CategoryTheory.ShortComplex.SnakeInput.v₂₃` `f₃`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `comm₂₃`
`comp_f₀` 📖	mathematical	—	`f₀` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₀`	—	—
`comp_f₁` 📖	mathematical	—	`f₁` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₁`	—	—
`comp_f₂` 📖	mathematical	—	`f₂` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₂`	—	—
`comp_f₃` 📖	mathematical	—	`f₃` `comp` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₃`	—	—
`ext` 📖	—	`f₀` `f₁` `f₂` `f₃`	—	—	—
`ext_iff` 📖	mathematical	—	`f₀` `f₁` `f₂` `f₃`	—	`ext`
`id_f₀` 📖	mathematical	—	`f₀` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₀`	—	—
`id_f₁` 📖	mathematical	—	`f₁` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₁`	—	—
`id_f₂` 📖	mathematical	—	`f₂` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₂`	—	—
`id_f₃` 📖	mathematical	—	`f₃` `id` `CategoryTheory.CategoryStruct.id` `CategoryTheory.ShortComplex` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `CategoryTheory.Abelian.toPreadditive` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.ShortComplex.instCategory` `CategoryTheory.ShortComplex.SnakeInput.L₃`	—	—

---

← Back to Index