## Stream: Is there code for X?

### Topic: Triviality of a quotient group implying subgroup is top

#### 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?

#### Mario Carneiro (Nov 17 2020 at 05:36):

Do you have a theorem statement?

#### Mario Carneiro (Nov 17 2020 at 05:37):

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

#### 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


#### 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