Question about Subgroup.index

Stream: maths

[Ching-Tsun Chou]

The index of a subgroup H of a group G is defined to be the cardinality of the quotient G/H:

https://leanprover-community.github.io/mathlib4_docs/Mathlib/GroupTheory/Index.html#Subgroup.index

But isn't it the case that the quotient group is well-defined only if H is a normal subgroup of G? The definition above does not seem to require that H be a normal subgroup.

[Ben Eltschig]

In general it's the type of left cosets of the subgroup. See QuotientGroup.instHasQuotientSubgroup.

[Ben Eltschig]

As for how you could have found this yourself, aside from just knowing what definition to search for - if you type

variable {G : Type*} [Group G] {H : Subgroup G}

#check G ⧸ H

in a file with the right imports, and hover over G ⧸ H in the infoview on the right, it will tell you that the term elaborated to
@HasQuotient.Quotient G (Subgroup G) QuotientGroup.instHasQuotientSubgroup H. I don't know what's the best way to look stuff like this up, but at least personally I've found using #check and then hovering over stuff in the infoview quite useful.

[Ching-Tsun Chou]

So G/H is defined by any subgroup H of any group G but it is a group only when H is a normal subgroup of G. Thanks for the tip for how to find the definition!

[Patrick Massot]

Ben Eltschig said:

In general it's the type of left cosets of the subgroup. See QuotientGroup.instHasQuotientSubgroup.

This is not quite true, it is the quotient type associated to the relevant action of the subgroup. It is isomorphic to the type of left cosets, but that is not how it is defined.

[Ching-Tsun Chou]

Alas, I have a more basic question: Why does Lean say it can't synthesize the type of G/H in the following example?

import Mathlib.GroupTheory.Index
import Mathlib.Tactic
import Mathlib.Util.Delaborators

open Subgroup

variable {G : Type*} [Group G] (H : Subgroup G)

#check (G / H)

[Ching-Tsun Chou]

The error msg is:

failed to synthesize
  HDiv (Type u_1) (Subgroup G) ?m.429

[Thomas Browning]

The division symbol needs to be a fancy unicode \quot rather than just /

[Ching-Tsun Chou]

Ah, I see. Thanks!