feat(submonoid, subgroup, subring): is_ring_hom instances for set.inclusion

Author: ChrisHughes24

src/group_theory/subgroup.lean

@@ -53,6 +53,12 @@ by subtype_instance
 instance subtype.add_group {s : set β} [is_add_subgroup s] : add_group s :=
 by subtype_instance
 attribute [to_additive subtype.add_group] subtype.group
+attribute [to_additive subtype.add_group._proof_1] subtype.group._proof_1
+attribute [to_additive subtype.add_group._proof_2] subtype.group._proof_2
+attribute [to_additive subtype.add_group._proof_3] subtype.group._proof_3
+attribute [to_additive subtype.add_group._proof_4] subtype.group._proof_4
+attribute [to_additive subtype.add_group._proof_5] subtype.group._proof_5
+attribute [to_additive subtype.add_group.equations._eqn_1] subtype.group.equations._eqn_1
 
 instance subtype.comm_group {α : Type*} [comm_group α] {s : set α} [is_subgroup s] : comm_group s :=
 by subtype_instance
@@ -545,11 +551,42 @@ lemma inj_iff_trivial_ker (f : α → β) [is_group_hom f] :
   function.injective f ↔ ker f = trivial α :=
 ⟨trivial_ker_of_inj f, inj_of_trivial_ker f⟩
 
-instance (s : set α) [is_subgroup s] : is_group_hom (subtype.val : s → α) :=
-⟨λ _ _, rfl⟩
-
 end is_group_hom
 
+instance subtype_val.is_group_hom [group α] {s : set α} [is_subgroup s] :
+  is_group_hom (subtype.val : s → α) := { ..subtype_val.is_monoid_hom }
+
+instance subtype_val.is_add_group_hom [add_group α] {s : set α} [is_add_subgroup s] :
+  is_add_group_hom (subtype.val : s → α) := { ..subtype_val.is_add_monoid_hom }
+attribute [to_additive subtype_val.is_group_hom] subtype_val.is_add_group_hom
+
+instance coe.is_group_hom [group α] {s : set α} [is_subgroup s] :
+  is_group_hom (coe : s → α) := { ..subtype_val.is_monoid_hom }
+
+instance coe.is_add_group_hom [add_group α] {s : set α} [is_add_subgroup s] :
+  is_add_group_hom (coe : s → α) :=
+{ ..subtype_val.is_add_monoid_hom }
+attribute [to_additive coe.is_group_hom] coe.is_add_group_hom
+
+instance subtype_mk.is_group_hom [group α] [group β] {s : set α}
+  [is_subgroup s] (f : β → α) [is_group_hom f] (h : ∀ x, f x ∈ s) :
+  is_group_hom (λ x, (⟨f x, h x⟩ : s)) := { ..subtype_mk.is_monoid_hom f h }
+
+instance subtype_mk.is_add_group_hom [add_group α] [add_group β] {s : set α}
+  [is_add_subgroup s] (f : β → α) [is_add_group_hom f] (h : ∀ x, f x ∈ s) :
+  is_add_group_hom (λ x, (⟨f x, h x⟩ : s)) :=
+{ ..subtype_mk.is_add_monoid_hom f h }
+attribute [to_additive subtype_mk.is_group_hom] subtype_mk.is_add_group_hom
+
+instance set_inclusion.is_group_hom [group α] {s t : set α}
+  [is_subgroup s] [is_subgroup t] (h : s ⊆ t) : is_group_hom (set.inclusion h) :=
+subtype_mk.is_group_hom _ _
+
+instance set_inclusion.is_add_group_hom [add_group α] {s t : set α}
+  [is_add_subgroup s] [is_add_subgroup t] (h : s ⊆ t) : is_add_group_hom (set.inclusion h) :=
+subtype_mk.is_add_group_hom _ _
+attribute [to_additive set_inclusion.is_group_hom] set_inclusion.is_add_group_hom
+
 section simple_group
 
 class simple_group (α : Type*) [group α] : Prop :=

src/group_theory/submonoid.lean

@@ -180,6 +180,25 @@ by induction n; simp [*, pow_succ]
 by induction n; [refl, simp [*, succ_smul]]
 attribute [to_additive is_add_submonoid.smul_coe] is_submonoid.coe_pow
 
+@[to_additive subtype_val.is_add_monoid_hom]
+instance subtype_val.is_monoid_hom [is_submonoid s] : is_monoid_hom (subtype.val : s → α) :=
+{ map_one := rfl, map_mul := λ _ _, rfl }
+
+@[to_additive coe.is_add_monoid_hom]
+instance coe.is_monoid_hom [is_submonoid s] : is_monoid_hom (coe : s → α) :=
+subtype_val.is_monoid_hom
+
+@[to_additive subtype_mk.is_add_monoid_hom]
+instance subtype_mk.is_monoid_hom {γ : Type*} [monoid γ] [is_submonoid s] (f : γ → α)
+  [is_monoid_hom f] (h : ∀ x, f x ∈ s) : is_monoid_hom (λ x, (⟨f x, h x⟩ : s)) :=
+{ map_one := subtype.eq (is_monoid_hom.map_one f),
+  map_mul := λ _ _, subtype.eq (is_monoid_hom.map_mul f) }
+
+@[to_additive set_inclusion.is_add_monoid_hom]
+instance set_inclusion.is_monoid_hom (t : set α) [is_submonoid s] [is_submonoid t] (h : s ⊆ t) :
+  is_monoid_hom (set.inclusion h) :=
+subtype_mk.is_monoid_hom _ _
+
 namespace monoid
 
 inductive in_closure (s : set α) : α → Prop

src/ring_theory/subring.lean

@@ -37,6 +37,21 @@ instance is_subring_set_range {R : Type u} {S : Type v} [ring R] [ring S]
 
 end is_ring_hom
 
+instance subtype_val.is_ring_hom {s : set R} [is_subring s] :
+  is_ring_hom (subtype.val : s → R) :=
+{ ..subtype_val.is_add_group_hom, ..subtype_val.is_monoid_hom }
+
+instance coe.is_ring_hom {s : set R} [is_subring s] : is_ring_hom (coe : s → R) :=
+subtype_val.is_ring_hom
+
+instance subtype_mk.is_ring_hom {γ : Type*} [ring γ] {s : set R} [is_subring s] (f : γ → R)
+  [is_ring_hom f] (h : ∀ x, f x ∈ s) : is_ring_hom (λ x, (⟨f x, h x⟩ : s)) :=
+{ ..subtype_mk.is_add_group_hom f h, ..subtype_mk.is_monoid_hom f h }
+
+instance set_inclusion.is_ring_hom {s t : set R} [is_subring s] [is_subring t] (h : s ⊆ t) :
+  is_ring_hom (set.inclusion h) :=
+subtype_mk.is_ring_hom _ _
+
 variables {cR : Type u} [comm_ring cR]
 
 instance subset.comm_ring {S : set cR} [is_subring S] : comm_ring S :=