feat(ring_theory/finiteness): add quotient of finitely presented (#6098)

I've added `algebra.finitely_presented.quotient`: the quotient of a finitely presented algebra by a finitely generated ideal is finitely presented. To do so I had to prove some preliminary results about finitely generated modules.

Author: riccardobrasca

src/algebra/algebra/basic.lean

@@ -1359,6 +1359,22 @@ lemma restrict_scalars_bot : restrict_scalars R (⊥ : submodule A M) = ⊥ := r
 @[simp]
 lemma restrict_scalars_top : restrict_scalars R (⊤ : submodule A M) = ⊤ := rfl
 
+/-- If `A` is an `R`-algebra, then the `R`-module generated by a set `X` is included in the
+`A`-module generated by `X`. -/
+lemma span_le_restrict_scalars (X : set M) : span R (X : set M) ≤ restrict_scalars R (span A X) :=
+submodule.span_le.mpr submodule.subset_span
+
+/-- If `A` is an `R`-algebra such that the induced morhpsim `R →+* A` is surjective, then the
+`R`-module generated by a set `X` equals the `A`-module generated by `X`. -/
+lemma span_eq_restrict_scalars (X : set M) (hsur : function.surjective (algebra_map R A)) :
+  span R X = restrict_scalars R (span A X) :=
+begin
+  apply (span_le_restrict_scalars R A M X).antisymm (λ m hm, _),
+  refine span_induction hm subset_span (zero_mem _) (λ _ _, add_mem _) (λ a m hm, _),
+  obtain ⟨r, rfl⟩ := hsur a,
+  simpa [algebra_map_smul] using smul_mem _ r hm
+end
+
 end submodule
 
 @[simp]

src/ring_theory/finiteness.lean

@@ -200,6 +200,8 @@ end finite_type
 
 namespace finitely_presented
 
+variables {R A B}
+
 /-- If `e : A ≃ₐ[R] B` and `A` is finitely presented, then so is `B`. -/
 lemma equiv (hfp : finitely_presented R A) (e : A ≃ₐ[R] B) : finitely_presented R B :=
 begin
@@ -217,6 +219,8 @@ begin
       ring_hom.ker_coe_equiv (alg_equiv.to_ring_equiv e), ring_hom.ker_eq_comap_bot] }
 end
 
+variable (R)
+
 /-- The ring of polynomials in finitely many variables is finitely presented. -/
 lemma mv_polynomial (ι : Type u_2) [fintype ι] : finitely_presented R (mv_polynomial ι R) :=
 begin
@@ -239,6 +243,26 @@ begin
     (mv_polynomial.pempty_alg_equiv R)
 end
 
+variable {R}
+
+/-- The quotient of a finitely presented algebra by a finitely generated ideal is finitely
+presented. -/
+lemma quotient {I : ideal A} (h : submodule.fg I) (hfp : finitely_presented R A) :
+  finitely_presented R I.quotient :=
+begin
+  obtain ⟨n, f, hf⟩ := hfp,
+  refine ⟨n, (ideal.quotient.mkₐ R I).comp f, _, _⟩,
+  { exact (ideal.quotient.mkₐ_surjective R I).comp hf.1 },
+  { refine submodule.fg_ker_ring_hom_comp _ _ hf.2 _ hf.1,
+    rwa ideal.quotient.mkₐ_ker R I }
+end
+
+/-- If `f : A →ₐ[R] B` is surjective with finitely generated kernel and `A` is finitely presented,
+then so is `B`. -/
+lemma of_surjective {f : A →ₐ[R] B} (hf : function.surjective f) (hker : f.to_ring_hom.ker.fg)
+  (hfp : finitely_presented R A) : finitely_presented R B :=
+equiv (quotient hker hfp) (ideal.quotient_ker_alg_equiv_of_surjective hf)
+
 end finitely_presented
 
 end algebra

src/ring_theory/noetherian.lean

@@ -200,6 +200,41 @@ begin
     { exact zero_smul _ }, { exact λ _ _ _, add_smul _ _ _ } }
 end
 
+/-- The kernel of the composition of two linear maps is finitely generated if both kernels are and
+the first morphism is surjective. -/
+lemma fg_ker_comp {R M N P : Type*} [ring R] [add_comm_group M] [module R M]
+  [add_comm_group N] [module R N] [add_comm_group P] [module R P] (f : M →ₗ[R] N)
+  (g : N →ₗ[R] P) (hf1 : f.ker.fg) (hf2 : g.ker.fg) (hsur : function.surjective f) :
+  (g.comp f).ker.fg :=
+begin
+  rw linear_map.ker_comp,
+  apply fg_of_fg_map_of_fg_inf_ker f,
+  { rwa [linear_map.map_comap_eq, linear_map.range_eq_top.2 hsur, top_inf_eq] },
+  { rwa [inf_of_le_right (show f.ker ≤ (comap f g.ker), from comap_mono (@bot_le _ _ g.ker))] }
+end
+
+lemma fg_restrict_scalars {R S M : Type*} [comm_ring R] [comm_ring S] [algebra R S]
+  [add_comm_group M] [module S M] [module R M] [is_scalar_tower R S M] (N : submodule S M)
+  (hfin : N.fg) (h : function.surjective (algebra_map R S)) : (submodule.restrict_scalars R N).fg :=
+begin
+  obtain ⟨X, rfl⟩ := hfin,
+  use X,
+  exact submodule.span_eq_restrict_scalars R S M X h
+end
+
+lemma fg_ker_ring_hom_comp {R S A : Type*} [comm_ring R] [comm_ring S] [comm_ring A]
+  (f : R →+* S) (g : S →+* A) (hf : f.ker.fg) (hg : g.ker.fg) (hsur : function.surjective f) :
+  (g.comp f).ker.fg :=
+begin
+  letI : algebra R S := ring_hom.to_algebra f,
+  letI : algebra R A := ring_hom.to_algebra (g.comp f),
+  letI : algebra S A := ring_hom.to_algebra g,
+  letI : is_scalar_tower R S A := is_scalar_tower.comap,
+  let f₁ := algebra.linear_map R S,
+  let g₁ := (is_scalar_tower.to_alg_hom R S A).to_linear_map,
+  exact fg_ker_comp f₁ g₁ hf (fg_restrict_scalars g.ker hg hsur) hsur
+end
+
 /-- Finitely generated submodules are precisely compact elements in the submodule lattice. -/
 theorem fg_iff_compact (s : submodule R M) : s.fg ↔ complete_lattice.is_compact_element s :=
 begin