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

ab_subgroup_iso

Browse source
This commit is contained in:
Egbert Rijke 2017-05-18 16:44:42 -04:00
parent eaf7290def
commit 8382043184
1 changed files with 16 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
algebra/subgroup.hlean
View file

@ -469,6 +469,22 @@ definition ab_image_lift [constructor] {G H : AbGroup} (f : G →g H) : G →g i
fapply is_embedding_subgroup_of_subgroup_incl,
end
definition ab_subgroup_iso {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) :
ab_subgroup R ≃g ab_subgroup S :=
begin
fapply isomorphism.mk,
exact subgroup_of_subgroup_incl H,
fapply is_equiv.adjointify,
exact subgroup_of_subgroup_incl K,
intro s, induction s with a p, fapply subtype_eq, reflexivity,
intro r, induction r with a p, fapply subtype_eq, reflexivity
end
definition ab_subgroup_iso_triangle {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) (K : Π (a : A), S a -> R a) : incl_of_subgroup R ~ incl_of_subgroup S ∘g ab_subgroup_iso H K :=
begin
intro r, induction r, reflexivity
end
end group
open group