Orbit of trivial subgroup

Stream: new members

[Laurent Bartholdi]

Sorry, me again... I would like to prove that the trivial subgroup has singleton orbits, and tried

@[simp] lemma orbit_bot (p : α) : mul_action.orbit (⊥ : subgroup G) p = {p} := begin
  ext1,
  rw mul_action.mem_orbit_iff,
  split,
  { intro h, cases h with g g_to_x,
    rw [← g_to_x,set.mem_singleton_iff],
    cases g with _ g_bot,
    have g_one := subgroup.mem_bot.mp g_bot,
    sorry },
  { intro h,  exact ⟨1,eq.trans (one_smul _ p) (set.mem_singleton_iff.mp h).symm⟩ }
end

but I'm stuck: I have an element g : ↥⊥ and would like to conclude g=1, but the only thing I can do is cases g which gives me g_val = 1. Any suggestion? I feel I'm screwing up with the different coercions...

[Yaël Dillies]

When you do cases g, g is not in your context anymore, right? It's been replaced by \<g_val, some_proof_term\> so g_val = 1 is what you want.

[Laurent Bartholdi]

@Yaël Dillies Yes, exactly! I get g_one : g_val = 1 but my goal is still ⟨g_val, g_bot⟩ • p = p, and I can't rewrite g_one in it to invoke one_smul

[Yaël Dillies]

What does simp do on the goal?

[Laurent Bartholdi]

nothing :(, just says it can't simplify

[Yaël Dillies]

Hmm, that's unfortunate. Can you add the lemma

@[simp, to_additive] lemma subgroup.mk_smul {G α : Type*} [group G] [mul_action G α]
  {S : subgroup G} {g : G} (hg : g ∈ S) (a : α) : (⟨g, hg⟩ : S) • a = g • a := rfl

and try again?

[Laurent Bartholdi]

You're a goddess!

[Yaël Dillies]

No, i just come with a brain-inbuilt Lean compiler :grinning:

[Laurent Bartholdi]

Is this something that should be part of the main library?

[Yaël Dillies]

Definitely. It not being in mathlib is an oversight.

[Eric Wieser]

docs#subgroup.smul_def

[Eric Wieser]

I think the lemma Yaël suggests above is not consistent with how we usually do subobject APIs

[Eric Wieser]

I recommend you instead prove

@[simp] lemma orbit_bot [subsingleton G] (p : α) : mul_action.orbit G p = {p} := begin
  ext1,
  rw mul_action.mem_orbit_iff,
  sorry
end

Which is more general than your statement

[Yaël Dillies]

Eric, are you claiming subgroup.mk_smul is a bad simp lemma? Why?

[Yaël Dillies]

If subgroup.smul_def were simp, I would understand, but it's not (and shouldn't be).

[Eric Wieser]

Yaël Dillies said:

Eric, are you claiming subgroup.mk_smul is a bad simp lemma? Why?

Yes, to be consistent with the fact we don't have .mk_zero or .neg_mk or .mk_add_mk or ...

[Eric Wieser]

Also the subtype.mk term it uses isn't very well typed (there's no subgroup.subtype_mk); though lean 4 resolves that

[Yaël Dillies]

docs#add_mem_class.mk_add_mk :thinking:

[Yaël Dillies]

Regardless of whether the lemmas you claim are missing, missing simp lemmas is not an argument against adding them!

[Eric Wieser]

Missing families of simp lemmas are evidence that the simp set has not been constructed with those lemmas in mind, and introducing them without further analysis might make things less confluent

[Eric Wieser]

But yes, given those exist I think the lemma you suggest is sensible after all

[Eric Wieser]

I would guess you need to repeat it for every subobject? I don't think we generalized the smul instances to use mul_mem_class, though we certainly could after the port

[Yaël Dillies]

Yes, I suspect it will have to be subobject-specific for the time being.