feat(ring_theory): move localization

Author: kckennylau

algebra/group.lean

@@ -229,12 +229,18 @@ section monoid
 
   @[simp] theorem divp_right_inj (u : units α) {a b : α} : a /ₚ u = b /ₚ u ↔ a = b :=
   units.mul_right_inj _
-  
+
   theorem divp_eq_one (a : α) (u : units α) : a /ₚ u = 1 ↔ a = u :=
   (units.mul_right_inj u).symm.trans $ by simp
 
   @[simp] theorem one_divp (u : units α) : 1 /ₚ u = ↑u⁻¹ :=
   by simp [divp]
+  
+  variable α
+  
+  class is_submonoid (S : set α) : Prop :=
+  (one_mem : (1:α) ∈ S)
+  (mul_mem : ∀ {s t}, s ∈ S → t ∈ S → s*t ∈ S)
 
 end monoid
 

algebra/group_power.lean

@@ -104,6 +104,12 @@ by rw [←pow_add, ←pow_add, add_comm]
 | (n+1) := by simp [smul_succ, list.sum_repeat n]
 attribute [to_additive list.sum_repeat] list.prod_repeat
 
+def powers (x : α) : set α := {y | ∃ n, x^n = y}
+
+instance powers.is_submonoid (x : α) : is_submonoid α (powers x) :=
+{ one_mem := ⟨0, by simp⟩,
+  mul_mem := λ x₁ x₂ ⟨n₁, hn₁⟩ ⟨n₂, hn₂⟩, ⟨n₁ + n₂, by simp [pow_add, *]⟩ }
+
 end monoid
 
 theorem nat.pow_eq_pow (p q : ℕ) : nat.pow p q = p ^ q :=

algebra/localization.lean

@@ -228,6 +228,21 @@ end
 
 end is_submodule
 
+section comm_ring
+
+theorem is_submodule.eq_univ_of_contains_unit {α : Type u} [comm_ring α] (S : set α) [is_submodule S]
+  (x y : α) (hx : x ∈ S) (h : y * x = 1) : S = set.univ :=
+set.ext $ λ z, ⟨λ hz, trivial, λ hz, calc
+    z = z * (y * x) : by simp [h]
+  ... = (z * y) * x : eq.symm $ mul_assoc z y x
+  ... ∈ S : is_submodule.smul (z * y) hx⟩
+
+theorem is_submodule.univ_of_one_mem {α : Type u} [comm_ring α] (S : set α) [is_submodule S] :
+  (1:α) ∈ S → S = set.univ :=
+λ h, set.ext $ λ z, ⟨λ hz, trivial, λ hz, by simpa using (is_submodule.smul z h : z * 1 ∈ S)⟩
+
+end comm_ring
+
 /-- A vector space is the same as a module, except the scalar ring is actually
   a field. (This adds commutativity of the multiplication and existence of inverses.)
   This is the traditional generalization of spaces like `ℝ^n`, which have a natural

algebra/module.lean

@@ -3,9 +3,9 @@ Copyright (c) 2014 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Leonardo de Moura, Floris van Doorn
 -/
-import algebra.group tactic
+import algebra.group tactic data.set.basic
 
-universe u
+universes u v
 variable {α : Type u}
 
 section
@@ -57,6 +57,31 @@ section comm_ring
   ⟨dvd_of_neg_dvd, neg_dvd_of_dvd⟩
 end comm_ring
 
+def nonunits (α : Type u) [comm_ring α] : set α := { x | ¬∃ y, y * x = 1 }
+
+class is_ring_hom {α : Type u} {β : Type v} [comm_ring α] [comm_ring β] (f : α → β) : Prop :=
+(map_add : ∀ {x y}, f (x + y) = f x + f y)
+(map_mul : ∀ {x y}, f (x * y) = f x * f y)
+(map_one : f 1 = 1)
+
+namespace is_ring_hom
+
+variables {β : Type v} [comm_ring α] [comm_ring β]
+variables (f : α → β) [is_ring_hom f] {x y : α}
+
+lemma map_zero : f 0 = 0 :=
+calc f 0 = f (0 + 0) - f 0 : by rw [map_add f]; simp
+     ... = 0 : by simp
+
+lemma map_neg : f (-x) = -f x :=
+calc f (-x) = f (-x + x) - f x : by rw [map_add f]; simp
+        ... = -f x : by simp [map_zero f]
+
+lemma map_sub : f (x - y) = f x - f y :=
+by simp [map_add f, map_neg f]
+
+end is_ring_hom
+
 set_option old_structure_cmd true
 /-- A domain is a ring with no zero divisors, i.e. satisfying
   the condition `a * b = 0 ↔ a = 0 ∨ b = 0`. Alternatively, a domain

algebra/ring.lean

