RFC: QuotientGroup etc

Stream: mathlib4

[Yury G. Kudryashov]

What do you think about the following refactor?

• drop docs#HasQuotient
• instead, introduce notations α ⧸* M and α ⧸+ M (or similar) for quotients by multiplicative and additive actions

This will change the definition from left cosets to right cosets, but they're propeq for a normal subgroup.

[Yury G. Kudryashov]

Or should we adjust notation to use left cosets by default to preserve defeq?

[Edward van de Meent]

do i understand correctly that the motivation for this is to change from left to right cosets? or is there some other reason?

[Edward van de Meent]

because i don't see the problem with using left cosets

[Yury G. Kudryashov]

My main reason is to make equality of G ⧸ H to the quotient by orbitRel more visible.

[Yury G. Kudryashov]

(i.e., not hidden behind multiple semireducible defs)

[Yury G. Kudryashov]

See #15483 for one source of motivation. Also, we have to force Lean to use the defeq when we apply generic lemmas about quotient by an action to group quotient in measure theory.

[Yury G. Kudryashov]

The only reason why I suggest right cosets is that they are given by orbitsRel H G, without H.op.

[Yury G. Kudryashov]

But this usage may disagree with literature, then we should use the action of the opposite (sub)group.

[Yury G. Kudryashov]

/me is away for a few hours.

[Edward van de Meent]

i think making a definition for quotients by an action is a good idea. i don't know if it will be able to completely replace the current quotients, but it can be a decent idea to try.

[Edward van de Meent]

quotients by actions (i think) would allow for another way to talk about primitive and transitive group actions.

[Edward van de Meent]

on the other hand, i don't know if it's a common pattern but it does make it so you can't talk about quotients by non-canonical MulAction G G...

[Edward van de Meent]

perhaps you really want quotients by the action map G ->* (A ≃ A)

[Edward van de Meent]

so the instances don't overlap

[Yury G. Kudryashov]

We use type tags for non-canonical actions. E.g., docs#ConjAct

[Yury G. Kudryashov]

It would be nice if someone who actually used both left and right cosets in their research comments on pros/cons of different approaches here. I saw these in a paper (e.g., in the definition of an infranilmanifold), but never actually used them.

[Eric Wieser]

Edward van de Meent said:

quotients by actions (i think) would allow for another way to talk about primitive and transitive group actions.

I think group quotients are already implemented as quotients by actions?

[Yury G. Kudryashov]

Yes but this defeq is hidden behind a semireducible definition or two.

[Eric Wieser]

Yes, this was more disputing my reading of Edward's claim that this unlocks new things mathematically.

[Eric Wieser]

Right now group quotients are defined as the quotient by the opposite action, right? At the time that was certainly done to avoid a behavior change, but I agree that removing the opposite would be a handy unification if it turns out not to matter.

[Edward van de Meent]

looking at it now, indeed it seems i was mistaken, except that it requires the action to be upon itself, rather than a different type.

[Yury G. Kudryashov]

Quotient groups were rewritten this way by @Heather Macbeth in !3#15045 based on this discussion: #maths > two different quotients by subgroup

[Andrew Yang]

What about

class HasQuotient (A : outParam <| Type u) (B : Type v) where
  quotientRel : B → Setoid A

abbrev HasQuotient.Quotient (A : outParam <| Type u) {B : Type v}
    [HasQuotient A B] (b : B) : Type max u v :=
  Quotient (HasQuotient.quotientRel b)

instead? Does this solve any problems?

[Yury G. Kudryashov]

All quotients we have are either the quotient by a multiplicative group action (1 instance) or the quotient by an additive group action (4 instances).

[Edward van de Meent]

i think the idea is to drop HasQuotient and rather define something like

-- not sure about outparams here yet
@[to_additive]
def MulActionQuotient (A B : Type*) [Group B] [MulAction B A] : Type _ :=
  Quotient (MulAction.orbitRel B A)

[Edward van de Meent]

or at least, that's what what i'd expect

[Edward van de Meent]

and then do some notation tricks

[Matthew Ballard]

General observation: I've found the principle of preserving covariance of actions even at the expense of possibly introducing inversion to be a useful thing

[Yury G. Kudryashov]

What does it mean in this context?

[Yury G. Kudryashov]

@Edward van de Meent We already have docs#MulAction.orbitRel.Quotient (which is reducible).

[Edward van de Meent]

is that not what you're referring to then?

[Yury G. Kudryashov]

I suggest that we remove a semireducible def or two on the way from G ⧸ H to this type. With the most natural way, this will change the definition from left cosets to right cosets, but we can avoid this, if we want to.

[Eric Wieser]

