feat(linear_algebra): add module (vector_space) structure for functio…

…n spaces

src/linear_algebra/basic.lean

@@ -56,6 +56,14 @@ by refine {to_fun := λc, ⟨f c, h c⟩, ..}; intros; apply set_coe.ext; simp
 @[simp] theorem cod_restrict_apply (p : submodule α β) (f : γ →ₗ[α] β) {h} (x : γ) :
   (cod_restrict p f h x : β) = f x := rfl
 
+@[simp] lemma comp_cod_restrict (p : submodule α γ) (h : ∀b, f b ∈ p) (g : δ →ₗ[α] β) :
+  (cod_restrict p f h).comp g = cod_restrict p (f.comp g) (assume b, h _) :=
+ext $ assume b, rfl
+
+@[simp] lemma subtype_comp_cod_restrict (p : submodule α γ) (h : ∀b, f b ∈ p) :
+  p.subtype.comp (cod_restrict p f h) = f :=
+ext $ assume b, rfl
+
 def inverse (g : γ → β) (h₁ : left_inverse g f) (h₂ : right_inverse g f) : γ →ₗ[α] β :=
 by dsimp [left_inverse, function.right_inverse] at h₁ h₂; exact
 ⟨g, λ x y, by rw [← h₁ (g (x + y)), ← h₁ (g x + g y)]; simp [h₂],
