Zulip Chat Archive

Stream: Is there code for X?

Topic: Triviality of a quotient group implying subgroup is top


view this post on Zulip Jordan Brown (Nov 17 2020 at 05:27):

Is there a result in mathlib that shows that, if G/H is trivial (which, in the case I am looking at, is represented by the bottom and top in subgroup G/H being equal), then H=G?

view this post on Zulip Mario Carneiro (Nov 17 2020 at 05:36):

Do you have a theorem statement?

view this post on Zulip Mario Carneiro (Nov 17 2020 at 05:37):

I guess you could prove it using docs#quotient_group.ker_mk

view this post on Zulip Mario Carneiro (Nov 17 2020 at 05:48):

import group_theory.quotient_group

namespace quotient_group
universes u v
variables {G : Type u} [group G] (N : subgroup G) [subgroup.normal N]

theorem eq_top_of_trivial_quotient (H : ( : subgroup (quotient N))  ) : N =  :=
begin
  rw [ ker_mk N, eq_top_iff, monoid_hom.ker,  subgroup.map_le_iff_le_comap],
  exact le_trans le_top H,
end
end quotient_group

view this post on Zulip Mario Carneiro (Nov 17 2020 at 05:51):

theorem eq_top_of_trivial_quotient (H : ( : subgroup (quotient N))  ) : N =  :=
(ker_mk N).symm.trans $ eq_top_iff.2 $ subgroup.map_le_iff_le_comap.1 $ le_trans le_top H

Last updated: May 07 2021 at 22:14 UTC