avoiding HEq

Stream: mathlib4

[Antoine Chambert-Loir]

In #24039, I define the equivalence of stabilizers in an orbit, refining docs#MulAction.stabilizerEquivStabilizerOfOrbitRel

My definition takes the form :

stabilizerEquivStabilizer {a b : α} {g : G} (hg : g • b = a) : stabilizer G b ≃* stabilizer G a := …

A suggestion of @Bhavik Mehta was to make a := g • b there, but then I can't manage to the prove the transitivity property. And since it follows from the refl property, it is really the latter that I can't prove.

Here is a MWE. I'd like to get advices about the most practical framing.

import Mathlib.GroupTheory.GroupAction.Basic

open MulAction

variable {G : Type*} [Group G] {α : Type*} [MulAction G α]

variable (h g : G) (a : α)

def sEs : stabilizer G a ≃* stabilizer G (g • a) :=
    ((MulAut.conj g).subgroupMap <| stabilizer G a).trans
    (MulEquiv.subgroupCongr (by simp [stabilizer_smul_eq_stabilizer_map_conj]))

def sEs_apply (x : stabilizer G a) :
    (sEs g a x : G) = MulAut.conj g x := by
  simp [sEs]

theorem sEs_refl (b : α) (H : g • a = b) :  -- reflexivity
    HEq (H ▸ sEs g a) (sEs g a) := by
  sorry

theorem sEs_refl_apply (b : α) (H : g • a = b) (x : stabilizer G a) :  -- reflexivity
    (H ▸ sEs g a) x = H ▸ (sEs g a) x := by
  sorry

theorem sEs_trans (h g : G) (a : α) :  -- transitivity
    mul_smul h g a ▸ sEs (h * g) a = (sEs g a).trans (sEs h (g • a)) := by
  ext x
  set t := mul_smul h g a
  conv_rhs =>
    simp [sEs, ← mul_assoc]
    rw [mul_assoc _ g⁻¹, ← mul_inv_rev, ← MulAut.conj_apply, ← sEs_apply]
  congr 1
  · rw [t]
  · simp [sEs_refl_apply]

[Kevin Buzzard]

I like your definition better than Bhavik's: it's more general. There is a bunch of (v : HeightOneSpectrum A) (w : HeightOneSpectrum B) (h : v = comap w) theorems in FLT for the same reason.

[Antoine Chambert-Loir]

I agree. Also, it's closer to the idea that an action of a group on a set gives (“is” ?) a groupoid, with objects that set and arrows given by the members of the group.
In any case, I believe there is a lesson in equality to get by proving the above MWE.

[Eric Wieser]

I think the lesson here is that if you do follow Bhavik's strategy, you should use a better casting function than the "stupid triangle"

[Eric Wieser]

The sorries can be proved with cases H; rfl I think

[Antoine Chambert-Loir]

I tried with docs#cast, but wasn't more successful either.

[Kevin Buzzard]

I only called it the "stupid triangle" in Lean 3 when it was far more stupid. Now I have some respect for it!

[Antoine Chambert-Loir]

Eric Wieser said:

The sorries can be proved with cases H; rfl I think

That looks pretty much like the “induction on equality” that people do in HoTT.

[Kevin Buzzard]

It is literally Lean's induction on equality.

[Antoine Chambert-Loir]

But now that both versions compile, I'm left into deciding which version is best for mathlib (and me).

[Kevin Buzzard]

My vote would be yours because yours is more general (it applies when the proof of the equality is not rfl). Does your version have any HEqs in? Avoiding HEq would be another reason to vote for yours.

[Eric Wieser]

Antoine Chambert-Loir said:

I tried with docs#cast, but wasn't more successful either.

I mean a dedicated "stabilizers at equal elements are isomorphic as monoids" def

[Eric Wieser]

Maybe a generic "equal submonoids are isomorphic" result, which I think exists, is sufficient

[Antoine Chambert-Loir]

Do you mean other than docs#MulAction.stabilizer_smul_eq_stabilizer_map_conj ?

[Eric Wieser]

I mean

import Mathlib.GroupTheory.GroupAction.Basic

open MulAction

variable {G : Type*} [Group G] {α : Type*} [MulAction G α]
variable (h g : G) (a : α)

def sEs : stabilizer G a ≃* stabilizer G (g • a) :=
    ((MulAut.conj g).subgroupMap <| stabilizer G a).trans
    (MulEquiv.subgroupCongr (by simp [stabilizer_smul_eq_stabilizer_map_conj]))

