From bd524fc19fd739d16c3b414988a12ecd3346a98b Mon Sep 17 00:00:00 2001
From: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Date: Sun, 7 Apr 2019 10:29:26 +0100
Subject: [PATCH] feat(field_theory/subfield): is_subfield instances (#891)

---
 src/field_theory/subfield.lean  | 20 ++++++++++++++++++++
 src/group_theory/submonoid.lean | 21 +++++++++++++++++++++
 src/ring_theory/subring.lean    | 13 +++++++------
 3 files changed, 48 insertions(+), 6 deletions(-)

diff --git a/src/field_theory/subfield.lean b/src/field_theory/subfield.lean
index 8755f1c15fefa..0cc98988c5ce3 100644
--- a/src/field_theory/subfield.lean
+++ b/src/field_theory/subfield.lean
@@ -11,6 +11,26 @@ variables {F : Type*} [field F] (S : set F)
 class is_subfield extends is_subring S : Prop :=
 (inv_mem : ∀ {x : F}, x ≠ 0 → x ∈ S → x⁻¹ ∈ S)
 
+instance univ.is_subfield : is_subfield (@set.univ F) :=
+{ inv_mem := by intros; trivial }
+
+instance preimage.is_subfield {K : Type*} [field K]
+  (f : F → K) [is_ring_hom f] (s : set K) [is_subfield s] : is_subfield (f ⁻¹' s) :=
+{ inv_mem := λ a ha0 (ha : f a ∈ s), show f a⁻¹ ∈ s,
+    by rw [is_field_hom.map_inv' f ha0];
+      exact is_subfield.inv_mem ((is_field_hom.map_ne_zero f).2 ha0) ha }
+
+instance image.is_subfield {K : Type*} [field K]
+  (f : F → K) [is_ring_hom f] (s : set F) [is_subfield s] : is_subfield (f '' s) :=
+{ inv_mem := λ a ha0 ⟨x, hx⟩,
+    have hx0 : x ≠ 0, from λ hx0, ha0 (hx.2 ▸ hx0.symm ▸ is_ring_hom.map_zero f),
+    ⟨x⁻¹, is_subfield.inv_mem hx0 hx.1,
+    by rw [← hx.2, is_field_hom.map_inv' f hx0]; refl⟩ }
+
+instance range.is_subfield {K : Type*} [field K]
+  (f : F → K) [is_ring_hom f] : is_subfield (set.range f) :=
+by rw ← set.image_univ; apply_instance
+
 namespace field
 
 def closure : set F :=
diff --git a/src/group_theory/submonoid.lean b/src/group_theory/submonoid.lean
index 3e180374c873a..bacee09896e9d 100644
--- a/src/group_theory/submonoid.lean
+++ b/src/group_theory/submonoid.lean
@@ -65,6 +65,27 @@ instance multiples.is_add_submonoid (x : β) : is_add_submonoid (multiples x) :=
 multiplicative.is_submonoid_iff.1 $ powers.is_submonoid _
 attribute [to_additive multiples.is_add_submonoid] powers.is_submonoid
 
+@[to_additive univ.is_add_submonoid]
+instance univ.is_submonoid : is_submonoid (@set.univ α) := by split; simp
+
+@[to_additive preimage.is_add_submonoid]
+instance preimage.is_submonoid {γ : Type*} [monoid γ] (f : α → γ) [is_monoid_hom f]
+  (s : set γ) [is_submonoid s] : is_submonoid (f ⁻¹' s) :=
+{ one_mem := show f 1 ∈ s, by rw is_monoid_hom.map_one f; exact is_submonoid.one_mem s,
+  mul_mem := λ a b (ha : f a ∈ s) (hb : f b ∈ s),
+    show f (a * b) ∈ s, by rw is_monoid_hom.map_mul f; exact is_submonoid.mul_mem ha hb }
+
+@[instance, to_additive image.is_add_submonoid]
+lemma image.is_submonoid {γ : Type*} [monoid γ] (f : α → γ) [is_monoid_hom f]
+  (s : set α) [is_submonoid s] : is_submonoid (f '' s) :=
+{ one_mem := ⟨1, is_submonoid.one_mem s, is_monoid_hom.map_one f⟩,
+  mul_mem := λ a b ⟨x, hx⟩ ⟨y, hy⟩, ⟨x * y, is_submonoid.mul_mem hx.1 hy.1,
+    by rw [is_monoid_hom.map_mul f, hx.2, hy.2]⟩ }
+
+instance range.is_submonoid {γ : Type*} [monoid γ] (f : α → γ) [is_monoid_hom f] :
+  is_submonoid (set.range f) :=
+by rw ← set.image_univ; apply_instance
+
 lemma is_submonoid.pow_mem {a : α} [is_submonoid s] (h : a ∈ s) : ∀ {n : ℕ}, a ^ n ∈ s
 | 0 := is_submonoid.one_mem s
 | (n + 1) := is_submonoid.mul_mem h is_submonoid.pow_mem
diff --git a/src/ring_theory/subring.lean b/src/ring_theory/subring.lean
index 68b76903e2e30..b460a850b1a01 100644
--- a/src/ring_theory/subring.lean
+++ b/src/ring_theory/subring.lean
@@ -26,13 +26,14 @@ namespace is_ring_hom
 instance {S : set R} [is_subring S] : is_ring_hom (@subtype.val R S) :=
 by refine {..} ; intros ; refl
 
+instance is_subring_preimage {R : Type u} {S : Type v} [ring R] [ring S]
+  (f : R → S) [is_ring_hom f] (s : set S) [is_subring s] : is_subring (f ⁻¹' s) := {}
+
+instance is_subring_image {R : Type u} {S : Type v} [ring R] [ring S]
+  (f : R → S) [is_ring_hom f] (s : set R) [is_subring s] : is_subring (f '' s) := {}
+
 instance is_subring_set_range {R : Type u} {S : Type v} [ring R] [ring S]
-  (f : R → S) [is_ring_hom f] : is_subring (set.range f) :=
-{ zero_mem := ⟨0, is_ring_hom.map_zero f⟩,
-  one_mem := ⟨1, is_ring_hom.map_one f⟩,
-  neg_mem := λ x ⟨p, hp⟩, ⟨-p, hp ▸ is_ring_hom.map_neg f⟩,
-  add_mem := λ x y ⟨p, hp⟩ ⟨q, hq⟩, ⟨p + q, hp ▸ hq ▸ is_ring_hom.map_add f⟩,
-  mul_mem := λ x y ⟨p, hp⟩ ⟨q, hq⟩, ⟨p * q, hp ▸ hq ▸ is_ring_hom.map_mul f⟩, }
+  (f : R → S) [is_ring_hom f] : is_subring (set.range f) := {}
 
 end is_ring_hom