refactor(algebra/module): split of type constructions and move quotie…

…nt, subtype and linear_map to their own theories in algebra/linear_algebra

algebra/group.lean

@@ -133,8 +133,8 @@ attribute [to_additive neg_add] mul_inv
 
 end pending_1857
 
-universe variable u
-variable {α : Type u}
+universe u
+variables {α : Type u}
 
 @[simp, to_additive add_left_inj]
 theorem mul_left_inj [left_cancel_semigroup α] {a b c : α} : a * b = a * c ↔ b = c :=

algebra/linear_algebra/basic.lean

@@ -208,6 +208,46 @@ have l = 0,
 have l 0 = 1, from finsupp.single_eq_same,
 by rw [‹l = 0›] at this; simp * at *
 
+lemma linear_independent_union {s t : set β}
+  (hs : linear_independent s) (ht : linear_independent t) (hst : span s ∩ span t = {0}) :
+  linear_independent (s ∪ t) :=
+(zero_ne_one_or_forall_eq_0 α).elim
+  (assume ne l hl eq0,
+    let ls := l.filter $ λb, b ∈ s, lt := l.filter $ λb, b ∈ t in
+    have hls : ↑ls.support ⊆ s, by simp [ls, subset_def],
+    have hlt : ↑lt.support ⊆ t, by simp [ls, subset_def],
+    have lt.sum (λb a, a • b) ∈ span t,
+      from is_submodule.sum $ assume b hb, is_submodule.smul _ $ subset_span $ hlt hb,
+    have l = ls + lt,
+      from
+      have ∀b, b ∈ s → b ∉ t,
+        from assume b hbs hbt,
+        have b ∈ span s ∩ span t, from ⟨subset_span hbs, subset_span hbt⟩,
+        have b = 0, by rw [hst] at this; simp * at *,
+        zero_not_mem_of_linear_independent ne hs $ this ▸ hbs,
+      have lt = l.filter (λb, b ∉ s),
+        from finsupp.ext $ assume b, by by_cases b ∈ t; by_cases b ∈ s; simp * at *,
+      by rw [this]; exact finsupp.filter_pos_add_filter_neg.symm,
+    have ls.sum (λb a, a • b) + lt.sum (λb a, a • b) = l.sum (λb a, a • b),
+      by rw [this, finsupp.sum_add_index]; simp [add_smul],
+    have ls_eq_neg_lt : ls.sum (λb a, a • b) = - lt.sum (λb a, a • b),
+      from eq_of_sub_eq_zero $ by simp [this, eq0],
+    have ls_sum_eq : ls.sum (λb a, a • b) = 0,
+      from
+      have - lt.sum (λb a, a • b) ∈ span t,
+        from is_submodule.neg $ is_submodule.sum $
+          assume b hb, is_submodule.smul _ $ subset_span $ hlt hb,
+      have ls.sum (λb a, a • b) ∈ span s ∩ span t,
+        from ⟨is_submodule.sum $ assume b hb, is_submodule.smul _ $ subset_span $ hls hb,
+          ls_eq_neg_lt.symm ▸ this⟩,
+      by rw [hst] at this; simp * at *,
+    have ls = 0, from hs _ (finsupp.support_subset_iff.mp hls) ls_sum_eq,
+    have lt_sum_eq : lt.sum (λb a, a • b) = 0,
+      from eq_of_neg_eq_neg $ by rw [←ls_eq_neg_lt, ls_sum_eq]; simp,
+    have lt = 0, from ht _ (finsupp.support_subset_iff.mp hlt) lt_sum_eq,
+    by simp [‹l = ls + lt›, ‹ls = 0›, ‹lt = 0›])
+  (assume eq_0 l _ _, finsupp.ext $ assume b, eq_0 _)
+
 lemma linear_independent_Union_of_directed {s : set (set β)} (hs : ∀a∈s, ∀b∈s, ∃c∈s, a ∪ b ⊆ c)
   (h : ∀a∈s, linear_independent a) : linear_independent (⋃₀s) :=
 assume l hl eq,

algebra/linear_algebra/linear_map_module.lean

