!4#3333 Data.ZMod.Quotient

Stream: PR reviews

[Mauricio Collares]

Parts of !4#3333 are massively complicated by the fact that we cannot make MulOpposite semireducible any more (as was done in mathlib3 via a local attribute). I just pushed a commit that manually re-does some of the MulEquivs there, but I don't know if that's the right approach. Feel free to just revert the commit if it is the wrong approach.

[Mauricio Collares]

I meant to post this in the mathlib4 stream, since this is not ready for review

[Kevin Buzzard]

docs4#MulOpposite

[Mauricio Collares]

Thanks. Also meant to say "semireducible" in the original message, fixed now.

[Kevin Buzzard]

Yeah, I was going to say "it's a structure, which has the same effect as being irreducible". So is the issue that the mathlib3 version abused definitional equality?

[Mauricio Collares]

Yes, locally

[Kevin Buzzard]

I have some Lean time now -- can you give me an example of something which is painful? I'd be interested to see.

[Mauricio Collares]

There are two rfl proofs in Data.ZMod.Quotient that don't work anymore (zpowersQuotientStabilizerEquiv_symm_apply, orbitZpowersEquiv_symm_apply). Those should be good examples. Or you can look at zpowersQuotientStabilizerEquiv before my last commit there.

[Mauricio Collares]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/two.20different.20quotients.20by.20subgroup (the whole thread) is related

[Eric Wieser]

So is the issue that the mathlib3 version abused definitional equality?

Or that it shouldn't have been irreducible in the first place; docs#add_opposite never was.

[Mauricio Collares]

Both are irreducible in mathlib4 at the moment

[Eric Wieser]

Worse, they're structures, right?

[Eric Wieser]

I don't remember the motivation, but maybe it's now moot after lean4#2210 landed and we can revert it?

[Mauricio Collares]

This was done in !4#1036. I quite like them as structures conceptually speaking, though. I wonder how many other files break, hopefully not many. My uneducated impression was that there's a lot of missing API on interactions between MulOpposite/AddOpposite and Multiplicative/Additive. There's discussion at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Order.2EGaloisConnection

[Eric Wieser]

It's specifically this quotient stuff where the defeq is needed

[Eric Wieser]

Here's a way to write that definition that might help preserve the defeqs we want:

  by
    letI f := zmultiplesQuotientStabilizerEquiv (Additive.ofMul a) b
    refine ((QuotientGroup.toQuotientAddGroup _).trans ?_).trans (AddEquiv.toMultiplicative f)
    refine AddEquiv.toMultiplicative ?_
    sorry

[Eric Wieser]

Specifically, this is the missing piece:

instance Normal.toAddSubgroup {G} [Group G] (S : Subgroup G) [Normal S] :
    AddSubgroup.Normal (Subgroup.toAddSubgroup S) :=
  sorry

def QuotientGroup.toQuotientAddGroup {G} [Group G] (S : Subgroup G) [Normal S] :
    G ⧸ S ≃* Multiplicative (Additive G ⧸ Subgroup.toAddSubgroup S) :=
sorry

[Kevin Buzzard]

How does one make the Subgroup of Multiplicative G corresponding to s : AddSubgroup G?
Edit: aah, you just told me!

Eric I don't follow your claim that defeq is _needed_. Why can't we just have a bunch of canonical isomorphisms? I'm pretty sure we already have the isomorphism G/M -> G/N coming from an equality M=N.

[Eric Wieser]

In lean3 those types were true by definition

[Eric Wieser]

Kevin, it's not _needed_ per se; but it was very convenient. Indeed, the isomorphism we're missing is the one I give above

[Eric Wieser]

I guess by "needed" what I mean is "structure eta alone is not enough to keep the defeqs we had in Lean 3"

[Eric Wieser]

Whereas for almost all other uses of MulOpposite, the defeqs we had in Lean3 are still around

[Kevin Buzzard]

The instance shouldn't be hard; as for the def, I feel like we should have a construction (Additive G \equiv+ A) \equiv (G \equiv* Multiplicative A), and this would I think help with it.

[Eric Wieser]

We have that, it's docs4#AddEquiv.toMultiplicative'

[Eric Wieser]

I'm pretty sure we already have the isomorphism G/M -> G/N coming from an equality M=N.

I agree, but I can't find it. Do you remember what it's called?

[Kevin Buzzard]

My suggestion has better notation ;-)

[Eric Wieser]

You mean it has the parens on both sides?

[Kevin Buzzard]

docs4#QuotientGroup.quotientMulEquivOfEq for the equality. No I just meant that I used A for an additive group.

[Eric Wieser]

QuotientGroup.toQuotientAddGroup will need to be an implemention of that function from scratch, with tweaked types

[Eric Wieser]

Hmm, maybe this whole problem goes away if we make MulOpposite and AddOpposite the same structure under the hood...

[Kevin Buzzard]

You are a Lean guru if you can guess the error I get from

import Mathlib.GroupTheory.QuotientGroup
import Mathlib.Algebra.Hom.Equiv.TypeTags

open Subgroup

