From 89d65b1dca5f3ad00acc5ea3bfedf56ffcecfe7c Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 2 Mar 2017 17:06:13 -0500 Subject: [PATCH 1/2] add is_short_exact.hlean --- algebra/is_short_exact.hlean | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 algebra/is_short_exact.hlean diff --git a/algebra/is_short_exact.hlean b/algebra/is_short_exact.hlean new file mode 100644 index 0000000..e7422fc --- /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) From e7c174719b8eebc41a05a8c5957a3f282067fcef Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 2 Mar 2017 17:08:00 -0500 Subject: [PATCH 2/2] fix typo --- algebra/is_short_exact.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/algebra/is_short_exact.hlean b/algebra/is_short_exact.hlean index e7422fc..3f94ced 100644 --- a/algebra/is_short_exact.hlean +++ b/algebra/is_short_exact.hlean @@ -19,4 +19,4 @@ 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) + (is_surj : is_split_surjective g)