Direct limit of modules, abelian groups, rings, and fields.

src/algebra/big_operators.lean

@@ -21,6 +21,10 @@ multiset.induction_on s.1 (let ⟨z⟩ := hι in ⟨z, λ _, false.elim⟩) $
   (λ h, h.symm ▸ h₁)
   (λ h, trans (H _ h) h₂)⟩
 
+theorem finset.exists_le {α : Type u} [nonempty α] [directed_order α] (s : finset α) :
+  ∃ M, ∀ i ∈ s, i ≤ M :=
+directed.finset_le (by apply_instance) directed_order.directed s
+
 namespace finset
 variables {s s₁ s₂ : finset α} {a : α} {f g : α → β}
 

src/algebra/module.lean

@@ -390,3 +390,11 @@ instance : module ℤ M :=
   smul_zero := gsmul_zero }
 
 end add_comm_group
+
+def is_add_group_hom.to_linear_map [add_comm_group α] [add_comm_group β]
+  (f : α → β) [is_add_group_hom f] : α →ₗ[ℤ] β :=
+{ to_fun := f,
+  add := is_add_group_hom.map_add f,
+  smul := λ i x, int.induction_on i (by rw [zero_smul, zero_smul, is_add_group_hom.map_zero f])
+    (λ i ih, by rw [add_smul, add_smul, is_add_group_hom.map_add f, ih, one_smul, one_smul])
+    (λ i ih, by rw [sub_smul, sub_smul, is_add_group_hom.map_sub f, ih, one_smul, one_smul]) }

src/data/dfinsupp.lean

@@ -559,6 +559,13 @@ support_zip_with
   support (-f) = support f :=
 by ext i; simp
 
+local attribute [instance] dfinsupp.to_module
+
+lemma support_smul {γ : Type w} [ring γ] [Π i, add_comm_group (β i)] [Π i, module γ (β i)]
+  [Π (i : ι), decidable_pred (eq (0 : β i))]
+  {b : γ} {v : Π₀ i, β i} : (b • v).support ⊆ v.support :=
+λ x, by simp [dfinsupp.mem_support_iff, not_imp_not] {contextual := tt}
+
 instance [decidable_eq ι] [Π i, has_zero (β i)] [Π i, decidable_eq (β i)] : decidable_eq (Π₀ i, β i) :=
 assume f g, decidable_of_iff (f.support = g.support ∧ (∀i∈f.support, f i = g i))
   ⟨assume ⟨h₁, h₂⟩, ext $ assume i,

src/data/polynomial.lean

@@ -116,6 +116,9 @@ instance C.is_semiring_hom : is_semiring_hom (C : α → polynomial α) :=
 
 @[simp] lemma C_pow : C (a ^ n) = C a ^ n := is_semiring_hom.map_pow _ _ _
 
+lemma nat_cast_eq_C (n : ℕ) : (n : polynomial α) = C n :=
+by refine (nat.eq_cast (λ n, C (n : α)) _ _ _ n).symm; simp
+
 section coeff
 
 lemma apply_eq_coeff : p n = coeff p n := rfl
@@ -518,6 +521,9 @@ end
 
 @[simp] lemma nat_degree_one : nat_degree (1 : polynomial α) = 0 := nat_degree_C 1
 
+@[simp] lemma nat_degree_nat_cast (n : ℕ) : nat_degree (n : polynomial α) = 0 :=
+by simp [nat_cast_eq_C]
+
 @[simp] lemma degree_monomial (n : ℕ) (ha : a ≠ 0) : degree (C a * X ^ n) = n :=
 by rw [← single_eq_C_mul_X, degree, support_single_ne_zero ha]; refl
 
@@ -1141,6 +1147,9 @@ variable {α}
 
 instance C.is_ring_hom : is_ring_hom (@C α _ _) := by apply is_ring_hom.of_semiring
 
