feat(ring_theory/noetherian): fg_pi (#10845)

src/linear_algebra/free_module/strong_rank_condition.lean

@@ -43,7 +43,9 @@ begin
   { rwa strong_rank_condition_iff_succ R },
   intros n f, by_contradiction hf,
 
-  letI := module.finite.of_basis (pi.basis_fun R (fin (n + 1))),
+  -- Lean is unable to find this instance without help, either via this `letI`, or via a duplicate
+  -- instance with unecessarily strong typeclasses on `R` and `M`.
+  letI : module.finite R (fin n.succ → R) := module.finite.pi,
 
   let g : (fin (n + 1) → R) →ₗ[R] fin (n + 1) → R :=
     (extend_by_zero.linear_map R cast_succ).comp f,

src/linear_algebra/pi.lean

@@ -215,12 +215,21 @@ def pi (I : set ι) (p : Π i, submodule R (φ i)) : submodule R (Π i, φ i) :=
   add_mem' := λ x y hx hy i hi, (p i).add_mem (hx i hi) (hy i hi),
   smul_mem' := λ c x hx i hi, (p i).smul_mem c (hx i hi) }
 
-variables {I : set ι} {p : Π i, submodule R (φ i)} {x : Π i, φ i}
+variables {I : set ι} {p q : Π i, submodule R (φ i)} {x : Π i, φ i}
 
 @[simp] lemma mem_pi : x ∈ pi I p ↔ ∀ i ∈ I, x i ∈ p i := iff.rfl
 
 @[simp, norm_cast] lemma coe_pi : (pi I p : set (Π i, φ i)) = set.pi I (λ i, p i) := rfl
 
+@[simp] lemma pi_empty (p : Π i, submodule R (φ i)) : pi ∅ p = ⊤ :=
+set_like.coe_injective $ set.empty_pi _
+
+@[simp] lemma pi_top (s : set ι) : pi s (λ i : ι, (⊤ : submodule R (φ i))) = ⊤ :=
+set_like.coe_injective $ set.pi_univ _
+
+lemma pi_mono {s : set ι} (h : ∀ i ∈ s, p i ≤ q i) : pi s p ≤ pi s q :=
+set.pi_mono h
+
 lemma binfi_comap_proj : (⨅ i ∈ I, comap (proj i) (p i)) = pi I p :=
 by { ext x, simp }
 

src/ring_theory/finiteness.lean

@@ -112,6 +112,13 @@ instance prod [hM : finite R M] [hN : finite R N] : finite R (M × N) :=
   exact submodule.fg_prod hM.1 hN.1
 end⟩
 
+instance pi {ι : Type*} {M : ι → Type*} [fintype ι] [Π i, add_comm_monoid (M i)]
+  [Π i, module R (M i)] [h : ∀ i, finite R (M i)] : finite R (Π i, M i) :=
+⟨begin
+  rw ← submodule.pi_top,
+  exact submodule.fg_pi (λ i, (h i).1),
+end⟩
+
 lemma equiv [hM : finite R M] (e : M ≃ₗ[R] N) : finite R N :=
 of_surjective (e : M →ₗ[R] N) e.surjective
 

src/ring_theory/noetherian.lean

@@ -184,6 +184,18 @@ fg_def.2 ⟨linear_map.inl R M P '' tb ∪ linear_map.inr R M P '' tc,
   (htb.1.image _).union (htc.1.image _),
   by rw [linear_map.span_inl_union_inr, htb.2, htc.2]⟩
 
+theorem fg_pi {ι : Type*} {M : ι → Type*} [fintype ι] [Π i, add_comm_monoid (M i)]
+  [Π i, module R (M i)] {p : Π i, submodule R (M i)} (hsb : ∀ i, (p i).fg) :
+  (submodule.pi set.univ p).fg :=
+begin
+  classical,
+  simp_rw fg_def at hsb ⊢,
+  choose t htf hts using hsb,
+  refine ⟨
+    ⋃ i, (linear_map.single i : _ →ₗ[R] _) '' t i, set.finite_Union $ λ i, (htf i).image _, _⟩,
+  simp_rw [span_Union, span_image, hts, submodule.supr_map_single],
+end
+
 /-- If 0 → M' → M → M'' → 0 is exact and M' and M'' are
 finitely generated then so is M. -/
 theorem fg_of_fg_map_of_fg_inf_ker {R M P : Type*} [ring R] [add_comm_group M] [module R M]