theorem sEs_trans (h g : G) (a : α) :
    sEs (h * g) a = (sEs g a |>.trans <| sEs h (g • a)).trans (MulEquiv.subgroupCongr (by rw [mul_smul])) := by
  ext x
  simp [sEs]

[Eric Wieser]

Your proposed version is just Bhavik's where you've composed with MulEquiv.subgroupCongr inside your definition

[Eric Wieser]

It's not clear to me why the hg : g • b = a version is better; it means the caller has to juggle the proof arguments in their theorems statements even if they don't intend to do any casting

[Antoine Chambert-Loir]

“that” is Bhavik's proposition? It looks simpler at first hand, indeed. But one doesn't want to have to summon Eric at any basic proof in the theory of group actions.

[Eric Wieser]

Edited above.

[Eric Wieser]

I'd argue you summoned me for the statement, not the proof :)

[Antoine Chambert-Loir]

OK, so I have two experts of distinct opinions here. I'll try with the other one to see whether it is more equally practical in my applications.

[Eric Wieser]

What does the statement of trans look like with your spelling?

[Antoine Chambert-Loir]

theorem stabilizerEquivStabilizer_trans {hg : g • b = a} {hh : h • c = b} :
    (stabilizerEquivStabilizer hh).trans (stabilizerEquivStabilizer hg)
      = (stabilizerEquivStabilizer (by rw [← hg, ←hh, ← smul_smul])) := by
  ext x; simp [stabilizerEquivStabilizer_apply]

[Antoine Chambert-Loir]

(This is after I removed additional hypothesis hk : k • c = a, for k : G.)

[Eric Wieser]

This one creates annoying side goals if you rewrite it backwards; I think both versions need a separate lemma for each direction.

[Eric Wieser]

For Bhavik's, that's

theorem sEs_trans' (h g : G) (a : α) :
    (sEs g a |>.trans <| sEs h (g • a)) = (sEs (h * g) a).trans (MulEquiv.subgroupCongr (by rw [mul_smul])) := by
  ext x
  simp [sEs]

[Bhavik Mehta]

Kevin Buzzard said:

My vote would be yours because yours is more general (it applies when the proof of the equality is not rfl). Does your version have any HEqs in? Avoiding HEq would be another reason to vote for yours.

The distinction is that in mine, the basic version insists that the elements are of the same form, but combined with a docs#MulEquiv.subgroupCongr, you don't lose any generality. And then we have separation between the two ideas "stabilising by something in the orbit is equivalent" and "stabilising by the same element is equivalent", where the latter already exists in mathlib

[Antoine Chambert-Loir]

These definitions were made for #24039, and losing the flexibility of specifying both points and the group elements leads into nightmares I prefer to avoid.

[Eric Wieser]

I don't follow; are you saying that in its current form, that PR is/causes a nightmare? Or that the hk : k • c = a version would be a nightmare?

[Antoine Chambert-Loir]

Using the simple version (with an explicit g • a instead of b, and an equality) seems complicated.
The goal is to use these group isomorphism to equivariant maps of group actions.

[Eric Wieser]

Is the complication present in #24039 already (and if so can you point to where you think it is worst), or are you saying that downstream results become complicated?

[Antoine Chambert-Loir]

No, everything worked well in #24039. It is when trying to apply your suggestion that it became more complicated.

[Eric Wieser]

What is "my suggestion" and "it", if not respectively what #24039 already does, and the theorems within it?

[Antoine Chambert-Loir]

"your suggestion" is to define stabilizerEquivStabilizer as

def stabilizerEquivStabilizer : stabilizer G a ≃* stabilizer G (g • a) := …

In #23962#24039, these group morphisms are used to define equivariant maps between group actions, namely the action of stabilizer G a on the complement of {a} (a docs#SubMulAction named ofStabilizer G a there) and the like for g • a.
This equivariant map has to be proved bijective, which it is, trivially, and for whatever reason,
this is more difficult to formalize with the above definition.

[Eric Wieser]

Are you talking about #23962, which is where ofStabilizer is defined?

[Antoine Chambert-Loir]

Sorry, yes.

[Eric Wieser]

This equivariant map has to be proved bijective,

What's the theorem name of this result?

[Antoine Chambert-Loir]

SubMulAction.ofStabilizer.conjMap_bijective