From 51dfc5e678b2d48c1c993a875d7a19030b1d94dd Mon Sep 17 00:00:00 2001 From: Yudai Yamazaki Date: Wed, 7 Aug 2024 11:50:09 +0000 Subject: [PATCH] feat(Subgroup/IsCommutative): add instance for MonoidHom.range (#15370) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds: - `instance Subgroup.commGroup_isCommutative [CommGroup G] (H : Subgroup G) : H.IsCommutative` for subgroups of an abelian group; and - `instance MonoidHom.range_isCommutative [CommGroup G] (f : G →* N) : f.range.IsCommutative`, for the range of a `MonoidHom` whose domain is abelian. It also adds a lemma `Subgroup.mul_comm_of_mem_isCommutative` to allow applying the commutativity without constructing terms of a `Subgroup`. (This lemma is included in this same PR as I mentioned it in the same Zulip thread, but is independent of the two instances above.) Please refer to the [Zulip thread](https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/CommGroup.20MonoidHom.2Erange.20if.20the.20domain.20is.20a.20CommGroup) for discussions. --- Mathlib/Algebra/Group/Subgroup/Basic.lean | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean index 2ca5fe50f09d6..f60917ae388d5 100644 --- a/Mathlib/Algebra/Group/Subgroup/Basic.lean +++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean @@ -1728,6 +1728,11 @@ attribute [class] AddSubgroup.IsCommutative instance IsCommutative.commGroup [h : H.IsCommutative] : CommGroup H := { H.toGroup with mul_comm := h.is_comm.comm } +/-- A subgroup of a commutative group is commutative. -/ +@[to_additive "A subgroup of a commutative group is commutative."] +instance commGroup_isCommutative {G : Type*} [CommGroup G] (H : Subgroup G) : H.IsCommutative := + ⟨CommMagma.to_isCommutative⟩ + @[to_additive] instance map_isCommutative (f : G →* G') [H.IsCommutative] : (H.map f).IsCommutative := ⟨⟨by @@ -1749,6 +1754,11 @@ theorem comap_injective_isCommutative {f : G' →* G} (hf : Injective f) [H.IsCo instance subgroupOf_isCommutative [H.IsCommutative] : (H.subgroupOf K).IsCommutative := H.comap_injective_isCommutative Subtype.coe_injective +@[to_additive] +lemma mul_comm_of_mem_isCommutative [H.IsCommutative] {a b : G} (ha : a ∈ H) (hb : b ∈ H) : + a * b = b * a := by + simpa only [Submonoid.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H) + end Subgroup namespace MulEquiv @@ -1954,6 +1964,11 @@ theorem mem_range {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y := @[to_additive] theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f := by ext; simp +@[to_additive] +instance range_isCommutative {G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) : + f.range.IsCommutative := + range_eq_map f ▸ Subgroup.map_isCommutative ⊤ f + @[to_additive (attr := simp)] theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,