instance Normal.toAddSubgroup {G} [Group G] (S : Subgroup G) [Normal S] :
    AddSubgroup.Normal (Subgroup.toAddSubgroup S) :=
  sorry

def QuotientGroup.toQuotientAddGroup {G} [Group G] (S : Subgroup G) [Normal S] :
    G ⧸ S ≃* Multiplicative (Additive G ⧸ Subgroup.toAddSubgroup S) :=
by convert AddEquiv.toMultiplicative' (AddEquiv.refl _)

[Kevin Buzzard]

failed to synthesize instance
  AddZeroClass ℕ+

[Eric Wieser]

error: nice try?

[Kevin Buzzard]

kind of

[Eric Wieser]

Yeah ok that's not on the list of things I expected

[Eric Wieser]

But it's going to ask you to prove that MulOpposite G = AddOpposite (Additive G), and that defeq broke

[Kevin Buzzard]

I'm confused about why opposites have got anything to do with anything.

[Eric Wieser]

Because the quotient is defined by the action by the opposite group (right multiplication)

[Eric Wieser]

So deep down there is an existential quantifying over MulOpposite

[Kevin Buzzard]

I was hoping Additive (G ⧸ S) = (Additive G ⧸ (Subgroup.toAddSubgroup S)) would be rfl

[Eric Wieser]

It's not, but it was in Lean 3 before we made MulOpposite a structure. That's the problem.

[Kevin Buzzard]

I guess this is an artificial hope anyway; really we should be writing down the isomorphisms, right?

[Eric Wieser]

Well, it depends where the threshold for "defeq abuse is ok" is

[Eric Wieser]

Eric Wieser said:

Hmm, maybe this whole problem goes away if we make MulOpposite and AddOpposite the same structure under the hood...

I'm trying this in https://github.com/leanprover-community/mathlib4/pull/4050

[Kevin Buzzard]

(I restarted Lean and the problem I posted went away)

[Kevin Buzzard]

(deleted)

[Eric Wieser]

(does your deleted code work?)

[Kevin Buzzard]

import Mathlib.GroupTheory.QuotientGroup
import Mathlib.Algebra.Hom.Equiv.TypeTags

open Subgroup

instance Normal.toAddSubgroup {G} [Group G] (S : Subgroup G) [Normal S] :
    AddSubgroup.Normal (Subgroup.toAddSubgroup S) where
  conj_mem := Normal.conj_mem (H := S) inferInstance

def QuotientGroup.toQuotientAddGroup {G} [Group G] (S : Subgroup G) [Normal S] :
    G ⧸ S ≃* Multiplicative (Additive G ⧸ toAddSubgroup S) :=
AddEquiv.toMultiplicative' sorry

Works fine (and is not slow as previously claimed)

[Eric Wieser]

Sure, but the sorry is just as hard as the original

[Eric Wieser]

(that instance should definitely be added to mathlib btw)

[Kevin Buzzard]

It doesn't have a mix of additive and multiplicative though, so it feels like progress.

[Kevin Buzzard]

Is it expected that I write toAddsubgroup S and Lean prettyprints it as the awful ↑(RelIso.toRelEmbedding toAddSubgroup).toEmbedding S?

[Eric Wieser]

!4#4050 works, and lets rfl close the sorry

[Kevin Buzzard]

docs4#Opposite

[Kevin Buzzard]

Why not just use Opposite?

[Eric Wieser]

Because I don't know whether we want Opposite to be defeq to MulOpposite

[Kevin Buzzard]

But you do think that we want AddOpposite to be defeq to MulOpposite??

[Kevin Buzzard]

Usually at this point you start going on about diamonds and semirings

[Kevin Buzzard]

It's certainly a hilarious fix though!

[Eric Wieser]

Yes, because we have Multiplicative X = Additive X right now, and it's weird to have that be true but not Multiplicative (AddOpposite X) = Additive (MulOpposite X)

[Eric Wieser]

It's a trade off between having "abuse" of defeqs and having to write lots of really stupid boilerplate

[Eric Wieser]

Until the abuse starts causing harm, the easier choice is to put off the boilerplate until it's really needed

[Kevin Buzzard]

With the advent of lean4#2210 I am a bit confused about which of def thing_which_bijects_with_X (X : Type) := X and structure thing_which_bijects_with_X (X : Type) := { random_name : X} we prefer nowadays.

[Eric Wieser]

The former is still a lot more convenient for avoiding boilerplate, which is why docs4#OrderDual still uses it

[Kevin Buzzard]

What's wrong with boilerplate? I should think ChatGPT could write it all by now anyway

[Eric Wieser]

Stuff like QuotientGroup.toQuotientAddGroup is fine, but it's nice when the stupid boilerplate can be proved by rfl

[Kevin Buzzard]

The "category theory" proof of Additive G ⧸ toAddSubgroup S ≃+ Additive (G ⧸ S) has the disadvantage that it uses the first isomorphism theorem (the isomorphism is induced from the surjection G -> G/S, additivised) so the inverse is noncomputable. I don't know how serious that problem is.

