From c0ea92a0b514a300998ca7000d19a504dd205bb1 Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 8 Jun 2017 17:51:25 -0600 Subject: [PATCH] Add dirsum_functor_isomorphism. --- algebra/direct_sum.hlean | 30 ++++++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean index e691287..aeb3142 100644 --- a/algebra/direct_sum.hlean +++ b/algebra/direct_sum.hlean @@ -1,7 +1,7 @@ /- -Copyright (c) 2015 Floris van Doorn. All rights reserved. +Copyright (c) 2015 Floris van Doorn, Egbert Rijke, Favonia. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Floris van Doorn, Egbert Rijke +Authors: Floris van Doorn, Egbert Rijke, Favonia Constructions with groups -/ @@ -156,4 +156,30 @@ namespace group definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y := dirsum_elim (λj, dirsum_incl Y (f j)) + definition dirsum_functor_isomorphism [constructor] (f : Πi, Y i ≃g Y' i) : dirsum Y ≃g dirsum Y' := + let to_hom := dirsum_functor (λ i, f i) in + let from_hom := dirsum_functor (λ i, (f i)⁻¹ᵍ) in + begin + fapply isomorphism.mk, + exact dirsum_functor (λ i, f i), + fapply is_equiv.adjointify, + exact dirsum_functor (λ i, (f i)⁻¹ᵍ), + { intro ds, + refine (homomorphism_comp_compute (dirsum_functor (λ i, f i)) (dirsum_functor (λ i, (f i)⁻¹ᵍ)) _)⁻¹ ⬝ _, + refine dirsum_functor_compose (λ i, f i) (λ i, (f i)⁻¹ᵍ) ds ⬝ _, + refine @dirsum_functor_homotopy I Y' Y' _ (λ i, !gid) (λ i, to_right_inv (equiv_of_isomorphism (f i))) ds ⬝ _, + exact !dirsum_functor_gid + }, + { intro ds, + refine (homomorphism_comp_compute (dirsum_functor (λ i, (f i)⁻¹ᵍ)) (dirsum_functor (λ i, f i)) _)⁻¹ ⬝ _, + refine dirsum_functor_compose (λ i, (f i)⁻¹ᵍ) (λ i, f i) ds ⬝ _, + refine @dirsum_functor_homotopy I Y Y _ (λ i, !gid) (λ i x, + proof + to_left_inv (equiv_of_isomorphism (f i)) x + qed + ) ds ⬝ _, + exact !dirsum_functor_gid + } + end + end group