<commit_before>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import category_theory.abelian.pseudoelements

/-!
# The four lemma

Consider the following commutative diagram with exact rows in an abelian category:

A ---f--> B ---g--> C ---h--> D
|         |         |         |
α         β         γ         δ
|         |         |         |
v         v         v         v
A' --f'-> B' --g'-> C' --h'-> D'

We prove the "mono" version of the four lemma: if α is an epimorphism and β and δ are monomorphisms,
then γ is a monomorphism.

## Future work

The "epi" four lemma and the five lemma, which is then an easy corollary.

## Tags

four lemma, diagram lemma, diagram chase
-/
open category_theory (hiding comp_apply)
open category_theory.abelian.pseudoelement

universes v u

variables {V : Type u} [category.{v} V] [abelian V]

local attribute [instance] preadditive.has_equalizers_of_has_kernels<commit_msg>chore(category_theory/abelian/diagram_lemmas/four): Make the diagram into a code block (#8192)<commit_after>/-
Copyright (c) 2020 <NAME>. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: <NAME>
-/
import category_theory.abelian.pseudoelements

/-!
# The four lemma

Consider the following commutative diagram with exact rows in an abelian category:

```
A ---f--> B ---g--> C ---h--> D
|         |         |         |
α         β         γ         δ
|         |         |         |
v         v         v         v
A' --f'-> B' --g'-> C' --h'-> D'
```

We prove the "mono" version of the four lemma: if α is an epimorphism and β and δ are monomorphisms,
then γ is a monomorphism.

## Future work

The "epi" four lemma and the five lemma, which is then an easy corollary.

## Tags

four lemma, diagram lemma, diagram chase
-/
open category_theory (hiding comp_apply)
open category_theory.abelian.pseudoelement

universes v u

variables {V : Type u} [category.{v} V] [abelian V]

local attribute [instance] preadditive.has_equalizers_of_has_kernels
{'fraction_non_alphanumeric': 0.10624106717484516, 'fraction_numerical': 0.007622677465459742, 'mean_word_length': 2.488372093023256, 'pattern_counts': {'":': 0, '<': 7, '<?xml version=': 0, '>': 19, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3221792', 'n_tokens_mistral': 713, 'n_tokens_neox': 645, 'n_words': 265}