|
| 1 | +/- |
| 2 | +Copyright (c) 2018 Johan Commelin. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Johan Commelin |
| 5 | +
|
| 6 | +! This file was ported from Lean 3 source module deprecated.subring |
| 7 | +! leanprover-community/mathlib commit 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d |
| 8 | +! Please do not edit these lines, except to modify the commit id |
| 9 | +! if you have ported upstream changes. |
| 10 | +-/ |
| 11 | +import Mathlib.Deprecated.Subgroup |
| 12 | +import Mathlib.Deprecated.Group |
| 13 | +import Mathlib.RingTheory.Subring.Basic |
| 14 | + |
| 15 | +/-! |
| 16 | +# Unbundled subrings (deprecated) |
| 17 | +
|
| 18 | +This file is deprecated, and is no longer imported by anything in mathlib other than other |
| 19 | +deprecated files, and test files. You should not need to import it. |
| 20 | +
|
| 21 | +This file defines predicates for unbundled subrings. Instead of using this file, please use |
| 22 | +`Subring`, defined in `RingTheory.Subring.Basic`, for subrings of rings. |
| 23 | +
|
| 24 | +## Main definitions |
| 25 | +
|
| 26 | +`IsSubring (S : Set R) : Prop` : the predicate that `S` is the underlying set of a subring |
| 27 | +of the ring `R`. The bundled variant `Subring R` should be used in preference to this. |
| 28 | +
|
| 29 | +## Tags |
| 30 | +
|
| 31 | +is_subring |
| 32 | +-/ |
| 33 | + |
| 34 | + |
| 35 | +universe u v |
| 36 | + |
| 37 | +open Group |
| 38 | + |
| 39 | +variable {R : Type u} [Ring R] |
| 40 | + |
| 41 | +/-- `S` is a subring: a set containing 1 and closed under multiplication, addition and additive |
| 42 | +inverse. -/ |
| 43 | +structure IsSubring (S : Set R) extends IsAddSubgroup S, IsSubmonoid S : Prop |
| 44 | +#align is_subring IsSubring |
| 45 | + |
| 46 | +/-- Construct a `Subring` from a set satisfying `IsSubring`. -/ |
| 47 | +def IsSubring.subring {S : Set R} (hs : IsSubring S) : Subring R where |
| 48 | + carrier := S |
| 49 | + one_mem' := hs.one_mem |
| 50 | + mul_mem' := hs.mul_mem |
| 51 | + zero_mem' := hs.zero_mem |
| 52 | + add_mem' := hs.add_mem |
| 53 | + neg_mem' := hs.neg_mem |
| 54 | +#align is_subring.subring IsSubring.subring |
| 55 | + |
| 56 | +namespace RingHom |
| 57 | + |
| 58 | +theorem isSubring_preimage {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) {s : Set S} |
| 59 | + (hs : IsSubring s) : IsSubring (f ⁻¹' s) := |
| 60 | + { IsAddGroupHom.preimage f.to_isAddGroupHom hs.toIsAddSubgroup, |
| 61 | + IsSubmonoid.preimage f.to_isMonoidHom hs.toIsSubmonoid with } |
| 62 | +#align ring_hom.is_subring_preimage RingHom.isSubring_preimage |
| 63 | + |
| 64 | +theorem isSubring_image {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) {s : Set R} |
| 65 | + (hs : IsSubring s) : IsSubring (f '' s) := |
| 66 | + { IsAddGroupHom.image_addSubgroup f.to_isAddGroupHom hs.toIsAddSubgroup, |
| 67 | + IsSubmonoid.image f.to_isMonoidHom hs.toIsSubmonoid with } |
| 68 | +#align ring_hom.is_subring_image RingHom.isSubring_image |
| 69 | + |
| 70 | +theorem isSubring_set_range {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : |
| 71 | + IsSubring (Set.range f) := |
| 72 | + { IsAddGroupHom.range_addSubgroup f.to_isAddGroupHom, Range.isSubmonoid f.to_isMonoidHom with } |
| 73 | +#align ring_hom.is_subring_set_range RingHom.isSubring_set_range |
| 74 | + |
| 75 | +end RingHom |
| 76 | + |
| 77 | +variable {cR : Type u} [CommRing cR] |
| 78 | + |
| 79 | +theorem IsSubring.inter {S₁ S₂ : Set R} (hS₁ : IsSubring S₁) (hS₂ : IsSubring S₂) : |
| 80 | + IsSubring (S₁ ∩ S₂) := |
| 81 | + { IsAddSubgroup.inter hS₁.toIsAddSubgroup hS₂.toIsAddSubgroup, |
| 82 | + IsSubmonoid.inter hS₁.toIsSubmonoid hS₂.toIsSubmonoid with } |
| 83 | +#align is_subring.inter IsSubring.inter |
| 84 | + |
| 85 | +theorem IsSubring.interᵢ {ι : Sort _} {S : ι → Set R} (h : ∀ y : ι, IsSubring (S y)) : |
| 86 | + IsSubring (Set.interᵢ S) := |
| 87 | + { IsAddSubgroup.interᵢ fun i ↦ (h i).toIsAddSubgroup, |
| 88 | + IsSubmonoid.interᵢ fun i ↦ (h i).toIsSubmonoid with } |
| 89 | +#align is_subring.Inter IsSubring.interᵢ |
| 90 | + |
| 91 | +theorem isSubring_unionᵢ_of_directed {ι : Type _} [Nonempty ι] {s : ι → Set R} |
| 92 | + (h : ∀ i, IsSubring (s i)) (directed : ∀ i j, ∃ k, s i ⊆ s k ∧ s j ⊆ s k) : |
| 93 | + IsSubring (⋃ i, s i) := |
| 94 | + { toIsAddSubgroup := isAddSubgroup_unionᵢ_of_directed (fun i ↦ (h i).toIsAddSubgroup) directed |
| 95 | + toIsSubmonoid := isSubmonoid_unionᵢ_of_directed (fun i ↦ (h i).toIsSubmonoid) directed } |
| 96 | +#align is_subring_Union_of_directed isSubring_unionᵢ_of_directed |
| 97 | + |
| 98 | +namespace Ring |
| 99 | + |
| 100 | +/-- The smallest subring containing a given subset of a ring, considered as a set. This function |
| 101 | +is deprecated; use `Subring.closure`. -/ |
| 102 | +def closure (s : Set R) := |
| 103 | + AddGroup.closure (Monoid.Closure s) |
| 104 | +#align ring.closure Ring.closure |
| 105 | + |
| 106 | +variable {s : Set R} |
| 107 | + |
| 108 | +-- attribute [local reducible] closure -- Porting note: not available in Lean4 |
| 109 | + |
| 110 | +theorem exists_list_of_mem_closure {a : R} (h : a ∈ closure s) : |
| 111 | + ∃ L : List (List R), (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = (-1 : R)) ∧ (L.map List.prod).sum = a := |
| 112 | + AddGroup.InClosure.recOn h |
| 113 | + fun {x} hx ↦ match x, Monoid.exists_list_of_mem_closure hx with |
| 114 | + | _, ⟨L, h1, rfl⟩ => ⟨[L], List.forall_mem_singleton.2 fun r hr ↦ Or.inl (h1 r hr), zero_add _⟩ |
| 115 | + ⟨[], List.forall_mem_nil _, rfl⟩ |
| 116 | + fun {b} _ ih ↦ match b, ih with |
| 117 | + | _, ⟨L1, h1, rfl⟩ => |
| 118 | + ⟨L1.map (List.cons (-1)), |
| 119 | + fun L2 h2 ↦ match L2, List.mem_map'.1 h2 with |
| 120 | + | _, ⟨L3, h3, rfl⟩ => List.forall_mem_cons.2 ⟨Or.inr rfl, h1 L3 h3⟩, by |
| 121 | + simp only [List.map_map, (· ∘ ·), List.prod_cons, neg_one_mul] |
| 122 | + refine' List.recOn L1 neg_zero.symm fun hd tl ih ↦ _ |
| 123 | + rw [List.map_cons, List.sum_cons, ih, List.map_cons, List.sum_cons, neg_add]⟩ |
| 124 | + fun {r1 r2} _ _ ih1 ih2 ↦ match r1, r2, ih1, ih2 with |
| 125 | + | _, _, ⟨L1, h1, rfl⟩, ⟨L2, h2, rfl⟩ => |
| 126 | + ⟨L1 ++ L2, List.forall_mem_append.2 ⟨h1, h2⟩, by rw [List.map_append, List.sum_append]⟩ |
| 127 | +#align ring.exists_list_of_mem_closure Ring.exists_list_of_mem_closure |
| 128 | + |
| 129 | +@[elab_as_elim] |
| 130 | +protected theorem InClosure.recOn {C : R → Prop} {x : R} (hx : x ∈ closure s) (h1 : C 1) |
| 131 | + (hneg1 : C (-1)) (hs : ∀ z ∈ s, ∀ n, C n → C (z * n)) (ha : ∀ {x y}, C x → C y → C (x + y)) : |
| 132 | + C x := by |
| 133 | + have h0 : C 0 := add_neg_self (1 : R) ▸ ha h1 hneg1 |
| 134 | + rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩ |
| 135 | + clear hx |
| 136 | + induction' L with hd tl ih |
| 137 | + · exact h0 |
| 138 | + rw [List.forall_mem_cons] at HL |
| 139 | + suffices C (List.prod hd) by |
| 140 | + rw [List.map_cons, List.sum_cons] |
| 141 | + exact ha this (ih HL.2) |
| 142 | + replace HL := HL.1 |
| 143 | + clear ih tl |
| 144 | + -- Porting note: Expanded `rsuffices` |
| 145 | + suffices ∃ L, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L) by |
| 146 | + rcases this with ⟨L, HL', HP | HP⟩ <;> rw [HP] <;> clear HP HL |
| 147 | + · induction' L with hd tl ih |
| 148 | + · exact h1 |
| 149 | + rw [List.forall_mem_cons] at HL' |
| 150 | + rw [List.prod_cons] |
| 151 | + exact hs _ HL'.1 _ (ih HL'.2) |
| 152 | + · induction' L with hd tl ih |
| 153 | + · exact hneg1 |
| 154 | + rw [List.prod_cons, neg_mul_eq_mul_neg] |
| 155 | + rw [List.forall_mem_cons] at HL' |
| 156 | + exact hs _ HL'.1 _ (ih HL'.2) |
| 157 | + induction' hd with hd tl ih |
| 158 | + · exact ⟨[], List.forall_mem_nil _, Or.inl rfl⟩ |
| 159 | + rw [List.forall_mem_cons] at HL |
| 160 | + rcases ih HL.2 with ⟨L, HL', HP | HP⟩ <;> cases' HL.1 with hhd hhd |
| 161 | + · exact |
| 162 | + ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, |
| 163 | + Or.inl <| by rw [List.prod_cons, List.prod_cons, HP]⟩ |
| 164 | + · exact ⟨L, HL', Or.inr <| by rw [List.prod_cons, hhd, neg_one_mul, HP]⟩ |
| 165 | + · exact |
| 166 | + ⟨hd::L, List.forall_mem_cons.2 ⟨hhd, HL'⟩, |
| 167 | + Or.inr <| by rw [List.prod_cons, List.prod_cons, HP, neg_mul_eq_mul_neg]⟩ |
| 168 | + · exact ⟨L, HL', Or.inl <| by rw [List.prod_cons, hhd, HP, neg_one_mul, neg_neg]⟩ |
| 169 | +#align ring.in_closure.rec_on Ring.InClosure.recOn |
| 170 | + |
| 171 | +theorem closure.isSubring : IsSubring (closure s) := |
| 172 | + { AddGroup.closure.isAddSubgroup _ with |
| 173 | + one_mem := AddGroup.mem_closure <| IsSubmonoid.one_mem <| Monoid.closure.isSubmonoid _ |
| 174 | + mul_mem := fun {a _} ha hb ↦ AddGroup.InClosure.recOn hb |
| 175 | + (fun {c} hc ↦ AddGroup.InClosure.recOn ha |
| 176 | + (fun hd ↦ AddGroup.subset_closure ((Monoid.closure.isSubmonoid _).mul_mem hd hc)) |
| 177 | + ((zero_mul c).symm ▸ (AddGroup.closure.isAddSubgroup _).zero_mem) |
| 178 | + (fun {d} _ hdc ↦ neg_mul_eq_neg_mul d c ▸ (AddGroup.closure.isAddSubgroup _).neg_mem hdc) |
| 179 | + fun {d e} _ _ hdc hec ↦ |
| 180 | + (add_mul d e c).symm ▸ (AddGroup.closure.isAddSubgroup _).add_mem hdc hec) |
| 181 | + ((mul_zero a).symm ▸ (AddGroup.closure.isAddSubgroup _).zero_mem) |
| 182 | + (fun {c} _ hac ↦ neg_mul_eq_mul_neg a c ▸ (AddGroup.closure.isAddSubgroup _).neg_mem hac) |
| 183 | + fun {c d} _ _ hac had ↦ |
| 184 | + (mul_add a c d).symm ▸ (AddGroup.closure.isAddSubgroup _).add_mem hac had } |
| 185 | +#align ring.closure.is_subring Ring.closure.isSubring |
| 186 | + |
| 187 | +theorem mem_closure {a : R} : a ∈ s → a ∈ closure s := |
| 188 | + AddGroup.mem_closure ∘ @Monoid.subset_closure _ _ _ _ |
| 189 | +#align ring.mem_closure Ring.mem_closure |
| 190 | + |
| 191 | +theorem subset_closure : s ⊆ closure s := |
| 192 | + fun _ ↦ mem_closure |
| 193 | +#align ring.subset_closure Ring.subset_closure |
| 194 | + |
| 195 | +theorem closure_subset {t : Set R} (ht : IsSubring t) : s ⊆ t → closure s ⊆ t := |
| 196 | + AddGroup.closure_subset ht.toIsAddSubgroup ∘ Monoid.closure_subset ht.toIsSubmonoid |
| 197 | +#align ring.closure_subset Ring.closure_subset |
| 198 | + |
| 199 | +theorem closure_subset_iff {s t : Set R} (ht : IsSubring t) : closure s ⊆ t ↔ s ⊆ t := |
| 200 | + (AddGroup.closure_subset_iff ht.toIsAddSubgroup).trans |
| 201 | + ⟨Set.Subset.trans Monoid.subset_closure, Monoid.closure_subset ht.toIsSubmonoid⟩ |
| 202 | +#align ring.closure_subset_iff Ring.closure_subset_iff |
| 203 | + |
| 204 | +theorem closure_mono {s t : Set R} (H : s ⊆ t) : closure s ⊆ closure t := |
| 205 | + closure_subset closure.isSubring <| Set.Subset.trans H subset_closure |
| 206 | +#align ring.closure_mono Ring.closure_mono |
| 207 | + |
| 208 | +theorem image_closure {S : Type _} [Ring S] (f : R →+* S) (s : Set R) : |
| 209 | + f '' closure s = closure (f '' s) := by |
| 210 | + refine' le_antisymm _ (closure_subset (RingHom.isSubring_image _ closure.isSubring) <| |
| 211 | + Set.image_subset _ subset_closure) |
| 212 | + rintro _ ⟨x, hx, rfl⟩ |
| 213 | + apply AddGroup.InClosure.recOn (motive := fun {x} _ ↦ f x ∈ closure (f '' s)) hx _ <;> intros |
| 214 | + · rw [f.map_zero] |
| 215 | + apply closure.isSubring.zero_mem |
| 216 | + · rw [f.map_neg] |
| 217 | + apply closure.isSubring.neg_mem |
| 218 | + assumption |
| 219 | + · rw [f.map_add] |
| 220 | + apply closure.isSubring.add_mem |
| 221 | + assumption' |
| 222 | + · apply AddGroup.mem_closure |
| 223 | + rw [← Monoid.image_closure f.to_isMonoidHom] |
| 224 | + apply Set.mem_image_of_mem |
| 225 | + assumption |
| 226 | +#align ring.image_closure Ring.image_closure |
| 227 | + |
| 228 | +end Ring |
0 commit comments