feature(ring_theory/subring): ring.closure

group_theory/subgroup.lean

@@ -194,6 +194,14 @@ theorem gmultiples_eq_closure {a : α} : gmultiples a = closure {a} :=
 group.gpowers_eq_closure
 attribute [to_additive add_group.gmultiples_eq_closure] group.gpowers_eq_closure
 
+@[elab_as_eliminator]
+theorem add_group.in_closure.rec_on {C : α → Prop}
+  {a : α} (H : a ∈ add_group.closure s)
+  (H1 : ∀ {a : α}, a ∈ s → C a) (H2 : C 0) (H3 : ∀ {a : α}, a ∈ add_group.closure s → C a → C (-a))
+  (H4 : ∀ {a b : α}, a ∈ add_group.closure s → b ∈ add_group.closure s → C a → C b → C (a + b)) :
+  C a :=
+group.in_closure.rec_on H (λ _, H1) H2 (λ _, H3) (λ _ _, H4)
+
 end add_group
 
 class normal_subgroup [group α] (s : set α) extends is_subgroup s : Prop :=

group_theory/submonoid.lean

@@ -182,4 +182,12 @@ theorem exists_list_of_mem_closure {s : set β} {a : β} :
   a ∈ closure s → ∃l:list β, (∀x∈l, x ∈ s) ∧ l.sum = a :=
 @monoid.exists_list_of_mem_closure (multiplicative β) _ _ _
 
+@[elab_as_eliminator]
+theorem add_monoid.in_closure.rec_on {s : set β} {C : β → Prop}
+  {a : β} (H : a ∈ closure s)
+  (H1 : ∀ {a : β}, a ∈ s → C a) (H2 : C 0)
+  (H3 : ∀ {a b : β}, a ∈ closure s → b ∈ closure s → C a → C b → C (a + b)) :
+  C a :=
+monoid.in_closure.rec_on H (λ _, H1) H2 (λ _ _, H3)
+
 end add_monoid

ring_theory/subring.lean

@@ -39,3 +39,60 @@ instance subtype.comm_ring {S : set cR} [is_subring S] : comm_ring (subtype S) :
 
 instance subring.domain {D : Type*} [integral_domain D] (S : set D) [is_subring S] : integral_domain S :=
 by subtype_instance
+
+namespace ring
+
+def closure (s : set R) := add_group.closure (monoid.closure s)
+
+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) :=
+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 _⟩
+    end)
+  ⟨[], list.forall_mem_nil _, rfl⟩
+  (λ 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⟩
+        end,
+      by simp only [list.map_map, (∘), list.prod_cons, neg_one_mul];
+      exact list.rec_on L1 neg_zero.symm (λ hd tl ih,
+        by rw [list.map_cons, list.sum_cons, ih, list.map_cons, list.sum_cons, neg_add])⟩
+    end)
+  (λ r1 r2 hr1 hr2 ih1 ih2, match r1, r2, ih1, ih2 with
+    | _, _, ⟨L1, h1, rfl⟩, ⟨L2, h2, rfl⟩ := ⟨L1 ++ L2, list.forall_mem_append.2 ⟨h1, h2⟩,
+      by rw [list.map_append, list.sum_append]⟩
+    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
+    (λ b hb, add_group.in_closure.rec_on ha
+      (λ a ha, add_group.subset_closure (is_submonoid.mul_mem ha hb))
+      ((zero_mul b).symm ▸ is_add_submonoid.zero_mem _)
+      (λ a ha hab, (neg_mul_eq_neg_mul a b) ▸ is_add_subgroup.neg_mem hab)
+      (λ a c ha hc hab hcb, (add_mul a c b).symm ▸ is_add_submonoid.add_mem hab hcb))
+    ((mul_zero a).symm ▸ is_add_submonoid.zero_mem _)
+    (λ b hb hab, (neg_mul_eq_mul_neg a b) ▸ is_add_subgroup.neg_mem hab)
+    (λ b c hb hc hab hac, (mul_add a b c).symm ▸ is_add_submonoid.add_mem hab hac),
+  .. add_group.closure.is_add_subgroup _ }
+
+theorem mem_closure {a : R} : a ∈ s → a ∈ closure s :=
+add_group.mem_closure ∘ @monoid.subset_closure _ _ _ _
+
+theorem subset_closure : s ⊆ closure s :=
+λ _, mem_closure
+
+theorem closure_subset {t : set R} [is_subring t] : s ⊆ t → closure s ⊆ t :=
+add_group.closure_subset ∘ monoid.closure_subset
+
+theorem closure_subset_iff (s t : set R) [is_subring t] : closure s ⊆ t ↔ s ⊆ t :=
+(add_group.closure_subset_iff _ t).trans
+  ⟨set.subset.trans monoid.subset_closure, monoid.closure_subset⟩
+
+end ring