@@ -0,0 +1,124 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Kenny Lau
+
+Type of linear functions
+-/
+import algebra.linear_algebra.basic
+
+universes u v w
+variables {α : Type u} {β : Type v} {γ : Type w}
+
+
+def linear_map {α : Type u} (β : Type v) (γ : Type w) [ring α] [module α β] [module α γ] :=
+subtype (@is_linear_map α β γ _ _ _)
+
+namespace linear_map
+variables [ring α] [module α β] [module α γ]
+variables {r : α} {A B C : linear_map β γ} {x y : β}
+include α
+
+instance : has_coe_to_fun (linear_map β γ) := ⟨_, subtype.val⟩
+
+theorem ext (h : ∀ x, A x = B x) : A = B := subtype.eq $ funext h
+
+lemma is_linear_map_coe : is_linear_map A := A.property
+
+@[simp] lemma map_add  : A (x + y) = A x + A y := is_linear_map_coe.add x y
+@[simp] lemma map_smul : A (r • x) = r • A x := is_linear_map_coe.smul r x
+@[simp] lemma map_zero : A 0 = 0 := is_linear_map_coe.zero
+@[simp] lemma map_neg  : A (-x) = -A x := is_linear_map_coe.neg _
+@[simp] lemma map_sub  : A (x - y) = A x - A y := is_linear_map_coe.sub _ _
+
+/- kernel -/
+
+def ker (A : linear_map β γ) : set β := {y | A y = 0}
+
+section ker
+
+@[simp] lemma mem_ker : x ∈ A.ker ↔ A x = 0 := iff.rfl
+
+theorem ker_of_map_eq_map (h : A x = A y) : x - y ∈ A.ker :=
+by rw [mem_ker, map_sub]; exact sub_eq_zero_of_eq h
+
+theorem inj_of_trivial_ker (H : A.ker ⊆ {0}) (h : A x = A y) : x = y :=
+eq_of_sub_eq_zero $ set.eq_of_mem_singleton $ H $ ker_of_map_eq_map h
+
+variables (α A)
+
+instance ker.is_submodule : is_submodule A.ker :=
+{ zero_ := map_zero,
+  add_ := λ x y HU HV, by rw mem_ker at *; simp [HU, HV, mem_ker],
+  smul := λ r x HV, by rw mem_ker at *; simp [HV] }
+
+theorem sub_ker (HU : x ∈ A.ker) (HV : y ∈ A.ker) : x - y ∈ A.ker :=
+is_submodule.sub HU HV
+
+end ker
+
+/- image -/
+
+def im (A : linear_map β γ) : set γ := {x | ∃ y, A y = x}
+
+@[simp] lemma mem_im {A : linear_map β γ} {z : γ} :
+  z ∈ A.im ↔ ∃ y, A y = z := iff.rfl
+
+instance im.is_submodule : is_submodule A.im :=
+{ zero_ := ⟨0, map_zero⟩,
+  add_ := λ a b ⟨x, hx⟩ ⟨y, hy⟩, ⟨x + y, by simp [hx, hy]⟩,
+  smul := λ r a ⟨x, hx⟩, ⟨r • x, by simp [hx]⟩ }
+
+section add_comm_group
+
+instance : has_add (linear_map β γ) := ⟨λhf hg, ⟨_, hf.2.map_add hg.2⟩⟩
+instance : has_zero (linear_map β γ) := ⟨⟨_, is_linear_map.map_zero⟩⟩
+instance : has_neg (linear_map β γ) := ⟨λhf, ⟨_, hf.2.map_neg⟩⟩
+
+@[simp] lemma add_app : (A + B) x = A x + B x := rfl
+@[simp] lemma zero_app : (0 : linear_map β γ) x = 0 := rfl
+@[simp] lemma neg_app : (-A) x = -A x := rfl
+
+instance : add_comm_group (linear_map β γ) :=
+by refine {add := (+), zero := 0, neg := has_neg.neg, ..}; { intros, apply ext, simp }
+
+end add_comm_group
+
+end linear_map
+
+namespace linear_map
+variables [comm_ring α] [module α β] [module α γ]
+
+instance : has_scalar α (linear_map β γ) := ⟨λr f, ⟨λb, r • f b, f.2.map_smul_right⟩⟩
+
+@[simp] lemma smul_app {r : α} {x : β} {A : linear_map β γ} : (r • A) x = r • (A x) := rfl
+
+variables (α β γ)
+
+instance : module α (linear_map β γ) :=
+by refine {smul := (•), ..linear_map.add_comm_group, ..};
+  { intros, apply ext, simp [smul_add, add_smul, mul_smul] }
+
+end linear_map
+
+namespace module
+variables [ring α] [module α β]
+include α
+
+instance : has_one (linear_map β β) := ⟨⟨id, is_linear_map.id⟩⟩
+instance : has_mul (linear_map β β) := ⟨λf g, ⟨_, is_linear_map.comp f.2 g.2⟩⟩
+
+@[simp] lemma one_app (x : β) : (1 : linear_map β β) x = x := rfl
+@[simp] lemma mul_app (A B : linear_map β β) (x : β) : (A * B) x = A (B x) := rfl
+
+variables (α β)
+
+-- declaring this an instance breaks `real.lean` with reaching max. instance resolution depth
+def endomorphism_ring : ring (linear_map β β) :=
+by refine {mul := (*), one := 1, ..linear_map.add_comm_group, ..};
+  { intros, apply linear_map.ext, simp }
+
+def general_linear_group :=
+@units (linear_map β β) (@ring.to_semiring _ (endomorphism_ring α β))
+
+end module

