CommGroup MonoidHom.range if the domain is a CommGroup

Stream: Is there code for X?

[Yudai Yamazaki]

Do we already have this?

import Mathlib.Algebra.Group.Subgroup.Basic

variable {M N : Type*} [CommGroup M] [Group N] {f : M →* N}

-- failed to synthesize
-- #synth CommGroup f.range

theorem MonoidHom.mul_comm_of_mem_range {n₁ n₂ : N} (h₁ : n₁ ∈ f.range) (h₂ : n₂ ∈ f.range) :
    n₁ * n₂ = n₂ * n₁ := by
  obtain ⟨m₁, rfl⟩ := h₁
  obtain ⟨m₂, rfl⟩ := h₂
  rw [← map_mul, mul_comm, map_mul]

instance : CommGroup f.range where
  mul_comm := by
    intro ⟨_, h₁⟩ ⟨_, h₂⟩
    simp only [Submonoid.mk_mul_mk, Subtype.mk.injEq]
    exact MonoidHom.mul_comm_of_mem_range h₁ h₂

[Edward van de Meent]

i imagine Subgroup.IsCommutative.commGroup would be involved...

[Edward van de Meent]

i suppose the missing instance is the variant of Subgroup.map_isCommutative with range rather than map...

[Yudai Yamazaki]

Thank you for the suggestions.

Subgroup.map_isCommutative almost works, but yes, IsCommutative instances for subgroups of CommGroup are missing.

import Mathlib.Algebra.Group.Subgroup.Basic

variable {M N : Type*} [CommGroup M] [Group N] {f : M →* N}

-- failed to synthesize
-- #synth (⊤ : Subgroup M).IsCommutative
instance (H : Subgroup M) : H.IsCommutative where
  is_comm := CommMagma.to_isCommutative

instance : f.range.IsCommutative := MonoidHom.range_eq_map f ▸ Subgroup.map_isCommutative ⊤ f
#synth CommGroup f.range

theorem MonoidHom.mul_comm_of_mem_range {n₁ n₂ : N} (h₁ : n₁ ∈ f.range) (h₂ : n₂ ∈ f.range) :
    n₁ * n₂ = n₂ * n₁ := by
  have := mul_comm (⟨n₁, h₁⟩ : f.range) ⟨n₂, h₂⟩
  simp only [Submonoid.mk_mul_mk, Subtype.mk.injEq] at this
  exact this

[Yudai Yamazaki]

Would it be worth to be a part of the Mathlib? I will be happy to make a PR if so, as I need the theorem for my project.

[Ruben Van de Velde]

Yeah, probably worth adding

[Yudai Yamazaki]

I have opened a PR: leanprover-community/mathlib4#15370. I would appreciate your comments.