Triviality of a quotient group implying subgroup is top

Stream: Is there code for X?

[Jordan Brown]

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?

[Mario Carneiro]

Do you have a theorem statement?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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