algebra/linear_algebra/quotient_module.lean

@@ -0,0 +1,103 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Johannes Hölzl
+
+Quotient construction on modules
+-/
+
+import algebra.linear_algebra.basic
+
+namespace is_submodule
+
+universes u v w
+variables {α : Type u} {β : Type v} {γ : Type w}
+variables [ring α] [module α β] [module α γ] (s : set β) [hs : is_submodule s]
+include α s hs
+
+open function
+
+def quotient_rel : setoid β :=
+⟨λb₁ b₂, b₁ - b₂ ∈ s,
+  assume b, by simp [zero],
+  assume b₁ b₂ hb,
+  have - (b₁ - b₂) ∈ s, from is_submodule.neg hb,
+  by simpa using this,
+  assume b₁ b₂ b₃ hb₁₂ hb₂₃,
+  have (b₁ - b₂) + (b₂ - b₃) ∈ s, from add hb₁₂ hb₂₃,
+  by simpa using this⟩
+
+local attribute [instance] quotient_rel
+
+def quotient : Type v := quotient (quotient_rel s)
+
+local notation ` Q ` := quotient s
+
+instance quotient.has_zero : has_zero Q := ⟨⟦ 0 ⟧⟩
+
+instance quotient.has_add : has_add Q :=
+⟨λa b, quotient.lift_on₂ a b (λa b, ⟦a + b⟧) $
+  assume a₁ a₂ b₁ b₂ (h₁ : a₁ - b₁ ∈ s) (h₂ : a₂ - b₂ ∈ s),
+  quotient.sound $
+  have (a₁ - b₁) + (a₂ - b₂) ∈ s, from add h₁ h₂,
+  show (a₁ + a₂) - (b₁ + b₂) ∈ s, by simpa⟩
+
+instance quotient.has_neg : has_neg Q :=
+⟨λa, quotient.lift_on a (λa, ⟦- a⟧) $ assume a b (h : a - b ∈ s),
+  quotient.sound $
+  have - (a - b) ∈ s, from neg h,
+  show (-a) - (-b) ∈ s, by simpa⟩
+
+instance quotient.has_scalar : has_scalar α Q :=
+⟨λa b, quotient.lift_on b (λb, ⟦a • b⟧) $ assume b₁ b₂ (h : b₁ - b₂ ∈ s),
+  quotient.sound $
+  have a • (b₁ - b₂) ∈ s, from is_submodule.smul a h,
+  show a • b₁ - a • b₂ ∈ s, by simpa [smul_add]⟩
+
+instance quotient.module : module α Q :=
+{ module .
+  zero := 0,
+  add  := (+),
+  neg  := has_neg.neg,
+  smul := (•),
+  add_assoc    := assume a b c, quotient.induction_on₃ a b c $ assume a b c, quotient.sound $
+    by simp,
+  add_comm     := assume a b, quotient.induction_on₂ a b $ assume a b, quotient.sound $
+    by simp,
+  add_zero     := assume a, quotient.induction_on a $ assume a, quotient.sound $
+    by simp,
+  zero_add     := assume a, quotient.induction_on a $ assume a, quotient.sound $
+    by simp,
+  add_left_neg := assume a, quotient.induction_on a $ assume a, quotient.sound $
+    by simp,
+  one_smul     := assume a, quotient.induction_on a $ assume a, quotient.sound $
+    by simp,
+  mul_smul     := assume a b c, quotient.induction_on c $ assume c, quotient.sound $
+    by simp [mul_smul],
+  smul_add     := assume a b c, quotient.induction_on₂ b c $ assume b c, quotient.sound $
+    by simp [smul_add],
+  add_smul     := assume a b c, quotient.induction_on c $ assume c, quotient.sound $
+    by simp [add_smul] }
+
+instance quotient.inhabited : inhabited Q := ⟨0⟩
+
+lemma is_linear_map_quotient_mk : @is_linear_map _ _ Q _ _ _ (λb, ⟦b⟧ : β → Q) :=
+by refine {..}; intros; refl
+
+def quotient.lift {f : β → γ} (hf : is_linear_map f) (h : ∀x∈s, f x = 0) (b : Q) : γ :=
+b.lift_on f $ assume a b (hab : a - b ∈ s),
+  have f a - f b = 0, by rw [←hf.sub]; exact h _ hab,
+  show f a = f b, from eq_of_sub_eq_zero this
+
+lemma is_linear_map_quotient_lift {f : β → γ} {h : ∀x y, x - y ∈ s → f x = f y}
+  (hf : is_linear_map f) : is_linear_map (λq:Q, quotient.lift_on q f h) :=
+⟨assume b₁ b₂, quotient.induction_on₂ b₁ b₂ $ assume b₁ b₂, hf.add b₁ b₂,
+  assume a b, quotient.induction_on b $ assume b, hf.smul a b⟩
+
+lemma quotient.injective_lift [is_submodule s] {f : β → γ} (hf : is_linear_map f)
+  (hs : s = {x | f x = 0}) : injective (quotient.lift s hf $ le_of_eq hs) :=
+assume a b, quotient.induction_on₂ a b $ assume a b (h : f a = f b), quotient.sound $
+  have f (a - b) = 0, by rw [hf.sub]; simp [h],
+  show a - b ∈ s, from hs.symm ▸ this
+
+end is_submodule