A related issue is dealing with all the different mk functions for going from the ambient type to the quotient; I think the approach using Setoid as a type class is frowned upon, but writing a new mk function for each quotient (which we currently do) feels a bit like writing a new coeFn function for each hom

[Yury G. Kudryashov]

Currently, G ⧸ H is definitionally equal to the quotient by the action of H.op but sometimes Lean fails to see through this definitional equality, because it doesn't unfold some of the definitions on the way.

[Yury G. Kudryashov]

@Eric Wieser I think that we should migrate to Quot r and [IsEquivalence r] but I'm too lazy to implement this.

[Eric Wieser]

Yury G. Kudryashov said:

Eric Wieser I think that we should migrate to Quot r and [IsEquivalence r] but I'm too lazy to implement this.

That sounds like one of quite a few sensible design choices; it might be worth enumerating more of them (on a wiki page?) before attempting any refactor.

[Eric Wieser]

Yury G. Kudryashov said:

Currently, G ⧸ H is definitionally equal to the quotient by the action of H.op but sometimes Lean fails to see through this definitional equality, because it doesn't unfold some of the definitions on the way.

What specifically are those definitions?

[Yury G. Kudryashov]

One of them is docs#QuotientGroup.leftRel

[Yury G. Kudryashov]

Also, I don't know which defs around HasQuotient get unfolded and which aren't.

[Yuyang Zhao]

Should we reduce the use of (· ≈ ·) and docs#Setoid.r in favor of docs#Setoid.Rel or even make Setoid a FunLike?

[Yuyang Zhao]

Currently Quotient APIs usually use (· ≈ ·) and docs#Setoid.r, which is annoying to use.

[Yuyang Zhao]

Yury G. Kudryashov said:

My main reason is to make equality of G ⧸ H to the quotient by orbitRel more visible.

It can be done after some further improvements to #15586, but there is a significant slowdown.

[Eric Wieser]

Yuyang Zhao said:

Should we reduce the use of (· ≈ ·) and docs#Setoid.r in favor of docs#Setoid.Rel

I think we're somewhat stuck here because docs#Setoid.r is in core yet docs#Setoid.Rel is in mathlib. So we might need a Lean RFC to tidy this up

[Eric Wieser]

(deleted)

[Eric Wieser]

I think ultimately it comes down to disagreement about whether docs#Setoid should be a class or a structure

[Yury G. Kudryashov]

Yuyang Zhao said:

Yury G. Kudryashov said:

My main reason is to make equality of G ⧸ H to the quotient by orbitRel more visible.

It can be done after some further improvements to #15586, but there is a significant slowdown.

Do you understand why does it make things slower?

[Yuyang Zhao]

It got better after adding Ideal.instHasQuotient back. The rest might be because simp can use lemmas about Quotient now.

[Yury G. Kudryashov]

The rest might be because simp can use lemmas about Quotient now.

Will it be better if we make MulAction.orbitRel.Quotient semireducible, then reducibly unfold to it?

[Yury G. Kudryashov]

(then we should rename it to MulAction.Orbits)

[Johan Commelin]

I tried to use quotients and orbitRel about two weeks ago, and I also found the current API lacking. So I'm in favour of Yury's proposal.

[Yury G. Kudryashov]

I won't have time to implementstart implementing it until next weekend.

[Yury G. Kudryashov]

Should G ⧸ H remain the quotient by the right action, or should we make it the quotient by the left action, with an explicit op somewhere required to use the right action?

[Johan Commelin]

Maybe worth a poll?

[Yury G. Kudryashov]

/poll Should G ⧸ H remain the quotient by the right action?
G ⧸ H becomes the quotient by the left action; more generally, X ⧸ G is the quotient of X by the action of G
G ⧸ H remains the quotient by the right action

[Yury G. Kudryashov]

I like the first approach, because it generalizes to X ⧸ G, and one can deal with right action by using MulOpposite or Subgroup.op.

[Matthew Ballard]

Or use inversion on the action group.

[Yury G. Kudryashov]

@Sébastien Gouëzel Could you please explain why leaving G ⧸ H is a better choice? I guess, you have some reason I don't see.

[Yury G. Kudryashov]

I added one more option, tagging all who already voted @Edward van de Meent @Yaël Dillies @Johan Commelin @Matthew Ballard @Sébastien Gouëzel

[Yury G. Kudryashov]

/poll Should we continue using the same notation for multiplicative and additive quotients?
Continue using ⧸ or ⧹ for both
Use different notation for multiplicative and additive quotients

[Johan Commelin]

If we can use ⧸ or ⧹ for both, that would be great. But I fear that diamonds will force us to disambiguate at some point

[Eric Wieser]

I think we can choose the notation independently of the underlying Expr

[Eric Wieser]

