Subgroup.closure_toAddSubgroup

Stream: mathlib4

[Xavier Roblot]

Somehow, I have the feeling that the proof below is not optimal. I seem to have trouble finding the best way to deal with Additive and Multiplicative. If anyone could improve on it, I would be grateful. Also, is there a way to deduce easily the proof of the Additive version from the Multiplicative version?

import Mathlib.Algebra.Group.Subgroup.Lattice

theorem Subgroup.closure_toAddSubgroup {G : Type*} [Group G] (s : Set G) :
    (Subgroup.closure s).toAddSubgroup = AddSubgroup.closure (Additive.ofMul '' s) := by
  rw [OrderIso.apply_eq_iff_eq_symm_apply, AddSubgroup.closure,
    OrderIso.map_sInf_eq_sInf_symm_preimage, OrderIso.symm_symm]
  simp_rw [Set.preimage_setOf_eq, coe_toAddSubgroup_apply, Set.preimage_equiv_eq_image_symm,
    Additive.toMul_symm_eq, Set.image_subset_iff, Equiv.preimage_image, closure]

theorem _AddSubgroup.closure_toSubgroup {G : Type*} [AddGroup G] (s : Set G) :
    (AddSubgroup.closure s).toSubgroup = Subgroup.closure (Multiplicative.ofAdd '' s) := by
  sorry

[María Inés de Frutos Fernández]

This is not exactly what you are asking for, but in case it is helpful, I wrote some similar theorems a while ago:

theorem AddSubgroup.toSubgroup_closure {A : Type} [AddGroup A] (S : Set A) :
    (AddSubgroup.closure S).toSubgroup  =
      Subgroup.closure (Multiplicative.toAdd ⁻¹' S) :=
  le_antisymm
    (AddSubgroup.toSubgroup.to_galoisConnection.l_le <|
      (AddSubgroup.closure_le _).2 <| Subgroup.subset_closure (G := Multiplicative A))
    ((Subgroup.closure_le _).2 <| AddSubgroup.subset_closure (G := A))

theorem Subgroup.toAddSubgroup_closure {G : Type} [Group G] (S : Set G) :
    (Subgroup.closure S).toAddSubgroup =
      AddSubgroup.closure (Additive.toMul ⁻¹' S) :=
  le_antisymm
    (Subgroup.toAddSubgroup.le_symm_apply.1 <|
      (Subgroup.closure_le _).2 (AddSubgroup.subset_closure (G := Additive G)))
    ((AddSubgroup.closure_le _).2 (Subgroup.subset_closure (G := G)))

[Xavier Roblot]

Thanks. It is quite close and I guess your proof is somewhat cleaner. In any case, it is interesting to see that you reproved the second version and were not able to use the first proof to deduce the second one.

[Eric Wieser]

Here's the second one in terms of the first:

theorem Subgroup.toAddSubgroup_closure {G : Type} [Group G] (S : Set G) :
    (Subgroup.closure S).toAddSubgroup =
      AddSubgroup.closure (Additive.toMul ⁻¹' S) :=
  AddSubgroup.toSubgroup.injective <| Eq.symm <| AddSubgroup.toSubgroup_closure _

[Xavier Roblot]

Thanks. Can I use that (with due credit) in a coming PR?

[Eric Wieser]

Yes, though I think you can shrink it further by using something from the Equiv API

[Xavier Roblot]

I have another question though. What is the best spelling for this result:

theorem AddSubgroup.closure_toSubgroup {A : Type*} [AddGroup A] (S : Set A) :
    (AddSubgroup.closure S).toSubgroup  =
      Subgroup.closure (Multiplicative.ofAdd '' S) :=

or

theorem AddSubgroup.closure_toSubgroup {A : Type} [AddGroup A] (S : Set A) :
    (AddSubgroup.closure S).toSubgroup  =
      Subgroup.closure (Multiplicative.toAdd ⁻¹' S) :=

That is: Multiplicative.ofAdd '' S or Multiplicative.toAdd ⁻¹' S?

[Eric Wieser]

I think the preimage is preferred

[Xavier Roblot]

Ok. thanks

[Xavier Roblot]

#23171

[Kevin Buzzard]

Preimage has better defeqs because there's not a random "exists" in the middle