feat(ring_theory/subring) various lemmas

ring_theory/subring.lean

@@ -27,6 +27,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_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⟩, }
+
 end is_ring_hom
 
 variables {cR : Type u} [comm_ring cR]
@@ -48,7 +56,7 @@ variable {s : set R}
 local attribute [reducible] closure
 
 theorem exists_list_of_mem_closure {a : R} (h : a ∈ closure s) :
-  (∃ L : list (list R), (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ -x ∈ s ∨ x = (-1:R)) ∧ (L.map list.prod).sum = a) :=
+  (∃ L : list (list R), (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = (-1:R)) ∧ (L.map list.prod).sum = a) :=
 add_group.in_closure.rec_on h
   (λ x hx, match x, monoid.exists_list_of_mem_closure hx with
     | _, ⟨L, h1, rfl⟩ := ⟨[L], list.forall_mem_singleton.2 (λ r hr, or.inl (h1 r hr)), zero_add _⟩
@@ -57,7 +65,7 @@ add_group.in_closure.rec_on h
   (λ b _ ih, match b, ih with
     | _, ⟨L1, h1, rfl⟩ := ⟨L1.map (list.cons (-1)),
       λ L2 h2, match L2, list.mem_map.1 h2 with
-        | _, ⟨L3, h3, rfl⟩ := list.forall_mem_cons.2 ⟨or.inr $ or.inr rfl, h1 L3 h3⟩
+        | _, ⟨L3, h3, rfl⟩ := list.forall_mem_cons.2 ⟨or.inr rfl, h1 L3 h3⟩
         end,
       by simp only [list.map_map, (∘), list.prod_cons, neg_one_mul];
       exact list.rec_on L1 neg_zero.symm (λ hd tl ih,
@@ -68,6 +76,41 @@ add_group.in_closure.rec_on h
       by rw [list.map_append, list.sum_append]⟩
     end)
 
+@[elab_as_eliminator]
+protected theorem in_closure.rec_on {C : R → Prop} {x : R} (hx : x ∈ closure s)
+  (h1 : C 1) (hneg1 : C (-1)) (hs : ∀ z ∈ s, ∀ n, C n → C (z * n))
+  (ha : ∀ {x y}, C x → C y → C (x + y)) : C x :=
+begin
+  have h0 : C 0 := add_neg_self (1:R) ▸ ha h1 hneg1,
+  rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩, clear hx,
+  induction L with hd tl ih, { exact h0 },
+  rw list.forall_mem_cons at HL,
+  suffices : C (list.prod hd),
+  { rw [list.map_cons, list.sum_cons],
+    exact ha this (ih HL.2) },
+  replace HL := HL.1, clear ih tl,
+  suffices : ∃ L : list R, (∀ x ∈ L, x ∈ s) ∧ (list.prod hd = list.prod L ∨ list.prod hd = -list.prod L),
+  { rcases this with ⟨L, HL', HP | HP⟩,
+    { rw HP, clear HP HL hd, induction L with hd tl ih, { exact h1 },
+      rw list.forall_mem_cons at HL',
+      rw list.prod_cons,
+      exact hs _ HL'.1 _ (ih HL'.2) },
+    rw HP, clear HP HL hd, induction L with hd tl ih, { exact hneg1 },
+    rw [list.prod_cons, neg_mul_eq_mul_neg],
+    rw list.forall_mem_cons at HL',
+    exact hs _ HL'.1 _ (ih HL'.2) },
+  induction hd with hd tl ih,
+  { exact ⟨[], list.forall_mem_nil _, or.inl rfl⟩ },
+  rw list.forall_mem_cons at HL,
+  rcases ih HL.2 with ⟨L, HL', HP | HP⟩; cases HL.1 with hhd hhd,
+  { exact ⟨hd :: L, list.forall_mem_cons.2 ⟨hhd, HL'⟩, or.inl $
+      by rw [list.prod_cons, list.prod_cons, HP]⟩ },
+  { exact ⟨L, HL', or.inr $ by rw [list.prod_cons, hhd, neg_one_mul, HP]⟩ },
+  { exact ⟨hd :: L, list.forall_mem_cons.2 ⟨hhd, HL'⟩, or.inr $
+      by rw [list.prod_cons, list.prod_cons, HP, neg_mul_eq_mul_neg]⟩ },
+  { exact ⟨L, HL', or.inl $ by rw [list.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩ }
+end
+
 instance : is_subring (closure s) :=
 { one_mem := add_group.mem_closure (is_submonoid.one_mem _),
   mul_mem := λ a b ha hb, add_group.in_closure.rec_on hb
@@ -94,4 +137,7 @@ theorem closure_subset_iff (s t : set R) [is_subring t] : closure s ⊆ t ↔ s
 (add_group.closure_subset_iff _ t).trans
   ⟨set.subset.trans monoid.subset_closure, monoid.closure_subset⟩
 
+theorem closure_mono {s t : set R} (H : s ⊆ t) : closure s ⊆ closure t :=
+closure_subset $ set.subset.trans H subset_closure
+
 end ring