I don't think we have any situations where T / S is ambiguously additive or multiplicative?

[Sébastien Gouëzel]

Yury G. Kudryashov said:

Sébastien Gouëzel Could you please explain why leaving G ⧸ H is a better choice? I guess, you have some reason I don't see.

It's just because, in usual mathematics, G / H is the quotient on the right, and H \ G is the quotient on the left. So I'd rather write H \ G for the quotient, i.e., I am on board with option 3.

[Kevin Buzzard]

Re the first poll: I'm not at lean for the next week but I just want to make sure I'm understanding this. Are lots of people voting for "make G/H not mean {gH : g in H} and thus deviate from the mathematical literature"? I would be strongly against deviations from the literature. There should be a natural left action of G on G/H, that's exactly why H is written on the right. If you want right cosets the notation is H\G and if you want double cosets HgK the notation is H\G/K. Sorry if I've misunderstood, I have patchy reception and no computer

[Richard Copley]

I'm the lucky owner of an elementary group theory textbook [1] that uses right cosets by default. It writes the function name to the right of the argument for function application (at least when the author remembers!) and writes compositions "backwards" accordingly too. However, it does use the notation G/H for the quotient group (defined in terms of (right) cosets).
image.png

I like the book, and there are advantages to those choices, but it's idiosyncratic. It's much more common in recent books to use left cosets by default, and that's what newcomers will expect. I think the combination of writing functions on the left (which I assume we're not changing!?) and using right cosets would be particularly odd in informal mathematics: we would have (Nσ)τ = N(τ∘σ) when σ,τ ∈ G are permutations and N ⊲ G, so we'd probably have to start defining σ * τ := τ ∘ σ. Not wrong or impossible, but confusing.

[1] Groups and Geometry, Peter M. Neumann, Gabrielle A. Stoy, and Edward C. Thompson

[Patrick Massot]

We will not write $Na$ anyway. This would be a rather bad abstraction barrier breaking.

[Richard Copley]

Currently left cosets, which are not the same type as elements of the quotient, are written g • (H : Set G), and there is no notation for right cosets. (Unless this has changed in the past few weeks.)

[Yaël Dillies]

The notation is (H : Set G) <• g and has been there for a few months already

[Yaël Dillies]

See file#Algebra/Group/Action/Opposite

[Yaël Dillies]

The PR was #8909, merged in December 2023

[Patrick Massot]

But this isn't a notation for the projection to the quotient, right? So this is not the discussion topic?

[Richard Copley]

Quite. I did say "in informal mathematics". In the current notation, where the quotient G ⧸ H is by the right action (that is, informally: the elements of the quotient are left cosets), we have

import Mathlib.GroupTheory.QuotientGroup

example (X) (H : Subgroup (Equiv.Perm X)) [H.Normal] (s t : Equiv.Perm X) :
    (s : Equiv.Perm X ⧸ H) * (t : Equiv.Perm X ⧸ H) = (t.trans s : Equiv.Perm X ⧸ H) :=
  rfl

I was suggesting that this, corresponding to [edit: fixed] (Hσ)τ = H(στ), might be what a newcomer naturally expects, and that changing it would lead to confusion.

[Yury G. Kudryashov]

Following the discussion, I removed my vote from option 1, leaving at option 3.

[Yuyang Zhao]

Does using the QuotLike API in #16421 help with this? I think it's almost ready, but would require a massive refactoring in Mathlib to migrate to it.

[Yury G. Kudryashov]

I think that these 2 changes are orthogonal.

[Yuyang Zhao]

Yury G. Kudryashov said:

My main reason is to make equality of G ⧸ H to the quotient by orbitRel more visible.

Ah sorry, I meant to make the relation more visible.

[Yury G. Kudryashov]

Do you mean generalizing relevant theories from "defeq to the quotient" to QuotLike?

[Yury G. Kudryashov]

Do you expect to have instances of QuotLike other than Quotient/Quot?

[Yuyang Zhao]

QuotLike APIs specify the type of quotient and the relation using typeclasses. I think most of the definitions based on Quot / Quotient in Mathlib should have a QuotLike instance. This would avoid duplication of APIs and problems caused by directly using the Quotient API.

[Yaël Dillies]

This also surely comes up in group theory, right? Eg the first isomorphism theorem could be made into a QuotLike instance

[Yuyang Zhao]

We can definitely have QuotLike (range φ) G (leftRel (ker φ)) if we need

[Yuyang Zhao]

I feel that #16421 is ready. Some of the naming may need to be discussed. For example, ⟦·⟧ is currently called mkQ in names. This distinguishes it from other .mks and makes it possible to write the quotient map as mkQ mkQ' mkQ_ h. But this will also require changing the old lemma names.