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

abgrpkernelquotientstuff

Browse source
This commit is contained in:
Steve Awodey 2017-02-10 12:07:48 -05:00
parent e3f1d64330
commit 92a4b95302
1 changed files with 17 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

17
algebra/quotient_group.hlean
View file

@ -346,7 +346,14 @@ definition ab_group_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p apply iff.mpr (ab_group_kernel_image_lift _ _ f a) p
end end
definition ab_group_kernel_quotient_to_image_triangle {A B : AbGroup} (f : A →g B) definition ab_group_kernel_quotient_to_image_domain_triangle {A B : AbGroup} (f : A →g B)
: ab_group_kernel_quotient_to_image (f) ∘g ab_qg_map (kernel_subgroup (f)) ~ image_lift(f) :=
begin
intros a,
esimp,
end
definition ab_group_kernel_quotient_to_image_codomain_triangle {A B : AbGroup} (f : A →g B)
: image_incl f ∘g ab_group_kernel_quotient_to_image f ~ kernel_quotient_extension f := : image_incl f ∘g ab_group_kernel_quotient_to_image f ~ kernel_quotient_extension f :=
begin begin
intro x, intro x,
@ -368,7 +375,7 @@ definition is_embedding_kernel_quotient_to_image {A B : AbGroup} (f : A →g B)
: is_embedding (ab_group_kernel_quotient_to_image f) := : is_embedding (ab_group_kernel_quotient_to_image f) :=
begin begin
fapply @is_embedding_factor _ (image f) B _ _ _ (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f), fapply @is_embedding_factor _ (image f) B _ _ _ (ab_group_kernel_quotient_to_image f) (image_incl f) (kernel_quotient_extension f),
exact ab_group_kernel_quotient_to_image_triangle f, exact ab_group_kernel_quotient_to_image_codomain_triangle f,
exact is_embedding_kernel_quotient_extension f exact is_embedding_kernel_quotient_extension f
end end
@ -388,6 +395,12 @@ definition codomain_surjection_is_quotient {A B : AbGroup} (f : A →g B)( H : i
exact (ab_group_first_iso_thm f) ⬝g (iso_surjection_ab_image_incl f H) exact (ab_group_first_iso_thm f) ⬝g (iso_surjection_ab_image_incl f H)
end end
definition codomain_surjection_is_quotient_triangle {A B : AbGroup} (f : A →g B)( H : is_surjective f)
: codomain_surjection_is_quotient (f)(H) ∘g ab_qg_map (kernel_subgroup f) ~ f :=
begin
intro a,
esimp
end
-- print iff.mpr -- print iff.mpr
/- set generating normal subgroup -/ /- set generating normal subgroup -/