Notation for quotient group elements

Stream: Is there code for X?

[Edward van de Meent]

I'm currently trying to define a property of cosets of a certain normal subgroup.
for this, i need to treat elements of the quotient as cosets. (i'd like to define a function which means i need to be able to talk about the collection of cosets, as a type)

what is the preferred spelling for this? there are currently two ways to spell this (which don't appear to be defeq, sadly), but my personal preference would be a third yet-to-be-added option... take the following example:

import Mathlib.GroupTheory.Coset

variable {G:Type*} [CommGroup G] (N:Subgroup G) (g : G) (a : G ⧸ N)

#check (⟦g⟧  = a) -- option 1. does not have as great of an api as option 2.
#check (QuotientGroup.mk g = a) -- option 2. using `rfl` doesn't unify this with option 1. this does seem to have good api, however.
#check (↑g = a) -- the same as option 2, but with coe-sugar

-- preferably i'd like to write things like g ∈ a.

i am a bit at a loss for what i should do here, because at least ⟦g⟧ is close to the notation you might come across in a paper as denoting a coset. i would rather not use ↑g as meaning "the coset containing g".

[Andrew Yang]

import Mathlib.GroupTheory.Coset

variable {G:Type*} [CommGroup G] (N:Subgroup G) (g : G) (a : G ⧸ N)

example : QuotientGroup.mk (s := N) g = ⟦g⟧ := rfl

This works for me though

[Andrew Yang]

But you are right that mathlib prefer QuotientGroup.mk more.

[Andrew Yang]

Do you have a concrete example of what you need? I'm guessing that G ⧸ N is good enough but I have to see the applications to make sure.

[Edward van de Meent]

ah, i realise why i thought they weren't defeq: the simp-nf is not the same for them.

example (x y : G) : (⟦x⟧ : G ⧸ N) = ⟦y⟧ ↔ (↑x : G ⧸ N) = ↑y := by
  simp? says simp only [Quotient.eq]
  sorry

[Edward van de Meent]

and at that point they no longer unify with rfl

[Edward van de Meent]

Andrew Yang said:

But you are right that mathlib prefer QuotientGroup.mk more.

but the square brackets look so much nicer :smiling_face_with_tear:

[Edward van de Meent]

as for my specific use case, i'd like to pick the infimum of a function G -> Nat per-coset. i already have Fintype N, all that really seems to be missing is an instance of SetLike (G/N) G...

[Kevin Buzzard]

Yeah I think SetLike would be a nice way of doing it; we're currently experimenting with SetLike for RingCon as a model for two-sided ideals at Imperial and it's working great.

[Edward van de Meent]

it is a bit annoying that you would have to define these instances for all instances of HasQuotient because the notation seems to be opaque... it would have been a bit easier if the way to say A / B has some meaning was rather something along these lines:

class AlternativeQuotientClass (A B : Type*) where
  to_setoid : B -> Setoid A

def AlternativeQuotientClass.Quotient ( A :Type*) { B:Type*} [inst: AlternativeQuotientClass A B] (b:B) :=
  Quotient (inst.to_setoid b)

this way, you can give a single instance for SetLike (A / b) A. Would i be correct in assuming that this definition would still be a fit for most of mathlib?

[Kevin Buzzard]

The advantage of Lean's opaque quotients is that the proof that the universal diagram commutes is rfl, and if quotients were defined via setoids then the universal property would spit out functions which would not even be computable ("use the axiom of choice to take a random element of the coset, and apply the function to that").

[Edward van de Meent]

i think there is some kind of miscommunication here... for instance,
there is the following definition:

instance instHasQuotientSubgroup : HasQuotient α (Subgroup α) :=
  ⟨fun s => Quotient (leftRel s)⟩

[Edward van de Meent]

i don't see the problem with making this go via AlternativeQuotientClass...

[Edward van de Meent]

this quotient is already defined via a setoid

[Edward van de Meent]

not as one, but via one

[Kevin Buzzard]

Sorry, you're right. Rather than editing my message and confusing things even more I'll say what I meant to say here: if quotients were defined via equivalence classes (i.e. a type whose terms were subsets) then (what I said above).

[Andrew Yang]

While this might work, I think practically every A / B in mathlib is based on HasQuotient α (Subgroup α) or its additive version, so I don't think it is that much of a work to "define these instances for all instances of HasQuotient" (which is practically two, and practically one under to_additive)?

[Kevin Buzzard]

(But now I realise that "define them as equivalence classes" is not what you're suggesting)

[Edward van de Meent]

Andrew Yang said:

While this might work, I think practically every A / B in mathlib is based on HasQuotient α (Subgroup α) or its additive version, so I don't think it is that much of a work to "define these instances for all instances of HasQuotient" (which is practically two, and practically one under to_additive)?

as i've just found out : Not the case. i defined the version for AddSubgroup, but because i'm actually taking the quotient with Submodule, it fails to synthesise the instance...

[Andrew Yang]

I don't think we have quotients by submonoids?

[Edward van de Meent]

oh sorry i meant submodules

[Andrew Yang]

Yeah but it should be one line away?

[Edward van de Meent]

the point is that you're still duplicating code

[Edward van de Meent]

also, i'm not sure how you'd make it one line?

variable {G : Type*} [AddGroup G] {N : AddSubgroup G}
instance QuotientAddGroup.instSetLike : SetLike (G ⧸ N) G where
  coe := fun x => {y | (y :G ⧸ N) = x}
  coe_injective' := fun x => by
    intro y heq
    simp only at heq
    rw [Set.ext_iff] at heq
    obtain ⟨x',hx'⟩ := QuotientAddGroup.mk_surjective x
    specialize heq x'
    simp only [mem_setOf_eq, hx',true_iff] at heq
    exact heq

variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M)

#synth SetLike (M ⧸ p) M -- this fails

here is a #mwe , if you'd like to give it a try

[Andrew Yang]

I think
instance : SetLike (A / B) A := inferInstanceAs (SetLike (A / B.toAddSubgroup) A)
is the best you can get?

[Edward van de Meent]

that is short :thinking:

[Patrick Massot]

Please, please don’t make it easy to see elements of G/N as sets in G. This will only encourage people to write bad code. This is a habit inherited from teachers trying to be nice to students discovering abstract maths, but in the long run this is making everything more complicated. In 99% cases those people should be using the universal property, and for the other cases we still have the projection to the quotient.

[Andrew Yang]

I think for his particular use case, it is fine to have this API? Is including this piece of warning somewhere near the scoped instance good enough?

[Edward van de Meent]

personally i don't see the harm. The fact that the type depends on those parameters already means that there are many types for "the same" group. Also, a proof is a proof is a proof, and when that proof becomes more understandable because it has an intuitive representation, that is a better proof imo

[Patrick Massot]

No, that’s not how formalized math work. I’m sure you will be happier in the long run if you try to think in more efficient terms, and change your intuition if needed.

[Patrick Massot]

Could you share your code so that we can have a less abstract discussion?

[Edward van de Meent]

i'm afraid it's a bit much to share as a #mwe... i'm currently working on formalizing the simplicity of the Mathieu-24 group

[Edward van de Meent]

for that, i have defined the extended binary GolayCode

[Edward van de Meent]

in order to prove simplicity, i will need to define the action of the automorphisms of the GolayCode (which are some mononomials on 2^24) on the cosets where the minimal weight is equal to 4

[Edward van de Meent]

this "minimal weight" notion is where i need the coersion to sets.

[Edward van de Meent]

i intend to define the following function:

golay_code_space := Fin 4 x Fin 6 -> ZMod 2
noncomputable def minimal_weight (x : golay_code_space / GolayCode) : Nat

[Edward van de Meent]

i intend on doing this by casting x:(golay_code_space / GolayCode) to Finset (Fin 4 x Fin 6), then using Finset.inf' with hammingNorm : golay_code_space -> Nat

[Patrick Massot]

We cannot really be sure without seeing what you need to prove, but with what you provided so far, it seems you could define your minimal_weight function using

import Mathlib

open Function QuotientGroup

variable {G : Type*} [CommGroup G] {N : Subgroup G}

noncomputable def foo (f : G → ℕ) (x : G ⧸ N) : G :=
  argminOn f wellFounded_lt (mk ⁻¹' {x}) (mk_surjective x)

noncomputable def bar (f : G → ℕ) (x : G ⧸ N) : ℕ :=
  f (foo f x)

How is that more complicated than trying to get a SetLike instance?

[Patrick Massot]

This is using docs#Function.argminOn

[Patrick Massot]

Note that finiteness of N is completely irrelevant here since ℕ is well-founded.

[Scott Carnahan]

As far as simplicity of M24 is concerned, have you considered the outline given in PlanetMath, which just uses multiple transitivity of the permutation action?

[Edward van de Meent]

i had not. however, it would seem that that still relies on the simplicity of projective special linear groups in addition to the fact that M21 is isomorphic to PSL (3,F4), neither of which seem easy to prove (from my perspective) or are in mathlib

[Edward van de Meent]

i am attempting to follow the proof in The Finite Simple Groups

[Patrick Massot]

Did you coordinate with @Antoine Chambert-Loir? He worked a lot on Iwasawa’s simplicity criterion.

[Edward van de Meent]

i did not coordinate, but i am aware of their work. i am planning on assuming the criterion.

[Antoine Chambert-Loir]

In any case, the Iwasawa criterion is now a PR, #12048 (with merge conflicts to solve, and a few dependent PR before that…)