[Merged by Bors] - feat(ring_theory/finiteness): add finiteness of restrict_scalars

src/ring_theory/adjoin/basic.lean

@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import algebra.algebra.subalgebra
 import linear_algebra.prod
+import algebra.algebra.tower
 
 /-!
 # Adjoining elements to form subalgebras
@@ -56,7 +57,7 @@ le_antisymm (adjoin_le h₁) h₂
 theorem adjoin_eq (S : subalgebra R A) : adjoin R ↑S = S :=
 adjoin_eq_of_le _ (set.subset.refl _) subset_adjoin
 
-@[elab_as_eliminator] theorem adjoin_induction {p : A → Prop} {x : A} (h : x ∈ adjoin R s) 
+@[elab_as_eliminator] theorem adjoin_induction {p : A → Prop} {x : A} (h : x ∈ adjoin R s)
   (Hs : ∀ x ∈ s, p x)
   (Halg : ∀ r, p (algebra_map R A r))
   (Hadd : ∀ x y, p x → p y → p (x + y))
@@ -205,6 +206,12 @@ begin
   congr' 1 with z, simp [submonoid.closure_union, submonoid.mem_sup, set.mem_mul]
 end
 
+variable (A)
+
+lemma adjoin_le_restrict_scalars (B : Type*) [semiring B] [algebra R B] [algebra A B]
+  [is_scalar_tower R A B] (s : set B) : adjoin R s ≤  subalgebra.restrict_scalars R (adjoin A s) :=
+algebra.adjoin_le algebra.subset_adjoin
+
 end comm_semiring
 
 section ring

src/ring_theory/finiteness.lean

@@ -90,7 +90,20 @@ variables (R)
 instance self : finite R R :=
 ⟨⟨{1}, by simpa only [finset.coe_singleton] using ideal.span_singleton_one⟩⟩
 
-variables {R}
+variable (M)
+
+lemma of_restrict_scalars_finite [module A M] [is_scalar_tower R A M] [hM : finite R M] :
+  finite A M :=
+begin
+  rw [finite_def, fg_def] at hM ⊢,
+  obtain ⟨S, hSfin, hSgen⟩ := hM,
+  refine ⟨S, hSfin, eq_top_iff.2 _⟩,
+  have := submodule.span_le_restrict_scalars R A M S,
+  rw hSgen at this,
+  exact this
+end
+
+variables {R M}
 
 instance prod [hM : finite R M] [hN : finite R N] : finite R (M × N) :=
 ⟨begin
@@ -142,6 +155,14 @@ protected lemma mv_polynomial (ι : Type*) [fintype ι] : finite_type R (mv_poly
 end⟩⟩
 end
 
+lemma of_restrict_scalars_finite_type [algebra A B] [is_scalar_tower R A B] [hB : finite_type R B] :
+  finite_type A B :=
+begin
+  obtain ⟨S, hS⟩ := hB.out,
+  refine ⟨⟨S, eq_top_iff.2 (λ b, _)⟩⟩,
+  convert adjoin_le_restrict_scalars R A B ↑S (eq_top_iff.1 hS b)
+end
+
 variables {R A B}
 
 lemma of_surjective (hRA : finite_type R A) (f : A →ₐ[R] B) (hf : surjective f) :
@@ -414,6 +435,16 @@ hf hg
 lemma finite_type {f : A →+* B} (hf : f.finite) : finite_type f :=
 @module.finite.finite_type _ _ _ _ f.to_algebra hf
 
+lemma of_comp_finite {f : A →+* B} {g : B →+* C} (h : (g.comp f).finite) : g.finite :=
+begin
+  letI := f.to_algebra,
+  letI := g.to_algebra,
+  letI := (g.comp f).to_algebra,
+  letI : is_scalar_tower A B C := restrict_scalars.is_scalar_tower A B C,
+  letI : module.finite A C := h,
+  exact module.finite.of_restrict_scalars_finite A B C
+end
+
 end finite
 
 namespace finite_type
@@ -446,6 +477,17 @@ hf hg
 lemma of_finite_presentation {f : A →+* B} (hf : f.finite_presentation) : f.finite_type :=
 @algebra.finite_type.of_finite_presentation A B _ _ f.to_algebra hf
 
+lemma of_comp_finite_type {f : A →+* B} {g : B →+* C} (h : (g.comp f).finite_type) :
+  g.finite_type :=
+begin
+  letI := f.to_algebra,
+  letI := g.to_algebra,
+  letI := (g.comp f).to_algebra,
+  letI : is_scalar_tower A B C := restrict_scalars.is_scalar_tower A B C,
+  letI : algebra.finite_type A C := h,
+  exact algebra.finite_type.of_restrict_scalars_finite_type A B C
+end
+
 end finite_type
 
 namespace finite_presentation
@@ -515,6 +557,9 @@ ring_hom.finite.of_surjective f hf
 lemma finite_type {f : A →ₐ[R] B} (hf : f.finite) : finite_type f :=
 ring_hom.finite.finite_type hf
 
+lemma of_comp_finite {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).finite) : g.finite :=
+ring_hom.finite.of_comp_finite h
+
 end finite
 
 namespace finite_type
@@ -539,6 +584,10 @@ ring_hom.finite_type.of_surjective f hf
 lemma of_finite_presentation {f : A →ₐ[R] B} (hf : f.finite_presentation) : f.finite_type :=
 ring_hom.finite_type.of_finite_presentation hf
 
+lemma of_comp_finite_type {f : A →ₐ[R] B} {g : B →ₐ[R] C} (h : (g.comp f).finite_type) :
+g.finite_type :=
+ring_hom.finite_type.of_comp_finite_type h
+
 end finite_type
 
 namespace finite_presentation