algebra/linear_algebra/subtype_module.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2017 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl, Kenny Lau
+
+Subtype construction of sub modules.
+-/
+import algebra.linear_algebra.basic
+
+universes u v w
+variables {α : Type u} {β : Type v} {γ : Type w}
+variables [ring α] [module α β] [module α γ] {p : set β} [is_submodule p]
+variables {r : α} {x y : {x : β // x ∈ p}}
+include α
+
+open is_submodule
+
+instance : has_add {x : β // x ∈ p} := ⟨λ ⟨x, px⟩ ⟨y, py⟩, ⟨x + y, add px py⟩⟩
+instance : has_zero {x : β // x ∈ p} := ⟨⟨0, zero⟩⟩
+instance : has_neg {x : β // x ∈ p} := ⟨λ ⟨x, hx⟩, ⟨-x, neg hx⟩⟩
+instance : has_scalar α {x : β // x ∈ p} := ⟨λ c ⟨x, hx⟩, ⟨c • x, smul c hx⟩⟩
+
+@[simp] lemma add_val : (x + y).val = x.val + y.val := by cases x; cases y; refl
+@[simp] lemma zero_val : (0 : {x : β // x ∈ p}).val = 0 := rfl
+@[simp] lemma neg_val : (-x).val = -x.val := by cases x; refl
+@[simp] lemma smul_val : (r • x).val = r • x.val := by cases x; refl
+
+instance : module α {x : β // x ∈ p} :=
+by refine {add := (+), zero := 0, neg := has_neg.neg, smul := (•), ..};
+  { intros, apply subtype.eq,
+    simp [smul_add, add_smul, mul_smul] }
+
+lemma sub_val : (x - y).val = x.val - y.val := by simp
+
+lemma is_linear_map_subtype_val {f : γ → {x : β // x ∈ p}} (hf : is_linear_map f) :
+  is_linear_map (λb, (f b).val) :=
+by refine {..}; simp [hf.add, hf.smul]
+
+lemma is_linear_map_subtype_mk {f : γ → β} (hf : is_linear_map f) {h : ∀c, f c ∈ p} :
+  is_linear_map (λc, ⟨f c, h c⟩ : γ → {x : β // x ∈ p}) :=
+by refine {..}; intros; apply subtype.eq; simp [hf.add, hf.smul]