trivial group quotient

Stream: Is there code for X?

[Chris Birkbeck]

Do we have the following:

lemma quot_triv [group G] (H : subgroup G)
(h: quotient_group.quotient H ≃ quotient_group.quotient (⊤: subgroup G)) :
H = ⊤ :=sorry

I can prove it, but before trying PR it I thought I'd check I wasn't hidden somewhere as
it feels like something we must have somewhere.

[Kevin Buzzard]

I think the thing to prove is subsingleton (quotient_group.quotient H) -> H = top

[Adam Topaz]

In any case, I think it would be better to assume an isomorphism with punit as opposed to the quotient of G by G

[Adam Topaz]

Presumably we already know that G/G is isomorphic to punit

[Adam Topaz]

Oh, yeah, Kevin's suggestion is indeed the way to go

[Adam Topaz]

But then one would have to transfer a subsingleton instance from punit. Can transport_instance handle subsingleton?

[Chris Birkbeck]

Well in the proof I did, I was using trunc. I started by showing

def triv_rel (α: Sort*) : α → α → Prop :=
λ a b, true

lemma rel_triv (α: Type u) (r: α → α → Prop ) (h: quot r ≃ trunc α) : eqv_gen r = triv_rel α :=sorry

and built up from here. Is there a reason to use one of subsingleton , trunc ,punit over the others?

[Adam Topaz]

Kevin's suggestion says that whenever G/H has at most one element, one has H=G. If you have some subgroup for which you have an equivalence between G/H and punit, you would then need to transport a subsingleton instance to G/H to be able to use such a lemma.

[Adam Topaz]

It depends on how you intend to use this lemma

[Chris Birkbeck]

Sure I guess Kevin's suggestion is the most natural. The reason it came up was I was proving some subgroup is equal to top, so using the version I wrote reduced me to checking some quotient which I already knew was trivial.

[Chris Birkbeck]

In any case, I guess this isn't already somewhere.

[Chris Birkbeck]

OK so I've made a draft PR for this here #9092, the main result is

lemma quot_subsingleton_triv  (H : subgroup G)
 (h: subsingleton (quotient_group.quotient H)) : H = ⊤ :=

Any comments on things to improve are very welcome. Specially the names of some of these lemmas.