michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

generalize is_exact

Browse source
This commit is contained in:
Floris van Doorn 2017-03-30 15:02:14 -04:00
parent 3cd846a757
commit 91931ca338
6 changed files with 38 additions and 40 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
algebra/ses.hlean
View file

@ -3,7 +3,7 @@ Copyright (c) 2017 Egbert Rijke. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Egbert Rijke
Basic facts about short exact sequences.
Basic facts about short exact sequences.
At the moment, it only covers short exact sequences of abelian groups, but this should be extended to short exact sequences in any abelian category.
-/
@ -13,18 +13,14 @@ import algebra.group_theory hit.set_quotient types.sigma types.list types.sum .q
open eq algebra is_trunc set_quotient relation sigma sigma.ops prod prod.ops sum list trunc function group trunc
equiv is_equiv
structure is_exact {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
( im_in_ker : Π(a:A), g (f a) = 1)
( ker_in_im : Π(b:B), (g b = 1) → image_subgroup f b)
structure SES (A B C : AbGroup) :=
( f : A →g B)
( g : B →g C)
( Hf : is_embedding f)
( Hg : is_surjective g)
( ex : is_exact f g)
( ex : is_exact_ag f g)
definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image_subgroup f)) :=
definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f) : SES A B (quotient_ab_group (image_subgroup f)) :=
begin
have Hg : is_surjective (ab_qg_map (image_subgroup f)),
from is_surjective_ab_qg_map (image_subgroup f),
@ -37,7 +33,7 @@ definition SES_of_inclusion {A B : AbGroup} (f : A →g B) (Hf : is_embedding f)
intro a,
fapply qg_map_eq_one, fapply tr, fapply fiber.mk, exact a, reflexivity,
intro b, intro p,
fapply rel_of_ab_qg_map_eq_one, assumption
exact rel_of_ab_qg_map_eq_one _ p
end
definition SES_of_subgroup {B : AbGroup} (S : subgroup_rel B) : SES (ab_subgroup S) B (quotient_ab_group S) :=
@ -73,7 +69,7 @@ definition SES_of_homomorphism {A B : AbGroup} (f : A →g B) : SES (ab_kernel f
exact is_surjective_image_lift f,
fapply is_exact.mk,
intro a, induction a with a p, fapply subtype_eq, exact p,
intro a p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact a,
intro a p, fapply tr, fapply fiber.mk, fapply sigma.mk, exact a,
exact calc
f a = image_incl f (image_lift f a) : by exact homotopy_of_eq (ap group_fun (image_factor f)) a
... = image_incl f 1 : ap (image_incl f) p
@ -90,10 +86,10 @@ definition SES_of_isomorphism_right {B C : AbGroup} (g : B ≃g C) : SES trivial
fapply is_surjective_of_is_equiv,
fapply is_exact.mk,
intro a, induction a, fapply respect_one,
intro b p,
intro b p,
have q : g b = g 1,
from p ⬝ (respect_one g)⁻¹,
note r := eq_of_fn_eq_fn (equiv_of_isomorphism g) q,
from p ⬝ (respect_one g)⁻¹,
note r := eq_of_fn_eq_fn (equiv_of_isomorphism g) q,
fapply tr, fapply fiber.mk, exact unit.star, rewrite r,
end
@ -113,10 +109,10 @@ parameters {A B C : AbGroup} (ses : SES A B C)
local abbreviation q := ab_qg_map (kernel_subgroup g)
local abbreviation B_mod_A := quotient_ab_group (kernel_subgroup g)
--definition quotient_SES {A B C : AbGroup} (ses : SES A B C) :
--definition quotient_SES {A B C : AbGroup} (ses : SES A B C) :
-- quotient_ab_group (image_subgroup (SES.f ses)) ≃g C :=
-- begin
-- fapply ab_group_first_iso_thm B C (SES.g ses),
-- fapply ab_group_first_iso_thm B C (SES.g ses),
-- end
-- definition pre_right_extend_SES (to separate the following definition and replace C with B/A)
@ -137,7 +133,7 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
(Σ (h : C →g C'), h ∘g g ~ k) ≃ (Σ (h' : B_mod_A →g C'), h' ∘g q ~ k) :=
begin
fapply equiv.mk,
intro pair, induction pair with h H,
intro pair, induction pair with h H,
fapply sigma.mk, exact h ∘g α, intro b,
exact H b,
fapply adjointify,
@ -153,8 +149,8 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
esimp, fapply is_prop.elimo, fapply pi.is_trunc_pi, intro a, fapply is_trunc_eq,
end
parameters {A' B' C' : AbGroup}
(ses' : SES A' B' C')
parameters {A' B' C' : AbGroup}
(ses' : SES A' B' C')
(hA : A →g A') (hB : B →g B') (htpy1 : hB ∘g f ~ (SES.f ses') ∘g hA)
local abbreviation f' := SES.f ses'
@ -162,12 +158,12 @@ definition quotient_triangle_extend_SES {C': AbGroup} (k : B →g C') :
local abbreviation ex' := SES.ex ses'
local abbreviation q' := ab_qg_map (kernel_subgroup g')
local abbreviation α' := quotient_codomain_SES
include htpy1
definition quotient_extend_unique_SES : is_contr (Σ (hC : C →g C'), hC ∘g g ~ g' ∘g hB) :=
definition quotient_extend_unique_SES : is_contr (Σ (hC : C →g C'), hC ∘g g ~ g' ∘g hB) :=
begin
fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))),
fapply @(is_trunc_equiv_closed_rev _ (quotient_triangle_extend_SES (g' ∘g hB))),
fapply ab_qg_universal_property,
intro b, intro K,
have k : trunctype.carrier (image_subgroup f b), from is_exact.ker_in_im ex b K,
@ -198,7 +194,7 @@ definition quotient_extend_SES_square : k ∘g (ab_qg_map (kernel_subgroup g)) ~
fapply quotient_group_compute
end
definition right_extend_SES : C →g C' :=
definition right_extend_SES : C →g C' :=
α' ∘g k ∘g α⁻¹ᵍ
local abbreviation hC := right_extend_SES
@ -229,7 +225,7 @@ definition right_extend_SES_unique_map (hC' : C →g C') (htpy2' : hC' ∘g g ~
begin
exact calc
hC ~ α' ∘g k ∘g α⁻¹ᵍ : by reflexivity
... ~ α' ∘g α'⁻¹ᵍ ∘g hC' ∘g α ∘g α⁻¹ᵍ :
... ~ α' ∘g α'⁻¹ᵍ ∘g hC' ∘g α ∘g α⁻¹ᵍ :
... ~ hC' ∘g α ∘g α⁻¹ᵍ : _
... ~ hC' : _
end

12
homotopy/cohomology.hlean
View file

@ -11,18 +11,6 @@ import .spectrum .EM ..algebra.arrow_group .fwedge ..choice .pushout ..move_to_l
open eq spectrum int trunc pointed EM group algebra circle sphere nat EM.ops equiv susp is_trunc
function fwedge cofiber bool lift sigma is_equiv choice pushout algebra unit pi
-- TODO: move
structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → image f b)
definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
is_exact f g
definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
(H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
is_exact.mk H₁ H₂
definition is_exact_trunc_functor {A B : Type} {C : Type*} {f : A → B} {g : B → C}
(H : is_exact_t f g) : @is_exact _ _ (ptrunc 0 C) (trunc_functor 0 f) (trunc_functor 0 g) :=
begin

4
homotopy/pushout.hlean
View file

@ -464,10 +464,6 @@ namespace pushout
/- universal property of cofiber -/
structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
definition cofiber_exact_1 {X Y Z : Type*} (f : X →* Y) (g : pcofiber f →* Z) :
(g ∘* pcod f) ∘* f ~* pconst X Z :=
!passoc ⬝* pwhisker_left _ !pcod_pcompose ⬝* !pcompose_pconst

2
homotopy/spherical_fibrations.hlean
View file

@ -59,7 +59,7 @@ namespace spherical_fibrations
begin
intro X, cases X with X p,
apply sigma.mk (psusp X), induction p with f, apply tr,
apply susp.psusp_equiv f
apply susp.psusp_pequiv f
end
definition BF_of_BG {n : ℕ} : BG n → BF n :=

18
move_to_lib.hlean
View file

@ -8,6 +8,24 @@ open eq nat int susp pointed pmap sigma is_equiv equiv fiber algebra trunc trunc
definition add_comm_right {A : Type} [add_comm_semigroup A] (n m k : A) : n + m + k = n + k + m :=
!add.assoc ⬝ ap (add n) !add.comm ⬝ !add.assoc⁻¹
structure is_exact_t {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → fiber f b)
structure is_exact {A B : Type} {C : Type*} (f : A → B) (g : B → C) :=
( im_in_ker : Π(a:A), g (f a) = pt)
( ker_in_im : Π(b:B), (g b = pt) → image f b)
definition is_exact_g {A B C : Group} (f : A →g B) (g : B →g C) :=
is_exact f g
definition is_exact_ag {A B C : AbGroup} (f : A →g B) (g : B →g C) :=
is_exact f g
definition is_exact_g.mk {A B C : Group} {f : A →g B} {g : B →g C}
(H₁ : Πa, g (f a) = 1) (H₂ : Πb, g b = 1 → image f b) : is_exact_g f g :=
is_exact.mk H₁ H₂
namespace algebra
definition inf_group_loopn (n : ℕ) (A : Type*) [H : is_succ n] : inf_group (Ω[n] A) :=
by induction H; exact _

2
pointed.hlean
View file

@ -930,7 +930,7 @@ namespace pointed
(ppcompose_left_loop_phomotopy' (pmap_of_map f x₀) !pconst) :=
begin
fapply phomotopy.mk,
{ esimp, esimp [pmap_eq_equiv], intro p,
{ esimp, intro p,
refine _ ⬝ ap011 (λx y, phomotopy_of_eq (ap1_gen _ x y _))
proof !eq_of_phomotopy_refl⁻¹ qed proof !eq_of_phomotopy_refl⁻¹ qed,
refine _ ⬝ ap phomotopy_of_eq !ap1_gen_idp_left⁻¹,