@@ -14,6 +14,12 @@ theorem forall_quotient_iff {α : Type*} [r : setoid α] {p : quotient r → Pro
   (∀a:quotient r, p a) ↔ (∀a:α, p ⟦a⟧) :=
 ⟨assume h x, h _, assume h a, a.induction_on h⟩
 
+@[simp] lemma quotient.lift_beta [s : setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α):
+quotient.lift f h (quotient.mk x) = f x := rfl
+
+@[simp] lemma quotient.lift_on_beta [s : setoid α] (f : α → β) (h : ∀ (a b : α), a ≈ b → f a = f b) (x : α):
+quotient.lift_on (quotient.mk x) f h = f x := rfl
+
 /-- Choose an element of the equivalence class using the axiom of choice.
   Sound but noncomputable. -/
 noncomputable def quot.out {r : α → α → Prop} (q : quot r) : α :=

data/quot.lean

@@ -0,0 +1,51 @@
+import algebra.ring algebra.module data.set.basic
+
+universe u
+
+class is_ideal {α : Type u} [comm_ring α] (S : set α) extends is_submodule S : Prop
+
+class is_proper_ideal {α : Type u} [comm_ring α] (S : set α) extends is_ideal S : Prop :=
+(ne_univ : S ≠ set.univ)
+
+class is_prime_ideal {α : Type u} [comm_ring α] (S : set α) extends is_proper_ideal S : Prop :=
+(mem_or_mem_of_mul_mem : ∀ {x y : α}, x * y ∈ S → x ∈ S ∨ y ∈ S)
+
+theorem mem_or_mem_of_mul_eq_zero {α : Type u} [comm_ring α] (S : set α) [is_prime_ideal S] :
+  ∀ {x y : α}, x * y = 0 → x ∈ S ∨ y ∈ S :=
+λ x y hxy, have x * y ∈ S, by rw hxy; from (@is_submodule.zero α α _ _ S _ : (0:α) ∈ S),
+is_prime_ideal.mem_or_mem_of_mul_mem this
+
+class is_maximal_ideal {α : Type u} [comm_ring α] (S : set α) extends is_proper_ideal S : Prop :=
+mk' ::
+  (eq_or_univ_of_subset : ∀ (T : set α) [is_submodule T], S ⊆ T → T = S ∨ T = set.univ)
+
+theorem is_maximal_ideal.mk {α : Type u} [comm_ring α] (S : set α) [is_submodule S] :
+  (1:α) ∉ S → (∀ x (T : set α) [is_submodule T], S ⊆ T → x ∉ S → x ∈ T → (1:α) ∈ T) → is_maximal_ideal S :=
+λ h₁ h₂,
+{ ne_univ := λ hu, have (1:α) ∈ S, by rw hu; trivial, h₁ this,
+  eq_or_univ_of_subset := λ T ht hst, or.cases_on (classical.em $ ∃ x, x ∉ S ∧ x ∈ T)
+    (λ ⟨x, hxns, hxt⟩, or.inr $ @@is_submodule.univ_of_one_mem _ T ht $ @@h₂ x T ht hst hxns hxt)
+    (λ hnts, or.inl $ set.ext $ λ x,
+       ⟨λ hxt, classical.by_contradiction $ λ hxns, hnts ⟨x, hxns, hxt⟩,
+        λ hxs, hst hxs⟩) }
+
+theorem not_unit_of_mem_maximal_ideal {α : Type u} [comm_ring α] (S : set α) [is_maximal_ideal S] : S ⊆ nonunits α :=
+λ x hx ⟨y, hxy⟩, is_proper_ideal.ne_univ S $ is_submodule.eq_univ_of_contains_unit S x y hx hxy
+
+class local_ring (α : Type u) [comm_ring α] :=
+(S : set α)
+(max : is_maximal_ideal S)
+(unique : ∀ T [is_maximal_ideal T], S = T)
+
+def local_of_nonunits_ideal {α : Type u} [comm_ring α] : (0:α) ≠ 1 → (∀ x y ∈ nonunits α, x + y ∈ nonunits α) → local_ring α :=
+λ hnze h, have hi : is_submodule (nonunits α), from
+{ zero_ := λ ⟨y, hy⟩, hnze $ by simpa using hy,
+  add_  := h,
+  smul  := λ x y hy ⟨z, hz⟩, hy ⟨x * z, by rw [← hz]; simp [mul_left_comm, mul_assoc]⟩ },
+{ S := nonunits α,
+  max := @@is_maximal_ideal.mk _ (nonunits α) hi (λ ho, ho ⟨1, mul_one 1⟩) $
+    λ x T ht hst hxns hxt, have hxu : _, from classical.by_contradiction hxns,
+    let ⟨y, hxy⟩ := hxu in by rw [← hxy]; exact @@is_submodule.smul _ _ ht y hxt,
+  unique := λ T hmt, or.cases_on (@@is_maximal_ideal.eq_or_univ_of_subset _ hmt (nonunits α) hi $
+      λ z hz, @@not_unit_of_mem_maximal_ideal _ T hmt hz) id $
+    (λ htu, false.elim $ ((set.set_eq_def _ _).1 htu 1).2 trivial ⟨1, mul_one 1⟩) }