diff --git a/algebra/is_short_exact.hlean b/algebra/is_short_exact.hlean
new file mode 100644
index 0000000..3f94ced
--- /dev/null
+++ b/algebra/is_short_exact.hlean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2017 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jeremy Avigad
+
+Short exact sequences
+-/
+import .quotient_group
+open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc_index pi group
+     is_trunc function sphere unit sum prod
+
+structure is_short_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  (is_emb    : is_embedding f)
+  (im_in_ker : Π(a:A), g (f a) = pt)
+  (ker_in_im : Π(b:B), (g b = pt) → image f b)
+  (is_surj   : is_surjective g)
+
+structure is_short_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
+  (is_emb    : is_embedding f)
+  (im_in_ker : Π(a:A), g (f a) = pt)
+  (ker_in_im : Π(b:B), (g b = pt) → fiber f b)
+  (is_surj   : is_split_surjective g)