From 3b6ff86d9c65d95829f74c5cbfe1820cc52df9e7 Mon Sep 17 00:00:00 2001 From: Jason Yuen Date: Sat, 18 Feb 2023 18:40:15 +0000 Subject: [PATCH] feat: port Deprecated.Subring (#2355) --- Mathlib.lean | 1 + Mathlib/Deprecated/Subring.lean | 228 ++++++++++++++++++++++++++++++++ 2 files changed, 229 insertions(+) create mode 100644 Mathlib/Deprecated/Subring.lean diff --git a/Mathlib.lean b/Mathlib.lean index b4f450f5514a4..515721d9f850e 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -681,6 +681,7 @@ import Mathlib.Deprecated.Group import Mathlib.Deprecated.Ring import Mathlib.Deprecated.Subgroup import Mathlib.Deprecated.Submonoid +import Mathlib.Deprecated.Subring import Mathlib.Dynamics.FixedPoints.Basic import Mathlib.Dynamics.FixedPoints.Topology import Mathlib.Dynamics.Minimal diff --git a/Mathlib/Deprecated/Subring.lean b/Mathlib/Deprecated/Subring.lean new file mode 100644 index 0000000000000..820853d192bdf --- /dev/null +++ b/Mathlib/Deprecated/Subring.lean @@ -0,0 +1,228 @@ +/- +Copyright (c) 2018 Johan Commelin. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Johan Commelin + +! This file was ported from Lean 3 source module deprecated.subring +! leanprover-community/mathlib commit 2738d2ca56cbc63be80c3bd48e9ed90ad94e947d +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Deprecated.Subgroup +import Mathlib.Deprecated.Group +import Mathlib.RingTheory.Subring.Basic + +/-! +# Unbundled subrings (deprecated) + +This file is deprecated, and is no longer imported by anything in mathlib other than other +deprecated files, and test files. You should not need to import it. + +This file defines predicates for unbundled subrings. Instead of using this file, please use +`Subring`, defined in `RingTheory.Subring.Basic`, for subrings of rings. + +## Main definitions + +`IsSubring (S : Set R) : Prop` : the predicate that `S` is the underlying set of a subring +of the ring `R`. The bundled variant `Subring R` should be used in preference to this. + +## Tags + +is_subring +-/ + + +universe u v + +open Group + +variable {R : Type u} [Ring R] + +/-- `S` is a subring: a set containing 1 and closed under multiplication, addition and additive +inverse. -/ +structure IsSubring (S : Set R) extends IsAddSubgroup S, IsSubmonoid S : Prop +#align is_subring IsSubring + +/-- Construct a `Subring` from a set satisfying `IsSubring`. -/ +def IsSubring.subring {S : Set R} (hs : IsSubring S) : Subring R where + carrier := S + one_mem' := hs.one_mem + mul_mem' := hs.mul_mem + zero_mem' := hs.zero_mem + add_mem' := hs.add_mem + neg_mem' := hs.neg_mem +#align is_subring.subring IsSubring.subring + +namespace RingHom + +theorem isSubring_preimage {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) {s : Set S} + (hs : IsSubring s) : IsSubring (f ⁻¹' s) := + { IsAddGroupHom.preimage f.to_isAddGroupHom hs.toIsAddSubgroup, + IsSubmonoid.preimage f.to_isMonoidHom hs.toIsSubmonoid with } +#align ring_hom.is_subring_preimage RingHom.isSubring_preimage + +theorem isSubring_image {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) {s : Set R} + (hs : IsSubring s) : IsSubring (f '' s) := + { IsAddGroupHom.image_addSubgroup f.to_isAddGroupHom hs.toIsAddSubgroup, + IsSubmonoid.image f.to_isMonoidHom hs.toIsSubmonoid with } +#align ring_hom.is_subring_image RingHom.isSubring_image + +theorem isSubring_set_range {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : + IsSubring (Set.range f) := + { IsAddGroupHom.range_addSubgroup f.to_isAddGroupHom, Range.isSubmonoid f.to_isMonoidHom with } +#align ring_hom.is_subring_set_range RingHom.isSubring_set_range + +end RingHom + +variable {cR : Type u} [CommRing cR] + +theorem IsSubring.inter {S₁ S₂ : Set R} (hS₁ : IsSubring S₁) (hS₂ : IsSubring S₂) : + IsSubring (S₁ ∩ S₂) := + { IsAddSubgroup.inter hS₁.toIsAddSubgroup hS₂.toIsAddSubgroup, + IsSubmonoid.inter hS₁.toIsSubmonoid hS₂.toIsSubmonoid with } +#align is_subring.inter IsSubring.inter + +theorem IsSubring.interᵢ {ι : Sort _} {S : ι → Set R} (h : ∀ y : ι, IsSubring (S y)) : + IsSubring (Set.interᵢ S) := + { IsAddSubgroup.interᵢ fun i ↦ (h i).toIsAddSubgroup, + IsSubmonoid.interᵢ fun i ↦ (h i).toIsSubmonoid with } +#align is_subring.Inter IsSubring.interᵢ + +theorem isSubring_unionᵢ_of_directed {ι : Type _} [Nonempty ι] {s : ι → Set R} + (h : ∀ i, IsSubring (s i)) (directed : ∀ i j, ∃ k, s i ⊆ s k ∧ s j ⊆ s k) : + IsSubring (⋃ i, s i) := + { toIsAddSubgroup := isAddSubgroup_unionᵢ_of_directed (fun i ↦ (h i).toIsAddSubgroup) directed + toIsSubmonoid := isSubmonoid_unionᵢ_of_directed (fun i ↦ (h i).toIsSubmonoid) directed } +#align is_subring_Union_of_directed isSubring_unionᵢ_of_directed + +namespace Ring + +/-- The smallest subring containing a given subset of a ring, considered as a set. This function +is deprecated; use `Subring.closure`. -/ +def closure (s : Set R) := + AddGroup.closure (Monoid.Closure s) +#align ring.closure Ring.closure + +variable {s : Set R} + +-- attribute [local reducible] closure -- Porting note: not available in Lean4 + +theorem exists_list_of_mem_closure {a : R} (h : a ∈ closure s) : + ∃ L : List (List R), (∀ l ∈ L, ∀ x ∈ l, x ∈ s ∨ x = (-1 : R)) ∧ (L.map List.prod).sum = a := + AddGroup.InClosure.recOn h + fun {x} hx ↦ match x, Monoid.exists_list_of_mem_closure hx with + | _, ⟨L, h1, rfl⟩ => ⟨[L], List.forall_mem_singleton.2 fun r hr ↦ Or.inl (h1 r hr), zero_add _⟩ + ⟨[], List.forall_mem_nil _, rfl⟩ + fun {b} _ ih ↦ match b, ih with + | _, ⟨L1, h1, rfl⟩ => + ⟨L1.map (List.cons (-1)), + fun L2 h2 ↦ match L2, List.mem_map'.1 h2 with + | _, ⟨L3, h3, rfl⟩ => List.forall_mem_cons.2 ⟨Or.inr rfl, h1 L3 h3⟩, by + simp only [List.map_map, (· ∘ ·), List.prod_cons, neg_one_mul] + refine' List.recOn L1 neg_zero.symm fun hd tl ih ↦ _ + rw [List.map_cons, List.sum_cons, ih, List.map_cons, List.sum_cons, neg_add]⟩ + fun {r1 r2} _ _ 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]⟩ +#align ring.exists_list_of_mem_closure Ring.exists_list_of_mem_closure + +@[elab_as_elim] +protected theorem InClosure.recOn {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 := by + 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) by + rw [List.map_cons, List.sum_cons] + exact ha this (ih HL.2) + replace HL := HL.1 + clear ih tl + -- Porting note: Expanded `rsuffices` + suffices ∃ L, (∀ x ∈ L, x ∈ s) ∧ (List.prod hd = List.prod L ∨ List.prod hd = -List.prod L) by + rcases this with ⟨L, HL', HP | HP⟩ <;> rw [HP] <;> clear HP HL + · 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) + · 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]⟩ +#align ring.in_closure.rec_on Ring.InClosure.recOn + +theorem closure.isSubring : IsSubring (closure s) := + { AddGroup.closure.isAddSubgroup _ with + one_mem := AddGroup.mem_closure <| IsSubmonoid.one_mem <| Monoid.closure.isSubmonoid _ + mul_mem := fun {a _} ha hb ↦ AddGroup.InClosure.recOn hb + (fun {c} hc ↦ AddGroup.InClosure.recOn ha + (fun hd ↦ AddGroup.subset_closure ((Monoid.closure.isSubmonoid _).mul_mem hd hc)) + ((zero_mul c).symm ▸ (AddGroup.closure.isAddSubgroup _).zero_mem) + (fun {d} _ hdc ↦ neg_mul_eq_neg_mul d c ▸ (AddGroup.closure.isAddSubgroup _).neg_mem hdc) + fun {d e} _ _ hdc hec ↦ + (add_mul d e c).symm ▸ (AddGroup.closure.isAddSubgroup _).add_mem hdc hec) + ((mul_zero a).symm ▸ (AddGroup.closure.isAddSubgroup _).zero_mem) + (fun {c} _ hac ↦ neg_mul_eq_mul_neg a c ▸ (AddGroup.closure.isAddSubgroup _).neg_mem hac) + fun {c d} _ _ hac had ↦ + (mul_add a c d).symm ▸ (AddGroup.closure.isAddSubgroup _).add_mem hac had } +#align ring.closure.is_subring Ring.closure.isSubring + +theorem mem_closure {a : R} : a ∈ s → a ∈ closure s := + AddGroup.mem_closure ∘ @Monoid.subset_closure _ _ _ _ +#align ring.mem_closure Ring.mem_closure + +theorem subset_closure : s ⊆ closure s := + fun _ ↦ mem_closure +#align ring.subset_closure Ring.subset_closure + +theorem closure_subset {t : Set R} (ht : IsSubring t) : s ⊆ t → closure s ⊆ t := + AddGroup.closure_subset ht.toIsAddSubgroup ∘ Monoid.closure_subset ht.toIsSubmonoid +#align ring.closure_subset Ring.closure_subset + +theorem closure_subset_iff {s t : Set R} (ht : IsSubring t) : closure s ⊆ t ↔ s ⊆ t := + (AddGroup.closure_subset_iff ht.toIsAddSubgroup).trans + ⟨Set.Subset.trans Monoid.subset_closure, Monoid.closure_subset ht.toIsSubmonoid⟩ +#align ring.closure_subset_iff Ring.closure_subset_iff + +theorem closure_mono {s t : Set R} (H : s ⊆ t) : closure s ⊆ closure t := + closure_subset closure.isSubring <| Set.Subset.trans H subset_closure +#align ring.closure_mono Ring.closure_mono + +theorem image_closure {S : Type _} [Ring S] (f : R →+* S) (s : Set R) : + f '' closure s = closure (f '' s) := by + refine' le_antisymm _ (closure_subset (RingHom.isSubring_image _ closure.isSubring) <| + Set.image_subset _ subset_closure) + rintro _ ⟨x, hx, rfl⟩ + apply AddGroup.InClosure.recOn (motive := fun {x} _ ↦ f x ∈ closure (f '' s)) hx _ <;> intros + · rw [f.map_zero] + apply closure.isSubring.zero_mem + · rw [f.map_neg] + apply closure.isSubring.neg_mem + assumption + · rw [f.map_add] + apply closure.isSubring.add_mem + assumption' + · apply AddGroup.mem_closure + rw [← Monoid.image_closure f.to_isMonoidHom] + apply Set.mem_image_of_mem + assumption +#align ring.image_closure Ring.image_closure + +end Ring