@@ -430,6 +438,9 @@ le_antisymm
 lemma map_comap_subtype : map p.subtype (comap p.subtype p') = p ⊓ p' :=
 ext $ λ x, ⟨by rintro ⟨⟨_, h₁⟩, h₂, rfl⟩; exact ⟨h₁, h₂⟩, λ ⟨h₁, h₂⟩, ⟨⟨_, h₁⟩, h₂, rfl⟩⟩
 
+lemma eq_zero_of_bot_submodule : ∀(b : (⊥ : submodule α β)), b = 0
+| ⟨b', hb⟩ := subtype.eq $ show b' = 0, from (mem_bot α).1 hb
+
 section
 variables (α)
 def span (s : set β) : submodule α β := Inf {p | s ⊆ p}
@@ -472,6 +483,9 @@ end
 @[simp] lemma span_empty : span α (∅ : set β) = ⊥ :=
 (submodule.gi α β).gc.l_bot
 
+@[simp] lemma span_univ : span α (univ : set β) = ⊤ :=
+eq_top_iff.2 $ le_def.2 $ subset_span
+
 lemma span_union (s t : set β) : span α (s ∪ t) = span α s ⊔ span α t :=
 (submodule.gi α β).gc.l_sup
 
@@ -494,6 +508,11 @@ begin
   { simp [-mem_coe]; exact λ a x i hi, ⟨i, smul_mem _ a hi⟩ },
 end
 
+lemma mem_supr_of_mem {ι : Sort*} {b : β} (p : ι → submodule α β) (i : ι) (h : b ∈ p i) :
+  b ∈ (⨆i, p i) :=
+have p i ≤ (⨆i, p i) := le_supr p i,
+@this b h
+
 @[simp] theorem mem_supr_of_directed {ι} (hι : nonempty ι)
   (S : ι → submodule α β)
   (H : ∀ i j, ∃ k, S i ≤ S k ∧ S j ≤ S k) {x} :
@@ -922,6 +941,10 @@ by rw [of_le, ker_cod_restrict, ker_subtype]
 lemma range_of_le (p q : submodule α β) (h : p ≤ q) : (of_le h).range = comap q.subtype p :=
 by rw [← map_top, of_le, linear_map.map_cod_restrict, map_top, range_subtype]
 
+lemma disjoint_iff_comap_eq_bot (p q : submodule α β) :
+  disjoint p q ↔ comap p.subtype q = ⊥ :=
+by rw [eq_bot_iff, ← map_le_map_iff p.ker_subtype, map_bot, map_comap_subtype]; refl
+
 /-- If N ⊆ M then submodules of N are the same as submodules of M contained in N -/
 def map_subtype.order_iso :
   ((≤) : submodule α p → submodule α p → Prop) ≃o
@@ -1136,12 +1159,28 @@ def of_top (p : submodule α β) (h : p = ⊤) : p ≃ₗ[α] β :=
 @[simp] theorem of_top_symm_apply (p : submodule α β) {h} (x : β) :
   ↑((of_top p h).symm x) = x := rfl
 
+lemma eq_bot_of_equiv (p : submodule α β) (e : p ≃ₗ[α] (⊥ : submodule α γ)) :
+  p = ⊥ :=
+begin
+  refine bot_unique (submodule.le_def'.2 $ assume b hb, (submodule.mem_bot α).2 _),
+  have := e.symm_apply_apply ⟨b, hb⟩,
+  rw [← e.coe_apply, submodule.eq_zero_of_bot_submodule ((e : p →ₗ[α] (⊥ : submodule α γ)) ⟨b, hb⟩),
+    ← e.symm.coe_apply, linear_map.map_zero] at this,
+  exact congr_arg (coe : p → β) this.symm
+end
+
 end ring
 
 section comm_ring
 variables [comm_ring α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
 variables [module α β] [module α γ] [module α δ]
 include α
+open linear_map
+
+def smul_of_unit (a : units α) : β ≃ₗ[α] β :=
+of_linear ((a:α) • 1 : β →ₗ β) (((a⁻¹ : units α) : α) • 1 : β →ₗ β)
+  (by rw [smul_comp, comp_smul, smul_smul, units.mul_inv, one_smul]; refl)
+  (by rw [smul_comp, comp_smul, smul_smul, units.inv_mul, one_smul]; refl)
 
 def congr_right (f : γ ≃ₗ[α] δ) : (β →ₗ[α] γ) ≃ₗ (β →ₗ δ) :=
 of_linear
@@ -1152,8 +1191,27 @@ of_linear
 
 end comm_ring
 
+section field
+variables [field α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
+variables [module α β] [module α γ] [module α δ]
+variable (β)
+open linear_map
+
+def smul_of_ne_zero (a : α) (ha : a ≠ 0) : β ≃ₗ[α] β :=
+smul_of_unit $ units.mk0 a ha
+
+end field
+
 end linear_equiv
 
+namespace equiv
+variables [ring α] [add_comm_group β] [module α β] [add_comm_group γ] [module α γ]
+
+def to_linear_equiv (e : β ≃ γ) (h : is_linear_map α (e : β → γ)) : β ≃ₗ[α] γ :=
+{ add := h.add, smul := h.smul, .. e}
+
+end equiv
+
 namespace linear_map
 variables [ring α] [add_comm_group β] [add_comm_group γ] [add_comm_group δ]
 variables [module α β] [module α γ] [module α δ]
@@ -1199,4 +1257,190 @@ noncomputable def sup_quotient_equiv_quotient_inf (p p' : submodule α β) :
       change y - (y + z) ∈ p', rwa [sub_add_eq_sub_sub, sub_self, zero_sub, neg_mem_iff]
     end }
 
+section pi
+universe i
+variables {φ : ι → Type i}
+variables [∀i, add_comm_group (φ i)] [∀i, module α (φ i)]
+
+/-- `pi` construction for linear functions. From a family of linear functions it produces a linear
+function into a family of modules. -/
+def pi (f : Πi, γ →ₗ[α] φ i) : γ →ₗ[α] (Πi, φ i) :=
+⟨λc i, f i c,
+  assume c d, funext $ assume i, (f i).add _ _, assume c d, funext $ assume i, (f i).smul _ _⟩
+
+@[simp] lemma pi_apply (f : Πi, γ →ₗ[α] φ i) (c : γ) (i : ι) :
+  pi f c i = f i c := rfl
+
+lemma ker_pi (f : Πi, γ →ₗ[α] φ i) : ker (pi f) = (⨅i:ι, ker (f i)) :=
+by ext c; simp [funext_iff]; refl
+
+lemma pi_eq_zero (f : Πi, γ →ₗ[α] φ i) : pi f = 0 ↔ (∀i, f i = 0) :=
+by simp only [linear_map.ext_iff, pi_apply, funext_iff]; exact ⟨λh a b, h b a, λh a b, h b a⟩
+
+lemma pi_zero : pi (λi, 0 : Πi, γ →ₗ[α] φ i) = 0 :=
+by ext; refl
+
+lemma pi_comp (f : Πi, γ →ₗ[α] φ i) (g : δ →ₗ[α] γ) : (pi f).comp g = pi (λi, (f i).comp g) :=
+rfl
+
+/-- Linear projection -/
+def proj (i : ι) : (Πi, φ i) →ₗ[α] φ i :=
+⟨ λa, a i, assume f g, rfl, assume c f, rfl ⟩
+
+@[simp] lemma proj_apply (i : ι) (b : Πi, φ i) : (proj i : (Πi, φ i) →ₗ[α] φ i) b = b i := rfl
+
+lemma proj_pi (f : Πi, γ →ₗ[α] φ i) (i : ι) : (proj i).comp (pi f) = f i :=
+ext $ assume c, rfl
+
+lemma infi_ker_proj : (⨅i, ker (proj i) : submodule α (Πi, φ i)) = ⊥ :=
+bot_unique $ submodule.le_def'.2 $ assume a h,
+begin
+  simp only [mem_infi, mem_ker, proj_apply] at h,
+  exact (mem_bot _).2 (funext $ assume i, h i)
+end
+
+section
+variables (α φ)
+def infi_ker_proj_equiv {I J : set ι} [decidable_pred (λi, i ∈ I)]
+  (hd : disjoint I J) (hu : set.univ ⊆ I ∪ J) :
+  (⨅i ∈ J, ker (proj i) : submodule α (Πi, φ i)) ≃ₗ[α] (Πi:I, φ i) :=
+begin
+  refine linear_equiv.of_linear
+    (pi $ λi, (proj (i:ι)).comp (submodule.subtype _))
+    (cod_restrict _ (pi $ λi, if h : i ∈ I then proj (⟨i, h⟩ : I) else 0) _) _ _,
+  { assume b,
+    simp only [mem_infi, mem_ker, funext_iff, proj_apply, pi_apply],
+    assume j hjJ,
+    have : j ∉ I := assume hjI, hd ⟨hjI, hjJ⟩,
+    rw [dif_neg this, zero_apply] },
+  { simp only [pi_comp, comp_assoc, subtype_comp_cod_restrict, proj_pi, dif_pos, subtype.val_prop'],
+    ext b ⟨j, hj⟩, refl },
+  { ext ⟨b, hb⟩,
+    apply subtype.coe_ext.2,
+    ext j,
+    have hb : ∀i ∈ J, b i = 0,
+    { simpa only [mem_infi, mem_ker, proj_apply] using (mem_infi _).1 hb },
+    simp only [comp_apply, pi_apply, id_apply, proj_apply, subtype_apply, cod_restrict_apply],
+    split_ifs,
+    { rw [dif_pos h], refl },
+    { rw [dif_neg h],
+      exact (hb _ $ (hu trivial).resolve_left h).symm } }
+end
+end
+
+section
+variable [decidable_eq ι]
+
+/-- `diag i j` is the identity map if `i = j` otherwise it is the constant 0 map. -/
+def diag (i j : ι) : φ i →ₗ[α] φ j :=
+@function.update ι (λj, φ i →ₗ[α] φ j) _ 0 i id j
+
+lemma update_apply (f : Πi, γ →ₗ[α] φ i) (c : γ) (i j : ι) (b : γ →ₗ[α] φ i) :
+  (update f i b j) c = update (λi, f i c) i (b c) j :=
+begin
+  by_cases j = i,
+  { rw [h, update_same, update_same] },
+  { rw [update_noteq h, update_noteq h] }
+end
+
+end
+
+section
+variable [decidable_eq ι]
+variables (α φ)
+
+/-- Standard basis -/
+def std_basis (i : ι) : φ i →ₗ[α] (Πi, φ i) := pi (diag i)
+
+lemma std_basis_apply (i : ι) (b : φ i) : std_basis α φ i b = update 0 i b :=
+by ext j; rw [std_basis, pi_apply, diag, update_apply]; refl
+
+@[simp] lemma std_basis_same (i : ι) (b : φ i) : std_basis α φ i b i = b :=
+by rw [std_basis_apply, update_same]
+
+lemma std_basis_ne (i j : ι) (h : j ≠ i) (b : φ i) : std_basis α φ i b j = 0 :=
+by rw [std_basis_apply, update_noteq h]; refl
+
+lemma ker_std_basis (i : ι) : ker (std_basis α φ i) = ⊥ :=
+ker_eq_bot.2 $ assume f g hfg,
+  have std_basis α φ i f i = std_basis α φ i g i := hfg ▸ rfl,
+  by simpa only [std_basis_same]
+
+lemma proj_comp_std_basis (i j : ι) : (proj i).comp (std_basis α φ j) = diag j i :=
+by rw [std_basis, proj_pi]
+
+lemma proj_std_basis_same (i : ι) : (proj i).comp (std_basis α φ i) = id :=
+by ext b; simp
+
+lemma proj_std_basis_ne (i j : ι) (h : i ≠ j) : (proj i).comp (std_basis α φ j) = 0 :=
+by ext b; simp [std_basis_ne α φ _ _ h]
+
+lemma supr_range_std_basis_le_infi_ker_proj (I J : set ι) (h : disjoint I J) :
+  (⨆i∈I, range (std_basis α φ i)) ≤ (⨅i∈J, ker (proj i)) :=
+begin
+  refine (supr_le $ assume i, supr_le $ assume hi, range_le_iff_comap.2 _),
+  simp only [(ker_comp _ _).symm, eq_top_iff, le_def', mem_ker, comap_infi, mem_infi],
+  assume b hb j hj,
+  have : i ≠ j := assume eq, h ⟨hi, eq.symm ▸ hj⟩,
+  rw [proj_std_basis_ne α φ j i this.symm, zero_apply]
+end
+
+lemma infi_ker_proj_le_supr_range_std_basis {I : finset ι} {J : set ι} (hu : set.univ ⊆ ↑I ∪ J) :
+  (⨅ i∈J, ker (proj i)) ≤ (⨆i∈I, range (std_basis α φ i)) :=
+submodule.le_def'.2
+begin
+  assume b hb,
+  simp only [mem_infi, mem_ker, proj_apply] at hb,
+  rw ← show I.sum (λi, std_basis α φ i (b i)) = b,
+  { ext i,
+    rw [pi.finset_sum_apply, ← std_basis_same α φ i (b i)],
+    refine finset.sum_eq_single i (assume j hjI ne, std_basis_ne _ _ _ _ ne.symm _) _,
+    assume hiI,
+    rw [std_basis_same],
+    exact hb _ ((hu trivial).resolve_left hiI) },
+  exact sum_mem _ (assume i hiI, mem_supr_of_mem _ i $ mem_supr_of_mem _ hiI $
+    linear_map.mem_range.2 ⟨_, rfl⟩)
+end
+
+lemma supr_range_std_basis_eq_infi_ker_proj {I J : set ι}
+  (hd : disjoint I J) (hu : set.univ ⊆ I ∪ J) (hI : set.finite I) :
+  (⨆i∈I, range (std_basis α φ i)) = (⨅i∈J, ker (proj i)) :=
+begin
+  refine le_antisymm (supr_range_std_basis_le_infi_ker_proj _ _ _ _ hd) _,
+  have : set.univ ⊆ ↑hI.to_finset ∪ J, { rwa [finset.coe_to_finset] },
+  refine le_trans (infi_ker_proj_le_supr_range_std_basis α φ this) (supr_le_supr $ assume i, _),
+  rw [← finset.mem_coe, finset.coe_to_finset],
+  exact le_refl _
+end
+
+lemma supr_range_std_basis [fintype ι] : (⨆i:ι, range (std_basis α φ i)) = ⊤ :=
+have (set.univ : set ι) ⊆ ↑(finset.univ : finset ι) ∪ ∅ := by rw [finset.coe_univ, set.union_empty],
+begin
+  apply top_unique,
+  convert (infi_ker_proj_le_supr_range_std_basis α φ this),
+  exact infi_emptyset.symm,
+  exact (funext $ λi, (@supr_pos _ _ _ (λh, range (std_basis α φ i)) $ finset.mem_univ i).symm)
+end
+
+lemma disjoint_std_basis_std_basis (I J : set ι) (h : disjoint I J) :
+  disjoint (⨆i∈I, range (std_basis α φ i)) (⨆i∈J, range (std_basis α φ i)) :=
+begin
+  refine disjoint_mono
+    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl I)
+    (supr_range_std_basis_le_infi_ker_proj _ _ _ _ $ set.disjoint_compl J) _,
+  simp only [disjoint, submodule.le_def', mem_infi, mem_inf, mem_ker, mem_bot, proj_apply,
+    funext_iff],
+  rintros b ⟨hI, hJ⟩ i,
+  classical,
+  by_cases hiI : i ∈ I,
+  { by_cases hiJ : i ∈ J,
+    { exact (h ⟨hiI, hiJ⟩).elim },
+    { exact hJ i hiJ } },
+  { exact hI i hiI }
+end
+
+end
+
+end pi
+
 end linear_map

src/linear_algebra/basis.lean

@@ -120,6 +120,30 @@ linear_independent_Union_of_directed
   ((directed_comp _ _ _).2 $ (directed_on_iff_directed _).1 hs)
   (by simpa using h)
 
+lemma linear_independent_Union_finite {ι : Type*} {f : ι → set β}
+  (hl : ∀i, linear_independent α (f i))
+  (hd : ∀i, ∀t:set ι, finite t → i ∉ t → disjoint (span α (f i)) (⨆i∈t, span α (f i))) :
+  linear_independent α (⋃i, f i) :=
+begin
+  classical,
+  rw [Union_eq_Union_finset f],
+  refine linear_independent_Union_of_directed (directed_of_sup _) _,
+  exact (assume t₁ t₂ ht, Union_subset_Union $ assume i, Union_subset_Union_const $ assume h, ht h),
+  assume t, rw [set.Union, ← finset.sup_eq_supr],
+  refine t.induction_on _ _,
+  { exact linear_independent_empty },
+  { rintros ⟨i⟩ s his ih,
+    rw [finset.sup_insert],
+    refine linear_independent_union (hl _) ih _,
+    rw [finset.sup_eq_supr],
+    refine disjoint_mono (le_refl _) _ (hd i _ _ his),
+    { simp only [(span_Union _).symm],
+      refine span_mono (@supr_le_supr2 (set β) _ _ _ _ _ _),
+      rintros ⟨i⟩, exact ⟨i, le_refl _⟩ },
+    { change finite (plift.up ⁻¹' s.to_set),
+      exact finite_preimage (assume i j, plift.up.inj) s.finite_to_set } }
+end
+
 section repr
 variables (hs : linear_independent α s)
 
@@ -565,3 +589,45 @@ begin
 end.
 
 end vector_space
+
+namespace pi
+open set linear_map
+
+section module
+variables {ι : Type*} {φ : ι → Type*}
+variables [ring α] [∀i, add_comm_group (φ i)] [∀i, module α (φ i)] [fintype ι] [decidable_eq ι]
+
+lemma linear_independent_std_basis (s : Πi, set (φ i)) (hs : ∀i, linear_independent α (s i)) :
+  linear_independent α (⋃i, std_basis α φ i '' s i) :=
+begin
+  refine linear_independent_Union_finite _ _,
+  { assume i,
+    refine (linear_independent_image_iff _).2 (hs i),
+    simp only [ker_std_basis, disjoint_bot_right] },
+  { assume i J _ hiJ,
+    simp [(set.Union.equations._eqn_1 _).symm, submodule.span_image, submodule.span_Union],
+    have h₁ : map (std_basis α φ i) (span α (s i)) ≤ (⨆j∈({i} : set ι), range (std_basis α φ j)),
+    { exact (le_supr_of_le i $ le_supr_of_le (set.mem_singleton _) $ map_mono $ le_top) },
+    have h₂ : (⨆j∈J, map (std_basis α φ j) (span α (s j))) ≤ (⨆j∈J, range (std_basis α φ j)),
+    { exact supr_le_supr (assume i, supr_le_supr $ assume hi, map_mono $ le_top) },
+    exact disjoint_mono h₁ h₂
+      (disjoint_std_basis_std_basis _ _ _ _ $ set.disjoint_singleton_left.2 hiJ) }
+end
+
+lemma is_basis_std_basis [fintype ι] (s : Πi, set (φ i)) (hs : ∀i, is_basis α (s i)) :
+  is_basis α (⋃i, std_basis α φ i '' s i) :=
+begin
+  refine ⟨linear_independent_std_basis _ (assume i, (hs i).1), _⟩,
+  simp only [submodule.span_Union, submodule.span_image, (assume i, (hs i).2), submodule.map_top,
+    supr_range_std_basis]
+end
+
+section
+variables (α ι)
+lemma is_basis_fun [fintype ι] : is_basis α (⋃i, std_basis α (λi:ι, α) i '' {1}) :=
+is_basis_std_basis _ (assume i, is_basis_singleton_one _)
+end
+
+end module
+
+end pi