+lemma int_cast_eq_C (n : ℤ) : (n : polynomial α) = C n :=
+congr_fun (int.eq_cast' _).symm n
+
 @[simp] lemma C_neg : C (-a) = -C a := is_ring_hom.map_neg C
 
 @[simp] lemma C_sub : C (a - b) = C a - C b := is_ring_hom.map_sub C
@@ -1164,6 +1173,9 @@ eval₂.is_ring_hom (C ∘ f)
 @[simp] lemma degree_neg (p : polynomial α) : degree (-p) = degree p :=
 by unfold degree; rw support_neg
 
+@[simp] lemma nat_degree_int_cast (n : ℤ) : nat_degree (n : polynomial α) = 0 :=
+by simp [int_cast_eq_C]
+
 @[simp] lemma coeff_neg (p : polynomial α) (n : ℕ) : coeff (-p) n = -coeff p n := rfl
 
 @[simp] lemma coeff_sub (p q : polynomial α) (n : ℕ) : coeff (p - q) n = coeff p n - coeff q n := rfl

src/linear_algebra/direct_sum_module.lean

@@ -11,7 +11,7 @@ import linear_algebra.basic
 
 universes u v w u₁
 
-variables (R : Type u) [comm_ring R]
+variables (R : Type u) [ring R]
 variables (ι : Type v) [decidable_eq ι] (β : ι → Type w)
 variables [Π i, add_comm_group (β i)] [Π i, module R (β i)]
 include R
@@ -28,7 +28,10 @@ dfinsupp.lmk β R
 
 def lof : Π i : ι, β i →ₗ[R] direct_sum ι β :=
 dfinsupp.lsingle β R
-variables {R ι β}
+variables {ι β}
+
+lemma single_eq_lof (i : ι) (b : β i) :
+  dfinsupp.single i b = lof R ι β i b := rfl
 
 theorem mk_smul (s : finset ι) (c : R) (x) : mk β s (c • x) = c • mk β s x :=
 (lmk R ι β s).map_smul c x
@@ -39,15 +42,15 @@ theorem of_smul (i : ι) (c : R) (x) : of β i (c • x) = c • of β i x :=
 variables {γ : Type u₁} [add_comm_group γ] [module R γ]
 variables (φ : Π i, β i →ₗ[R] γ)
 
-variables (R ι γ φ)
+variables (ι γ φ)
 def to_module : direct_sum ι β →ₗ[R] γ :=
 { to_fun := to_group (λ i, φ i),
   add := to_group_add _,
   smul := λ c x, direct_sum.induction_on x
     (by rw [smul_zero, to_group_zero, smul_zero])
     (λ i x, by rw [← of_smul, to_group_of, to_group_of, (φ i).map_smul c x])
     (λ x y ihx ihy, by rw [smul_add, to_group_add, ihx, ihy, to_group_add, smul_add]) }
-variables {R ι γ φ}
+variables {ι γ φ}
 
 @[simp] lemma to_module_lof (i) (x : β i) : to_module R ι γ φ (lof R ι β i x) = φ i x :=
 to_group_of (λ i, φ i) i x
@@ -61,7 +64,7 @@ variables {ψ} {ψ' : direct_sum ι β →ₗ[R] γ}
 
 theorem to_module.ext (H : ∀ i, ψ.comp (lof R ι β i) = ψ'.comp (lof R ι β i)) (f : direct_sum ι β) :
   ψ f = ψ' f :=
-by rw [to_module.unique ψ, to_module.unique ψ', funext H]
+by rw [to_module.unique R ψ, to_module.unique R ψ', funext H]
 
 def lset_to_set (S T : set ι) (H : S ⊆ T) :
   direct_sum S (β ∘ subtype.val) →ₗ direct_sum T (β ∘ subtype.val) :=
@@ -72,4 +75,34 @@ protected def lid (M : Type v) [add_comm_group M] [module R M] :
 { .. direct_sum.id M,
   .. to_module R punit M (λ i, linear_map.id) }
 
+variables (ι β)
+def component (i : ι) : direct_sum ι β →ₗ[R] β i :=
+{ to_fun := λ f, f i,
+  add := λ _ _, dfinsupp.add_apply,
+  smul := λ _ _, dfinsupp.smul_apply }
+
+variables {ι β}
+@[simp] lemma lof_apply (i : ι) (b : β i) : ((lof R ι β i) b) i = b :=
+by rw [lof, dfinsupp.lsingle_apply, dfinsupp.single_apply, dif_pos rfl]
+
+lemma apply_eq_component (f : direct_sum ι β) (i : ι) :
+  f i = component R ι β i f := rfl
+
+@[simp] lemma component.lof_self (i : ι) (b : β i) :
+  component R ι β i ((lof R ι β i) b) = b :=
+lof_apply R i b
+
+lemma component.of (i j : ι) (b : β j) :
+  component R ι β i ((lof R ι β j) b) =
+  if h : j = i then eq.rec_on h b else 0 :=
+dfinsupp.single_apply
+
+@[extensionality] lemma ext {f g : direct_sum ι β}
+  (h : ∀ i, component R ι β i f = component R ι β i g) : f = g :=
+dfinsupp.ext h
+
+lemma ext_iff {f g : direct_sum ι β} : f = g ↔
+  ∀ i, component R ι β i f = component R ι β i g :=
+⟨λ h _, by rw h, ext R⟩
+
 end direct_sum

src/linear_algebra/tensor_product.lean

@@ -410,10 +410,10 @@ begin
     (lift $ direct_sum.to_module R _ _ $ λ i₁, flip $ direct_sum.to_module R _ _ $ λ i₂,
       flip $ curry $ direct_sum.lof R (ι₁ × ι₂) (λ i, β₁ i.1 ⊗[R] β₂ i.2) (i₁, i₂))
     (direct_sum.to_module R _ _ $ λ i, map (direct_sum.lof R _ _ _) (direct_sum.lof R _ _ _))
-    (linear_map.ext $ direct_sum.to_module.ext $ λ i, mk_compr₂_inj $
+    (linear_map.ext $ direct_sum.to_module.ext _ $ λ i, mk_compr₂_inj $
       linear_map.ext $ λ x₁, linear_map.ext $ λ x₂, _)
-    (mk_compr₂_inj $ linear_map.ext $ direct_sum.to_module.ext $ λ i₁, linear_map.ext $ λ x₁,
-      linear_map.ext $ direct_sum.to_module.ext $ λ i₂, linear_map.ext $ λ x₂, _);
+    (mk_compr₂_inj $ linear_map.ext $ direct_sum.to_module.ext _ $ λ i₁, linear_map.ext $ λ x₁,
+      linear_map.ext $ direct_sum.to_module.ext _ $ λ i₂, linear_map.ext $ λ x₂, _);
   repeat { rw compr₂_apply <|> rw comp_apply <|> rw id_apply <|> rw mk_apply <|>
     rw direct_sum.to_module_lof <|> rw map_tmul <|> rw lift.tmul <|> rw flip_apply <|>
     rw curry_apply },

src/order/basic.lean

@@ -537,3 +537,6 @@ theorem directed_comp {ι} (f : ι → β) (g : β → α) :
 theorem directed_mono {s : α → α → Prop} {ι} (f : ι → α)
   (H : ∀ a b, r a b → s a b) (h : directed r f) : directed s f :=
 λ a b, let ⟨c, h₁, h₂⟩ := h a b in ⟨c, H _ _ h₁, H _ _ h₂⟩
+
+class directed_order (α : Type u) extends preorder α :=
+(directed : ∀ i j : α, ∃ k, i ≤ k ∧ j ≤ k)

src/ring_theory/free_comm_ring.lean

@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2019 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Johan Commelin
+-/
+
 import group_theory.free_abelian_group data.equiv.algebra data.equiv.functor data.polynomial
 import ring_theory.ideal_operations ring_theory.free_ring
 
@@ -99,6 +105,100 @@ lift $ of ∘ f
 @[simp] lemma map_mul (x y) : map f (x * y) = map f x * map f y := lift_mul _ _ _
 @[simp] lemma map_pow (x) (n : ℕ) : map f (x ^ n) = (map f x) ^ n := lift_pow _ _ _
 
+def is_supported (x : free_comm_ring α) (s : set α) : Prop :=
+x ∈ ring.closure (of '' s)
+
+section is_supported
+variables {x y : free_comm_ring α} {s t : set α}
+
+theorem is_supported_upwards (hs : is_supported x s) (hst : s ⊆ t) :
+  is_supported x t :=
+ring.closure_mono (set.mono_image hst) hs
+
+theorem is_supported_add (hxs : is_supported x s) (hys : is_supported y s) :
+  is_supported (x + y) s :=
+is_add_submonoid.add_mem hxs hys
+
+theorem is_supported_neg (hxs : is_supported x s) :
+  is_supported (-x) s :=
+is_add_subgroup.neg_mem hxs
+
+theorem is_supported_sub (hxs : is_supported x s) (hys : is_supported y s) :
+  is_supported (x - y) s :=
+is_add_subgroup.sub_mem _ _ _ hxs hys
+
+theorem is_supported_mul (hxs : is_supported x s) (hys : is_supported y s) :
+  is_supported (x * y) s :=
+is_submonoid.mul_mem hxs hys
+
+theorem is_supported_zero : is_supported 0 s :=
+is_add_submonoid.zero_mem _
+
+theorem is_supported_one : is_supported 1 s :=
+is_submonoid.one_mem _
+
+theorem is_supported_int {i : ℤ} {s : set α} : is_supported ↑i s :=
+int.induction_on i is_supported_zero
+  (λ i hi, by rw [int.cast_add, int.cast_one]; exact is_supported_add hi is_supported_one)
+  (λ i hi, by rw [int.cast_sub, int.cast_one]; exact is_supported_sub hi is_supported_one)
+
+end is_supported
+
+def restriction (s : set α) [decidable_pred s] (x : free_comm_ring α) : free_comm_ring s :=
+lift (λ p, if H : p ∈ s then of ⟨p, H⟩ else 0) x
+
+section restriction
+variables (s : set α) [decidable_pred s] (x y : free_comm_ring α)
+@[simp] lemma restriction_of (p) : restriction s (of p) = if H : p ∈ s then of ⟨p, H⟩ else 0 := lift_of _ _
+@[simp] lemma restriction_zero : restriction s 0 = 0 := lift_zero _
+@[simp] lemma restriction_one : restriction s 1 = 1 := lift_one _
+@[simp] lemma restriction_add : restriction s (x + y) = restriction s x + restriction s y := lift_add _ _ _
+@[simp] lemma restriction_neg : restriction s (-x) = -restriction s x := lift_neg _ _
+@[simp] lemma restriction_sub : restriction s (x - y) = restriction s x - restriction s y := lift_sub _ _ _
+@[simp] lemma restriction_mul : restriction s (x * y) = restriction s x * restriction s y := lift_mul _ _ _
+end restriction
+
+theorem is_supported_of {p} {s : set α} : is_supported (of p) s ↔ p ∈ s :=
+suffices is_supported (of p) s → p ∈ s, from ⟨this, λ hps, ring.subset_closure ⟨p, hps, rfl⟩⟩,
+assume hps : is_supported (of p) s, begin
+  classical,
+  have : ∀ x, is_supported x s →
+    ∃ (n : ℤ), lift (λ a, if a ∈ s then (0 : polynomial ℤ) else polynomial.X) x = n,
+  { intros x hx, refine ring.in_closure.rec_on hx _ _ _ _,
+    { use 1, rw [lift_one], norm_cast },
+    { use -1, rw [lift_neg, lift_one], norm_cast },
+    { rintros _ ⟨z, hzs, rfl⟩ _ _, use 0, rw [lift_mul, lift_of, if_pos hzs, zero_mul], norm_cast },
+    { rintros x y ⟨q, hq⟩ ⟨r, hr⟩, refine ⟨q+r, _⟩, rw [lift_add, hq, hr], norm_cast } },
+  specialize this (of p) hps, rw [lift_of] at this, split_ifs at this, { exact h },
+  exfalso, apply int.zero_ne_one,
+  rcases this with ⟨w, H⟩, rw polynomial.int_cast_eq_C at H,
+  exact congr_arg (λ (f : polynomial ℤ), f.coeff 1) H.symm
+end
+
+theorem map_subtype_val_restriction {x} (s : set α) [decidable_pred s] (hxs : is_supported x s) :
+  map subtype.val (restriction s x) = x :=
+begin
+  refine ring.in_closure.rec_on hxs _ _ _ _,
+  { rw restriction_one, refl },
+  { rw [restriction_neg, map_neg, restriction_one], refl },
+  { rintros _ ⟨p, hps, rfl⟩ n ih, rw [restriction_mul, restriction_of, dif_pos hps, map_mul, map_of, ih] },
+  { intros x y ihx ihy, rw [restriction_add, map_add, ihx, ihy] }
+end
+
+theorem exists_finite_support (x : free_comm_ring α) : ∃ s : set α, set.finite s ∧ is_supported x s :=
+free_comm_ring.induction_on x
+  ⟨∅, set.finite_empty, is_supported_neg is_supported_one⟩
+  (λ p, ⟨{p}, set.finite_singleton p, is_supported_of.2 $ finset.mem_singleton_self _⟩)
+  (λ x y ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩, ⟨s ∪ t, set.finite_union hfs hft, is_supported_add
+    (is_supported_upwards hxs $ set.subset_union_left s t)
+    (is_supported_upwards hxt $ set.subset_union_right s t)⟩)
+  (λ x y ⟨s, hfs, hxs⟩ ⟨t, hft, hxt⟩, ⟨s ∪ t, set.finite_union hfs hft, is_supported_mul
+    (is_supported_upwards hxs $ set.subset_union_left s t)
+    (is_supported_upwards hxt $ set.subset_union_right s t)⟩)
+
+theorem exists_finset_support (x : free_comm_ring α) : ∃ s : finset α, is_supported x ↑s :=
+let ⟨s, hfs, hxs⟩ := exists_finite_support x in ⟨hfs.to_finset, by rwa finset.coe_to_finset⟩
+
 end free_comm_ring
 
 

src/ring_theory/free_ring.lean

@@ -1,3 +1,9 @@
+/-
+Copyright (c) 2019 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau, Johan Commelin
+-/
+
 import group_theory.free_abelian_group data.equiv.algebra data.polynomial
 
 universes u v