Sugroup sup

Stream: Is there code for X?

[Patrick Massot]

Are we really missing the following lemma??

example {G : Type*} [Group G] (H H' : Subgroup G) :
    ((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G))

There is docs#Subgroup.iSup_eq_closure which is the version for any indexed family of subgroups and a completely crazy docs#Subgroup.sup_eq_closure but I can't find the above.

[Eric Wieser]

docs#Subgroup.closure_union is where I'd expect it

[Patrick Massot]

I opened #7468 in case nobody can find it.

[Patrick Massot]

Eric, this is very much related but not the same.

[Patrick Massot]

See https://github.com/leanprover-community/mathlib4/pull/7468/files#diff-3ea21bd11ed765ebb85bf53c26a6b0ced8171afca566b2b1aaf9b685dbe2e421R3543 to see my statement in action.

[Eric Wieser]

Looking at your PR, I see that you use precisely the two results I was going to say we already have

[Eric Wieser]

I think this omission is consistent across all the subobjects

[Eric Wieser]

(and that its omission is a semi-deliberate "this is just two lemmas together" thing)

[Eric Wieser]

Perhaps a good indication that this is a bad lemma is that it doesn't help for H ⊔ H' ⊔ H''

[Patrick Massot]

To be honest, my actual use if for teaching Lean only. I literally want to be able to say: I know H \sqcap H' looks silly but the fact that the underlying set is H \cap H' is kind of random, it contrasts with

example {G : Type*} [Group G] (H H' : Subgroup G) :
    ((H ⊔ H' : Subgroup G) : Set G) = Subgroup.closure ((H : Set G) ∪ (H' : Set G)) :=  sup_eq_closure H H'

[Patrick Massot]

and I also I won't admit how much time I wasted coming up with the proof, but it was way too much time.

[Patrick Massot]

And the current situation is really inconsistent with docs#Subgroup.iSup_eq_closure

[Eric Wieser]

It looks like there's a clash in your PR with existing lemmas that use H * H' instead of H ∪ H'

[Patrick Massot]

Oh yes, I even mentioned it in my first post above...

[Patrick Massot]

I tried a blind fix. We'll see what CI thinks.

[Eric Wieser]

Is it mathematically crazy in your opinion, or just crazy in the context of the result you were hoping to find?

[Patrick Massot]

It is mathematically weird because it is more complicated than the union version for no apparent benefit (the multiplication is larger than the union so it's a less good generating set). Note there is a meaningful and relevant very related result in the commutative case: docs#Subgroup.mem_sup. I guess the "crazy" version exists only in relation to this.

[Patrick Massot]

Anyway, there is currently a marching band playing on campus next to my office, and I interpret this as a subtle clue that it may be getting late and I should leave my office and go back home.

[Antoine Chambert-Loir]

Patrick Massot said:

It is mathematically weird because it is more complicated than the union version for no apparent benefit (the multiplication is larger than the union so it's a less good generating set). Note there is a meaningful and relevant very related result in the commutative case: docs#Subgroup.mem_sup. I guess the "crazy" version exists only in relation to this.

The “correct” multiplicative result could be that H ⊔ H' = H * H' when one of them normalizes the other one, at least when one of them is normal.