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

is_embedding_ab_subgroup_of_subgroup_incl

Browse source
This commit is contained in:
Egbert Rijke 2017-04-20 15:45:00 -04:00
parent 07d775563b
commit fd5d774e55
1 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
algebra/subgroup.hlean
View file

@ -427,9 +427,22 @@ namespace group
:=
subgroup_functor (gid G) H
definition is_embedding_subgroup_of_subgroup_incl {R S : subgroup_rel G} (H : Π (g : G), R g -> S g) : is_embedding (subgroup_of_subgroup_incl H) :=
begin
fapply is_embedding_of_is_injective,
intro x y p,
induction x with x r, induction y with y s,
fapply subtype_eq, esimp,
unfold subgroup_of_subgroup_incl at p, exact ap pr1 p,
end
definition ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : ab_subgroup R →g ab_subgroup S
:=
ab_subgroup_functor (gid A) H
definition is_embedding_ab_subgroup_of_subgroup_incl {A : AbGroup} {R S : subgroup_rel A} (H : Π (a : A), R a -> S a) : is_embedding (ab_subgroup_of_subgroup_incl H) :=
begin
fapply is_embedding_subgroup_of_subgroup_incl,
end
end group