refactor(linear_algebra, ring_theory): rework submodules; move them t…

…o linear_algebra

data/set/basic.lean

@@ -6,6 +6,40 @@ Author: Jeremy Avigad, Leonardo de Moura
 import tactic.ext tactic.finish data.subtype tactic.interactive
 open function
 
+
+/- set coercion to a type -/
+namespace set
+instance {α : Type*} : has_coe_to_sort (set α) := ⟨_, λ s, {x // x ∈ s}⟩
+end set
+
+section set_coe
+universe u
+variables {α : Type u}
+@[simp] theorem set.set_coe_eq_subtype (s : set α) :
+  coe_sort.{(u+1) (u+2)} s = {x // x ∈ s} := rfl
+
+@[simp] theorem set_coe.forall {s : set α} {p : s → Prop} :
+  (∀ x : s, p x) ↔ (∀ x (h : x ∈ s), p ⟨x, h⟩) :=
+subtype.forall
+
+@[simp] theorem set_coe.exists {s : set α} {p : s → Prop} :
+  (∃ x : s, p x) ↔ (∃ x (h : x ∈ s), p ⟨x, h⟩) :=
+subtype.exists
+
+@[simp] theorem set_coe_cast : ∀ {s t : set α} (H' : s = t) (H : @eq (Type u) s t) (x : s),
+  cast H x = ⟨x.1, H' ▸ x.2⟩
+| s _ rfl _ ⟨x, h⟩ := rfl
+
+theorem set_coe.ext {s : set α} {a b : s} : (↑a : α) = ↑b → a = b :=
+subtype.eq
+
+theorem set_coe.ext_iff {s : set α} {a b : s} : (↑a : α) = ↑b ↔ a = b :=
+iff.intro set_coe.ext (assume h, h ▸ rfl)
+
+end set_coe
+
+lemma subtype.mem {α : Type*} {s : set α} (p : s) : (p : α) ∈ s := p.property
+
 namespace set
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {ι : Sort x} {a : α} {s t : set α}
@@ -38,24 +72,6 @@ instance decidable_set_of (p : α → Prop) [H : decidable_pred p] : decidable_p
 
 @[simp] theorem set_of_subset_set_of {p q : α → Prop} : {a | p a} ⊆ {a | q a} ↔ (∀a, p a → q a) := iff.rfl
 
-/- set coercion to a type -/
-
-instance : has_coe_to_sort (set α) := ⟨_, λ s, {x // x ∈ s}⟩
-
-@[simp] theorem set_coe_eq_subtype (s : set α) : coe_sort.{(u+1) (u+2)} s = {x // x ∈ s} := rfl
-
-@[simp] theorem set_coe.forall {s : set α} {p : s → Prop} :
-  (∀ x : s, p x) ↔ (∀ x (h : x ∈ s), p ⟨x, h⟩) :=
-subtype.forall
-
-@[simp] theorem set_coe.exists {s : set α} {p : s → Prop} :
-  (∃ x : s, p x) ↔ (∃ x (h : x ∈ s), p ⟨x, h⟩) :=
-subtype.exists
-
-@[simp] theorem set_coe_cast : ∀ {s t : set α} (H' : s = t) (H : @eq (Type u) s t) (x : s),
-  cast H x = ⟨x.1, H' ▸ x.2⟩
-| s _ rfl _ ⟨x, h⟩ := rfl
-
 /- subset -/
 
 -- TODO(Jeremy): write a tactic to unfold specific instances of generic notation?
@@ -869,6 +885,14 @@ subset.antisymm
   (image_preimage_subset f s)
   (λ x hx, let ⟨y, e⟩ := h x in ⟨y, (e.symm ▸ hx : f y ∈ s), e⟩)
 
+lemma preimage_eq_preimage {f : β → α} (hf : surjective f) : f ⁻¹' s = preimage f t ↔ s = t :=
+iff.intro
+  (assume eq, by rw [← @image_preimage_eq β α f s hf, ← @image_preimage_eq β α f t hf, eq])
+  (assume eq, eq ▸ rfl)
+
+lemma surjective_preimage {f : β → α} (hf : surjective f) : injective (preimage f) :=
+assume s t, (preimage_eq_preimage hf).1
+
 theorem compl_image : image (@compl α) = preimage compl :=
 image_eq_preimage_of_inverse compl_compl compl_compl
 
@@ -897,6 +921,20 @@ set.ext $ assume a,
 lemma preimage_subset_iff {A : set α} {B : set β} {f : α → β} :
   f⁻¹' B ⊆ A ↔ (∀ a : α, f a ∈ B → a ∈ A) := iff.rfl
 
+lemma image_eq_image {f : α → β} (hf : injective f) : f '' s = f '' t ↔ s = t :=
+iff.symm $ iff.intro (assume eq, eq ▸ rfl) $ assume eq,
+  by rw [← preimage_image_eq s hf, ← preimage_image_eq t hf, eq]
+
+lemma image_subset_image_iff {f : α → β} (hf : injective f) : f '' s ⊆ f '' t ↔ s ⊆ t :=
+begin
+  refine (iff.symm $ iff.intro (image_subset f) $ assume h, _),
+  rw [← preimage_image_eq s hf, ← preimage_image_eq t hf],
+  exact preimage_mono h
+end
+
+lemma injective_image {f : α → β} (hf : injective f) : injective (('') f) :=
+assume s t, (image_eq_image hf).1
+
 end image
 
 theorem univ_eq_true_false : univ = ({true, false} : set Prop) :=

linear_algebra/linear_map_module.lean

@@ -15,14 +15,6 @@ local attribute [instance] classical.prop_decidable
 universes u v w
 variables {α : Type u} {β : Type v} {γ : Type w}
 
-namespace classical
-
-lemma some_spec2 {α : Type u} {p : α → Prop} {h : ∃a, p a} (q : α → Prop) (hpq : ∀a, p a → q a) :
-  q (some h) :=
-hpq _ $ some_spec _
-
-end classical
-
 /-- The type of linear maps `β → γ` between α-modules β and γ -/
 def linear_map {α : Type u} (β : Type v) (γ : Type w) [ring α] [module α β] [module α γ] :=
 subtype (@is_linear_map α β γ _ _ _)
@@ -122,21 +114,21 @@ iff.intro
 
 /-- second isomorphism law -/
 def union_quotient_equiv_quotient_inter {s t : set β} [is_submodule s] [is_submodule t] :
-  quotient s (subtype.val ⁻¹' (s ∩ t)) ≃ₗ quotient (span (s ∪ t)) (subtype.val ⁻¹' t) :=
-let sel₁ : s → span (s ∪ t) := λb, ⟨b.1, subset_span $ or.inl b.2⟩ in
-have sel₁_val : ∀b:s, (sel₁ b).1 = b.1, from assume b, rfl,
+  quotient s ((coe : s → β) ⁻¹' (s ∩ t)) ≃ₗ quotient (span (s ∪ t)) ((coe : span (s ∪ t) → β) ⁻¹' t) :=
+let sel₁ : s → span (s ∪ t) := λb, ⟨(b : β), subset_span $ or.inl b.2⟩ in
+have sel₁_val : ∀b:s, (sel₁ b : β) = b, from assume b, rfl,
 have ∀b'∈span (s ∪ t), ∃x:s, ∃y∈t, b' = x.1 + y,
   by simp [span_union, span_eq_of_is_submodule, _inst_4, _inst_5] {contextual := tt},
 let sel₂ : span (s ∪ t) → s := λb', classical.some (this b'.1 b'.2) in
-have sel₂_spec : ∀b':span (s ∪ t), ∃y∈t, b'.1 = (sel₂ b').1 + y,
+have sel₂_spec : ∀b':span (s ∪ t), ∃y∈t, (b' : β) = (sel₂ b' : β) + y,
   from assume b', classical.some_spec (this b'.1 b'.2),
 { to_fun :=
   begin
     intro b,
     fapply quotient.lift_on' b,
     { intro b', exact sel₁ b' },
     { assume b₁ b₂ h,
-      change b₁ - b₂ ∈ subtype.val ⁻¹' (s ∩ t) at h,
+      change b₁ - b₂ ∈ coe ⁻¹' (s ∩ t) at h,
       apply quotient_module.eq.2, simp * at * }
   end,
   inv_fun :=
@@ -148,11 +140,11 @@ have sel₂_spec : ∀b':span (s ∪ t), ∃y∈t, b'.1 = (sel₂ b').1 + y,
       change b₁ - b₂ ∈ _ at h,
       rcases (sel₂_spec b₁) with ⟨c₁, hc₁, eq_c₁⟩,
       rcases (sel₂_spec b₂) with ⟨c₂, hc₂, eq_c₂⟩,
-      have : ((sel₂ b₁).1 - (sel₂ b₂).1) + (c₁ - c₂) ∈ t,
+      have : ((sel₂ b₁ : β) - (sel₂ b₂ : β)) + (c₁ - c₂) ∈ t,
       { simpa [eq_c₁, eq_c₂, add_comm, add_left_comm, add_assoc] using h, },
-      have ht : (sel₂ b₁).1 - (sel₂ b₂).1 ∈ t,
+      have ht : (sel₂ b₁ : β) - (sel₂ b₂ : β) ∈ t,
       { rwa [is_submodule.add_left_iff (is_submodule.sub hc₁ hc₂)] at this },
-      have hs : (sel₂ b₁).1 - (sel₂ b₂).1 ∈ s,
+      have hs : (sel₂ b₁ : β) - (sel₂ b₂ : β) ∈ s,
       { from is_submodule.sub (sel₂ b₁).2 (sel₂ b₂).2 },
       apply quotient_module.eq.2,
       simp * at * }
@@ -166,16 +158,16 @@ have sel₂_spec : ∀b':span (s ∪ t), ∃y∈t, b'.1 = (sel₂ b').1 + y,
   left_inv := assume b', @quotient.induction_on _ (quotient_rel _) _ b'
   begin
     intro b, apply quotient_module.eq.2,
-    rcases (sel₂_spec (sel₁ b)) with ⟨c, hc, eq⟩,
-    have b_eq : b.1 = c + (sel₂ (sel₁ b)).1,
+    rcases (sel₂_spec (sel₁ b)) with ⟨c, hct, eq⟩,
+    have b_eq : (b : β) = c + (sel₂ (sel₁ b)),
     { simpa [sel₁_val] using eq },
-    have : b.1 ∈ s, from b.2,
+    have : (b : β) ∈ s, from b.2,
     have hcs : c ∈ s,
-    { rwa [b_eq, is_submodule.add_left_iff (sel₂ (sel₁ b)).2] at this },
-    show (sel₂ (sel₁ b) - b).1 ∈ s ∩ t, { simp [eq, hc, hcs, is_submodule.neg_iff] }
+    { rwa [b_eq, is_submodule.add_left_iff (sel₂ (sel₁ b)).mem] at this },
+    show (sel₂ (sel₁ b) - b : β) ∈ s ∩ t, { simp [b_eq, hct, hcs, is_submodule.neg_iff] }
   end,
   linear_fun :=  is_linear_map_quotient_lift _ $ (is_linear_map_quotient_mk _).comp $
-    is_linear_map_subtype_mk _ (is_linear_map_subtype_val is_linear_map.id) _ }
+    is_linear_map_subtype_mk _ (is_submodule.is_linear_map_coe s) _ }
 
 end
 

linear_algebra/quotient_module.lean

@@ -99,6 +99,9 @@ instance quotient.module : module α Q :=
 @[simp] lemma coe_smul (a : α) (b : β) : ((a • b : β) : Q) = a • b := rfl
 @[simp] lemma coe_add (a b : β) : ((a + b : β) : Q) = a + b := rfl
 
+lemma coe_eq_zero (b : β) : (b : quotient β s) = 0 ↔ b ∈ s :=
+by rw [← (coe_zero s), quotient_module.eq]; simp
+
 instance quotient.inhabited : inhabited Q := ⟨0⟩
 
 lemma is_linear_map_quotient_mk : @is_linear_map _ _ Q _ _ _ (λb, mk b : β → Q) :=