feat(group_theory/subgroup/basic): Map a subgroup under an iso (#17775)

YaelDillies · YaelDillies · commit cf8e77c63631 · 2023-01-13T10:23:39.000Z
Cross-reference `mul_equiv.subgroup_map` and `subgroup.equiv_map_of_injective`. Add lemmas connecting them.
diff --git a/src/group_theory/commensurable.lean b/src/group_theory/commensurable.lean
@@ -52,10 +52,10 @@ lemma equivalence : equivalence (@commensurable G _) :=
 /--Equivalence of `K/H ⊓ K` with `gKg⁻¹/gHg⁻¹ ⊓ gKg⁻¹`-/
 def  quot_conj_equiv (H K : subgroup G) (g : conj_act G) :
   K ⧸ (H.subgroup_of K) ≃ (g • K).1 ⧸ ((g • H).subgroup_of (g • K)) :=
-quotient.congr (K.equiv_smul g).to_equiv (λ a b, by { rw [←quotient.eq', ←quotient.eq',
+quotient.congr (K.equiv_smul g).to_equiv (λ a b, by { dsimp, rw [←quotient.eq', ←quotient.eq',
   quotient_group.eq', quotient_group.eq', subgroup.mem_subgroup_of, subgroup.mem_subgroup_of,
-  mul_equiv.to_equiv_eq_coe, mul_equiv.coe_to_equiv, ←mul_equiv.map_inv, ←mul_equiv.map_mul,
-  subgroup.equiv_smul_apply_coe, subgroup.smul_mem_pointwise_smul_iff] })
+  ←mul_equiv.map_inv, ←mul_equiv.map_mul, subgroup.equiv_smul_apply_coe],
+  exact subgroup.smul_mem_pointwise_smul_iff.symm })
 
 lemma commensurable_conj {H K : subgroup G} (g : conj_act G) :
    commensurable H K ↔ commensurable (g • H) (g • K) :=
diff --git a/src/group_theory/subgroup/basic.lean b/src/group_theory/subgroup/basic.lean
@@ -87,9 +87,10 @@ membership of a subgroup's underlying set.
 subgroup, subgroups
 -/
 
+open function
 open_locale big_operators
 
-variables {G : Type*} [group G]
+variables {G G' : Type*} [group G] [group G']
 variables {A : Type*} [add_group A]
 
 section subgroup_class
@@ -1781,16 +1782,16 @@ instance is_commutative.comm_group [h : H.is_commutative] : comm_group H :=
 instance center.is_commutative : (center G).is_commutative :=
 ⟨⟨λ a b, subtype.ext (b.2 a)⟩⟩
 
-@[to_additive] instance map_is_commutative {G' : Type*} [group G'] (f : G →* G')
-  [H.is_commutative] : (H.map f).is_commutative :=
+@[to_additive] instance map_is_commutative (f : G →* G') [H.is_commutative] :
+  (H.map f).is_commutative :=
 ⟨⟨begin
   rintros ⟨-, a, ha, rfl⟩ ⟨-, b, hb, rfl⟩,
   rw [subtype.ext_iff, coe_mul, coe_mul, subtype.coe_mk, subtype.coe_mk, ←map_mul, ←map_mul],
   exact congr_arg f (subtype.ext_iff.mp (mul_comm ⟨a, ha⟩ ⟨b, hb⟩)),
 end⟩⟩
 
-@[to_additive] lemma comap_injective_is_commutative {G' : Type*} [group G'] {f : G' →* G}
-  (hf : function.injective f) [H.is_commutative] : (H.comap f).is_commutative :=
+@[to_additive] lemma comap_injective_is_commutative {f : G' →* G} (hf : injective f)
+  [H.is_commutative] : (H.comap f).is_commutative :=
 ⟨⟨λ a b, subtype.ext begin
   have := mul_comm (⟨f a, a.2⟩ : H) (⟨f b, b.2⟩ : H),
   rwa [subtype.ext_iff, coe_mul, coe_mul, coe_mk, coe_mk, ←map_mul, ←map_mul, hf.eq_iff] at this,
@@ -2405,8 +2406,10 @@ comap_sup_eq_of_le_range L.subtype (hH.trans L.subtype_range.ge) (hK.trans L.sub
   codisjoint (H.subgroup_of (H ⊔ K)) (K.subgroup_of (H ⊔ K)) :=
 by { rw [codisjoint_iff, sup_subgroup_of_eq, subgroup_of_self], exacts [le_sup_left, le_sup_right] }
 
-/-- A subgroup is isomorphic to its image under an injective function -/
-@[to_additive  "An additive subgroup is isomorphic to its image under an injective function"]
+/-- A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
+use `mul_equiv.subgroup_map` for better definitional equalities. -/
+@[to_additive  "An additive subgroup is isomorphic to its image under an injective function. If you
+have an isomorphism, use `add_equiv.add_subgroup_map` for better definitional equalities."]
 noncomputable def equiv_map_of_injective (H : subgroup G)
   (f : G →* N) (hf : function.injective f) : H ≃* H.map f :=
 { map_mul' := λ _ _, subtype.ext (f.map_mul _ _), ..equiv.set.image f H hf }
@@ -2764,8 +2767,6 @@ end subgroup
 
 namespace monoid_hom
 
-variables {G' : Type*} [group G']
-
 /-- The `monoid_hom` from the preimage of a subgroup to itself. -/
 @[to_additive "the `add_monoid_hom` from the preimage of an additive subgroup to itself.", simps]
 def subgroup_comap (f : G →* G') (H' : subgroup G') : H'.comap f →* H' :=
@@ -2784,7 +2785,6 @@ f.submonoid_map_surjective H.to_submonoid
 end monoid_hom
 
 namespace mul_equiv
-
 variables {H K : subgroup G}
 
 /-- Makes the identity isomorphism from a proof two subgroups of a multiplicative
@@ -2794,20 +2794,30 @@ two subgroups of an additive group are equal."]
 def subgroup_congr (h : H = K) : H ≃* K :=
 { map_mul' :=  λ _ _, rfl, ..equiv.set_congr $ congr_arg _ h }
 
-/-- A `mul_equiv` `φ` between two groups `G` and `G'` induces a `mul_equiv` between
-a subgroup `H ≤ G` and the subgroup `φ(H) ≤ G'`. -/
-@[to_additive "An `add_equiv` `φ` between two additive groups `G` and `G'` induces an `add_equiv`
-between a subgroup `H ≤ G` and the subgroup `φ(H) ≤ G'`. "]
-def subgroup_map {G'} [group G'] (e : G ≃* G') (H : subgroup G) :
-  H ≃* H.map e.to_monoid_hom :=
-e.submonoid_map H.to_submonoid
+/-- A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
+use `subgroup.equiv_map_of_injective`. -/
+@[to_additive  "An additive subgroup is isomorphic to its image under an an isomorphism. If you only
+have an injective map, use `add_subgroup.equiv_map_of_injective`."]
+def subgroup_map (e : G ≃* G') (H : subgroup G) : H ≃* H.map (e : G →* G') :=
+mul_equiv.submonoid_map (e : G ≃* G') H.to_submonoid
 
-end mul_equiv
+@[simp, to_additive]
+lemma coe_subgroup_map_apply (e : G ≃* G') (H : subgroup G) (g : H) :
+  ((subgroup_map e H g : H.map (e : G →* G')) : G') = e g := rfl
+
+@[simp, to_additive]
+lemma subgroup_map_symm_apply (e : G ≃* G') (H : subgroup G) (g : H.map (e : G →* G')) :
+  (e.subgroup_map H).symm g = ⟨e.symm g, set_like.mem_coe.1 $ set.mem_image_equiv.1 g.2⟩ := rfl
 
--- TODO : ↥(⊤ : subgroup H) ≃* H ?
+end mul_equiv
 
 namespace subgroup
 
+@[simp, to_additive]
+lemma equiv_map_of_injective_coe_mul_equiv (H : subgroup G) (e : G ≃* G') :
+  H.equiv_map_of_injective (e : G →* G') (equiv_like.injective e) = e.subgroup_map H :=
+by { ext, refl }
+
 variables {C : Type*} [comm_group C] {s t : subgroup C} {x : C}
 
 @[to_additive]
diff --git a/src/group_theory/submonoid/operations.lean b/src/group_theory/submonoid/operations.lean
@@ -605,8 +605,10 @@ def top_equiv : (⊤ : submonoid M) ≃* M :=
   (top_equiv : _ ≃* M).to_monoid_hom = (⊤ : submonoid M).subtype :=
 rfl
 
-/-- A submonoid is isomorphic to its image under an injective function -/
-@[to_additive "An additive submonoid is isomorphic to its image under an injective function"]
+/-- A subgroup is isomorphic to its image under an injective function. If you have an isomorphism,
+use `mul_equiv.submonoid_map` for better definitional equalities. -/
+@[to_additive  "An additive subgroup is isomorphic to its image under an injective function. If you
+have an isomorphism, use `add_equiv.add_submonoid_map` for better definitional equalities."]
 noncomputable def equiv_map_of_injective
   (f : M →* N) (hf : function.injective f) : S ≃* S.map f :=
 { map_mul' := λ _ _, subtype.ext (f.map_mul _ _), ..equiv.set.image f S hf }
@@ -1055,15 +1057,25 @@ a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`.
 See `monoid_hom.submonoid_map` for a variant for `monoid_hom`s. -/
 @[to_additive "An `add_equiv` `φ` between two additive monoids `M` and `N` induces an `add_equiv`
 between a submonoid `S ≤ M` and the submonoid `φ(S) ≤ N`. See `add_monoid_hom.add_submonoid_map`
-for a variant for `add_monoid_hom`s.", simps]
+for a variant for `add_monoid_hom`s."]
 def submonoid_map (e : M ≃* N) (S : submonoid M) : S ≃* S.map e.to_monoid_hom :=
-{ to_fun := λ x, ⟨e x, _⟩,
-  inv_fun := λ x, ⟨e.symm x, _⟩, -- we restate this for `simps` to avoid `⇑e.symm.to_equiv x`
-  ..e.to_monoid_hom.submonoid_map S,
-  ..e.to_equiv.image S }
+{ map_mul' := λ _ _, subtype.ext (map_mul e _ _), ..(e : M ≃ N).image S }
+
+@[simp, to_additive]
+lemma coe_submonoid_map_apply (e : M ≃* N) (S : submonoid M) (g : S) :
+  ((submonoid_map e S g : S.map (e : M →* N)) : N) = e g := rfl
+
+@[simp, to_additive add_equiv.add_submonoid_map_symm_apply]
+lemma submonoid_map_symm_apply (e : M ≃* N) (S : submonoid M) (g : S.map (e : M →* N)) :
+  (e.submonoid_map S).symm g = ⟨e.symm g, set_like.mem_coe.1 $ set.mem_image_equiv.1 g.2⟩ := rfl
 
 end mul_equiv
 
+@[simp, to_additive]
+lemma submonoid.equiv_map_of_injective_coe_mul_equiv (e : M ≃* N) :
+  S.equiv_map_of_injective (e : M →* N) (equiv_like.injective e) = e.submonoid_map S :=
+by { ext, refl }
+
 section actions
 /-! ### Actions by `submonoid`s
 
