refactor(linear_algebra/basic): extract definitions about pi types to…

… a new file (#6130)

This makes it consistent with how the `prod` definitions are in their own file.
With each in its own file, it should be easier to unify the APIs between them.
This does not do anything other than copy across the definitions.

src/linear_algebra/affine_space/affine_map.lean

@@ -6,6 +6,7 @@ Author: Joseph Myers.
 import linear_algebra.affine_space.basic
 import linear_algebra.tensor_product
 import linear_algebra.prod
+import linear_algebra.pi
 import data.set.intervals.unordered_interval
 
 /-!

src/linear_algebra/basic.lean

@@ -2237,97 +2237,6 @@ quotient_inf_equiv_sup_quotient_symm_apply_eq_zero_iff.2 hx
 
 end isomorphism_laws
 
-section pi
-universe i
-variables [semiring R] [add_comm_monoid M₂] [semimodule R M₂] [add_comm_monoid M₃] [semimodule R M₃]
-{φ : ι → Type i} [∀i, add_comm_monoid (φ i)] [∀i, semimodule R (φ 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, M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (Πi, φ i) :=
-⟨λc i, f i c, λ c d, funext $ λ i, (f i).map_add _ _, λ c d, funext $ λ i, (f i).map_smul _ _⟩
-
-@[simp] lemma pi_apply (f : Πi, M₂ →ₗ[R] φ i) (c : M₂) (i : ι) :
-  pi f c i = f i c := rfl
-
-lemma ker_pi (f : Πi, M₂ →ₗ[R] φ i) : ker (pi f) = (⨅i:ι, ker (f i)) :=
-by ext c; simp [funext_iff]; refl
-
-lemma pi_eq_zero (f : Πi, M₂ →ₗ[R] φ 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, M₂ →ₗ[R] φ i) = 0 :=
-by ext; refl
-
-lemma pi_comp (f : Πi, M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) : (pi f).comp g = pi (λi, (f i).comp g) :=
-rfl
-
-/-- The projections from a family of modules are linear maps. -/
-def proj (i : ι) : (Πi, φ i) →ₗ[R] φ i :=
-⟨ λa, a i, assume f g, rfl, assume c f, rfl ⟩
-
-@[simp] lemma proj_apply (i : ι) (b : Πi, φ i) : (proj i : (Πi, φ i) →ₗ[R] φ i) b = b i := rfl
-
-lemma proj_pi (f : Πi, M₂ →ₗ[R] φ i) (i : ι) : (proj i).comp (pi f) = f i :=
-ext $ assume c, rfl
-
-lemma infi_ker_proj : (⨅i, ker (proj i) : submodule R (Π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 (R φ)
-
-/-- If `I` and `J` are disjoint index sets, the product of the kernels of the `J`th projections of
-`φ` is linearly equivalent to the product over `I`. -/
-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 R (Πi, φ i)) ≃ₗ[R] (Π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.coe_prop],
-    ext b ⟨j, hj⟩, refl },
-  { ext1 ⟨b, hb⟩,
-    apply subtype.ext,
-    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,
-    { refl },
-    { 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 →ₗ[R] φ j :=
-@function.update ι (λj, φ i →ₗ[R] φ j) _ 0 i id j
-
-lemma update_apply (f : Πi, M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ 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
-
-end pi
-
 section fun_left
 variables (R M) [semiring R] [add_comm_monoid M] [semimodule R M]
 variables {m n p : Type*}

src/linear_algebra/pi.lean

@@ -0,0 +1,121 @@
+/-
+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, Mario Carneiro, Kevin Buzzard, Yury Kudryashov, Eric Wieser
+-/
+import linear_algebra.basic
+
+/-!
+# Pi types of semimodules
+
+This file defines constructors for linear maps whose domains or codomains are pi types.
+
+It contains theorems relating these to each other, as well as to `linear_map.ker`.
+
+## Main definitions
+
+- pi types in the codomain:
+  - `linear_map.proj`
+  - `linear_map.pi`
+- `linear_map.diag`
+
+-/
+
+universes u v w x y z u' v' w' y'
+variables {R : Type u} {K : Type u'} {M : Type v} {V : Type v'} {M₂ : Type w} {V₂ : Type w'}
+variables {M₃ : Type y} {V₃ : Type y'} {M₄ : Type z} {ι : Type x}
+
+namespace linear_map
+
+open function
+open submodule
+
+universe i
+variables [semiring R] [add_comm_monoid M₂] [semimodule R M₂] [add_comm_monoid M₃] [semimodule R M₃]
+{φ : ι → Type i} [∀i, add_comm_monoid (φ i)] [∀i, semimodule R (φ 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, M₂ →ₗ[R] φ i) : M₂ →ₗ[R] (Πi, φ i) :=
+⟨λc i, f i c, λ c d, funext $ λ i, (f i).map_add _ _, λ c d, funext $ λ i, (f i).map_smul _ _⟩
+
+@[simp] lemma pi_apply (f : Πi, M₂ →ₗ[R] φ i) (c : M₂) (i : ι) :
+  pi f c i = f i c := rfl
+
+lemma ker_pi (f : Πi, M₂ →ₗ[R] φ i) : ker (pi f) = (⨅i:ι, ker (f i)) :=
+by ext c; simp [funext_iff]; refl
+
+lemma pi_eq_zero (f : Πi, M₂ →ₗ[R] φ 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, M₂ →ₗ[R] φ i) = 0 :=
+by ext; refl
+
+lemma pi_comp (f : Πi, M₂ →ₗ[R] φ i) (g : M₃ →ₗ[R] M₂) : (pi f).comp g = pi (λi, (f i).comp g) :=
+rfl
+
+/-- The projections from a family of modules are linear maps. -/
+def proj (i : ι) : (Πi, φ i) →ₗ[R] φ i :=
+⟨ λa, a i, assume f g, rfl, assume c f, rfl ⟩
+
+@[simp] lemma proj_apply (i : ι) (b : Πi, φ i) : (proj i : (Πi, φ i) →ₗ[R] φ i) b = b i := rfl
+
+lemma proj_pi (f : Πi, M₂ →ₗ[R] φ i) (i : ι) : (proj i).comp (pi f) = f i :=
+ext $ assume c, rfl
+
+lemma infi_ker_proj : (⨅i, ker (proj i) : submodule R (Π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 (R φ)
+
+/-- If `I` and `J` are disjoint index sets, the product of the kernels of the `J`th projections of
+`φ` is linearly equivalent to the product over `I`. -/
+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 R (Πi, φ i)) ≃ₗ[R] (Π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.coe_prop],
+    ext b ⟨j, hj⟩, refl },
+  { ext1 ⟨b, hb⟩,
+    apply subtype.ext,
+    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,
+    { refl },
+    { 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 →ₗ[R] φ j :=
+@function.update ι (λj, φ i →ₗ[R] φ j) _ 0 i id j
+
+lemma update_apply (f : Πi, M₂ →ₗ[R] φ i) (c : M₂) (i j : ι) (b : M₂ →ₗ[R] φ 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
+
+end linear_map

src/linear_algebra/std_basis.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 import linear_algebra.basic
 import linear_algebra.basis
+import linear_algebra.pi
 
 /-!
 # The standard basis

src/topology/algebra/module.lean

@@ -7,6 +7,7 @@ import topology.algebra.ring
 import topology.uniform_space.uniform_embedding
 import algebra.algebra.basic
 import linear_algebra.projection
+import linear_algebra.pi
 
 /-!
 # Theory of topological modules and continuous linear maps.