[Kevin Buzzard]

What the heck is going on here BTW? I have an obscure error:

import Mathlib.GroupTheory.QuotientGroup
import Mathlib.Algebra.Hom.Equiv.TypeTags

open Subgroup

instance Normal.toAddSubgroup {G} [Group G] (S : Subgroup G) [Normal S] :
    AddSubgroup.Normal (Subgroup.toAddSubgroup S) where
  conj_mem := Normal.conj_mem (H := S) inferInstance

def foo {G} [Group G] (S : Subgroup G) [Normal S] :
    Additive G ⧸ toAddSubgroup S ≃+ Additive (G ⧸ S) :=
  (QuotientAddGroup.quotientAddEquivOfEq sorry : Additive G ⧸ toAddSubgroup S ≃+ Additive G ⧸ _).trans
  (QuotientAddGroup.quotientKerEquivOfSurjective
    (MonoidHom.toAdditive (QuotientGroup.mk' S) : Additive G →+ Additive (G ⧸ S)) sorry)
/-
IR check failed at 'foo._rarg', error: unknown declaration 'QuotientAddGroup.quotientKerEquivOfSurjective'
-/

#check QuotientAddGroup.quotientKerEquivOfSurjective -- works fine

Edit: fixed by marking foo noncomputable. That's a pretty weird way to tell me to do that :-/

[Kevin Buzzard]

Here's what I imagine the "category theory philosophy" proof looks like:

import Mathlib.GroupTheory.QuotientGroup
import Mathlib.Algebra.Hom.Equiv.TypeTags
import Mathlib.Tactic

open Subgroup MonoidHom

instance Normal.toAddSubgroup {G} [Group G] (S : Subgroup G) [Normal S] :
    AddSubgroup.Normal (Subgroup.toAddSubgroup S) where
  conj_mem := Normal.conj_mem (H := S) inferInstance

lemma lemma1 {G H : Type _} [Group G] [Group H] (φ : G →* H) :
    Function.Surjective (toAdditive φ) ↔ Function.Surjective φ := Iff.rfl

lemma lemma2 {G} [Group G] (S : Subgroup G) [Normal S] :
    toAddSubgroup S = AddMonoidHom.ker (toAdditive (QuotientGroup.mk' S)) := by
  sorry

noncomputable def foo {G} [Group G] (S : Subgroup G) [Normal S] :
    Additive G ⧸ toAddSubgroup S ≃+ Additive (G ⧸ S) :=
  (QuotientAddGroup.quotientAddEquivOfEq (lemma2 S) : Additive G ⧸ toAddSubgroup S ≃+ Additive G ⧸ _).trans
  (QuotientAddGroup.quotientKerEquivOfSurjective
    (MonoidHom.toAdditive (QuotientGroup.mk' S) : Additive G →+ Additive (G ⧸ S)) $
    QuotientGroup.mk'_surjective S)

-- at least this part is computable
example {G} [Group G] (S T : Subgroup G) [Normal S] [Normal T] (h : S = T) (g : G) :
  QuotientGroup.quotientMulEquivOfEq h (QuotientGroup.mk g) = QuotientGroup.mk g := rfl

noncomputable def QuotientGroup.toQuotientAddGroup {G} [Group G] (S : Subgroup G) [Normal S] :
    G ⧸ S ≃* Multiplicative (Additive G ⧸ toAddSubgroup S) :=
AddEquiv.toMultiplicative' (foo S).symm

Still one sorry to go

[Kevin Buzzard]

lemma lemma2 {G} [Group G] (S : Subgroup G) [Normal S] :
    toAddSubgroup S = AddMonoidHom.ker (toAdditive (QuotientGroup.mk' S)) := by
  ext g
  exact SetLike.ext_iff.1 (QuotientGroup.ker_mk' S).symm g -- more defeq abuse

So I'm moaning about defeq abuse on the one hand and then using it on the other :-/

[Eric Wieser]

IMO it's totally unreasonable for these stupid isomorphisms to be non-computable, when in lean3 it was "the identity"

[Eric Wieser]

(for those who don't care about computability: this also has a lousy defeq in the reverse direction)

[Eric Wieser]

I'll cleanup my AddOpposite = MulOpposite PR tomorrow, which should optimistically remove all the hacks from this port

[Kevin Buzzard]

Why not go the whole hog and let's go back to AddOpposite X := X?

[Kevin Buzzard]

I guess a strongly related question is "now we can't switch between irreducible and semireducible at will, do we want always irreducible or always semireducible".

[Eric Wieser]

I've restarted !4#3333 at !4#4074 and the port was trivial after !4#4050

[Alex J. Best]

I don't have time to read this thread right now unfortunately so maybe you have all already solved this issue, but I had a go at removing the relevant local attribute in mathlib3 by being a lot more explicit at various equivs in https://github.com/leanprover-community/mathlib/tree/alexjbest/bye-semired feel free to adopt it if its helpful

[Eric Wieser]

My preference would be to merge !4#4050 (which restores the Lean3 behavior we need for this file), and consider a larger refactor post-port