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

image of a surjection is the codomain

Browse source
This commit is contained in:
Steve Awodey 2017-01-26 16:44:49 -05:00
parent c09f568992
commit 271459d533
2 changed files with 23 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
algebra/.#exact_couple.hlean Symbolic link
View file

@ -0,0 +1 @@
Steve@steveawodeysAir.wv.cc.cmu.edu.6485

23
algebra/subgroup.hlean
View file

@ -281,7 +281,28 @@ namespace group
definition image_incl {G H : Group} (f : G →g H) : image f →g H :=
incl_of_subgroup (image_subgroup f)
definition comm_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image_subgroup f)
definition ab_image_incl {A B : AbGroup} (f : A →g B) : ab_image f →g B := incl_of_subgroup (image_subgroup f)
definition is_equiv_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H : is_surjective f) : is_equiv (ab_image_incl f ) :=
begin
fapply is_equiv.adjointify (ab_image_incl f),
intro b,
fapply sigma.mk,
exact b,
exact H b,
intro b,
reflexivity,
intro x,
apply subtype_eq,
reflexivity
end
definition iso_surjection_ab_image_incl {A B : AbGroup} (f : A →g B) (H : is_surjective f) : ab_image f ≃g B :=
begin
fapply isomorphism.mk,
exact (ab_image_incl f),
exact is_equiv_surjection_ab_image_incl f H
end
definition hom_lift {G H : Group} (f : G →g H) (K : subgroup_rel H) (Hyp : Π (g : G), K (f g)) : G →g subgroup K :=
begin