feat(ring_theory/algebra_tower): Artin--Tate lemma (#4282)

Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>

Author: kckennylau

src/field_theory/intermediate_field.lean

@@ -210,7 +210,7 @@ instance to_algebra : algebra S L :=
 S.to_subalgebra.to_algebra
 
 instance : is_scalar_tower K S L :=
-is_scalar_tower.subalgebra _ _ S.to_subalgebra
+is_scalar_tower.subalgebra' _ _ _ S.to_subalgebra
 
 variables {L' : Type*} [field L'] [algebra K L']
 

src/linear_algebra/basic.lean

@@ -723,6 +723,11 @@ le_antisymm (span_le.2 h₁) h₂
 @[simp] lemma span_eq : span R (p : set M) = p :=
 span_eq_of_le _ (subset.refl _) subset_span
 
+lemma map_span (f : M →ₗ[R] M₂) (s : set M) :
+  (span R s).map f = span R (f '' s) :=
+eq.symm $ span_eq_of_le _ (set.image_subset f subset_span) $
+map_le_iff_le_comap.2 $ span_le.2 $ λ x hx, subset_span ⟨x, hx, rfl⟩
+
 /-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
 preserved under addition and scalar multiplication, then `p` holds for all elements of the span of
 `s`. -/

src/linear_algebra/finsupp.lean

@@ -11,12 +11,12 @@ noncomputable theory
 
 open set linear_map submodule
 
-open_locale classical
+open_locale classical big_operators
 
 namespace finsupp
 
 variables {α : Type*} {M : Type*} {N : Type*} {R : Type*}
-variables [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
 
 def lsingle (a : α) : M →ₗ[R] (α →₀ M) :=
 ⟨single a, assume a b, single_add, assume c b, (smul_single _ _ _).symm⟩
@@ -41,7 +41,7 @@ rfl
 rfl
 
 @[simp] lemma ker_lsingle (a : α) : (lsingle a : M →ₗ[R] (α →₀ M)).ker = ⊥ :=
-ker_eq_bot.2 (single_injective a)
+ker_eq_bot_of_injective (single_injective a)
 
 lemma lsingle_range_le_ker_lapply (s t : set α) (h : disjoint s t) :
   (⨆a∈s, (lsingle a : M →ₗ[R] (α →₀ M)).range) ≤ (⨅a∈t, ker (lapply a)) :=
@@ -284,7 +284,7 @@ end lmap_domain
 
 section total
 variables (α) {α' : Type*} (M) {M' : Type*} (R)
-          [add_comm_group M'] [module R M']
+          [add_comm_monoid M'] [semimodule R M']
           (v : α → M) {v' : α' → M'}
 
 /-- Interprets (l : α →₀ R) as linear combination of the elements in the family (v : α → M) and
@@ -463,7 +463,7 @@ by simp [lcongr]
 end finsupp
 
 variables {R : Type*} {M : Type*} {N : Type*}
-variables [ring R] [add_comm_group M] [module R M] [add_comm_group N] [module R N]
+variables [semiring R] [add_comm_monoid M] [semimodule R M] [add_comm_monoid N] [semimodule R N]
 
 lemma linear_map.map_finsupp_total
   (f : M →ₗ[R] N) {ι : Type*} {g : ι → M} (l : ι →₀ R) :
@@ -496,3 +496,10 @@ begin
   have hi : i ∈ s, { rw finset.mem_image, exact ⟨⟨x, hx⟩, finset.mem_univ _, rfl⟩ },
   exact hN i hi (hg _),
 end
+
+lemma mem_span_finset {s : finset M} {x : M} :
+  x ∈ span R (↑s : set M) ↔ ∃ f : M → R, ∑ i in s, f i • i = x :=
+⟨λ hx, let ⟨v, hvs, hvx⟩ := (finsupp.mem_span_iff_total _).1
+    (show x ∈ span R (id '' (↑s : set M)), by rwa set.image_id) in
+  ⟨v, hvx ▸ (finsupp.total_apply_of_mem_supported _ hvs).symm⟩,
+λ ⟨f, hf⟩, hf ▸ sum_mem _ (λ i hi, smul_mem _ _ $ subset_span hi)⟩

src/ring_theory/adjoin.lean

@@ -29,11 +29,11 @@ open submodule
 
 namespace algebra
 
-variables {R : Type u} {A : Type v}
+variables {R : Type u} {A : Type v} {B : Type w}
 
 section semiring
-variables [comm_semiring R] [semiring A]
-variables [algebra R A] {s t : set A}
+variables [comm_semiring R] [semiring A] [semiring B]
+variables [algebra R A] [algebra R B] {s t : set A}
 open subsemiring
 
 theorem subset_adjoin : s ⊆ adjoin R s :=
@@ -76,6 +76,11 @@ begin
   exact span_le.2 (show monoid.closure s ⊆ adjoin R s, from monoid.closure_subset subset_adjoin)
 end
 
+lemma adjoin_image (f : A →ₐ[R] B) (s : set A) :
+  adjoin R (f '' s) = (adjoin R s).map f :=
+le_antisymm (adjoin_le $ set.image_subset _ subset_adjoin) $
+subalgebra.map_le.2 $ adjoin_le $ set.image_subset_iff.1 subset_adjoin
+
 end semiring
 
 section comm_semiring
@@ -199,21 +204,44 @@ end algebra
 
 namespace subalgebra
 
-variables {R : Type u} {A : Type v}
-variables [comm_ring R] [comm_ring A] [algebra R A]
+variables {R : Type u} {A : Type v} {B : Type w}
+variables [comm_semiring R] [semiring A] [algebra R A] [semiring B] [algebra R B]
 
 /-- A subalgebra `S` is finitely generated if there exists `t : finset A` such that
 `algebra.adjoin R t = S`. -/
 def fg (S : subalgebra R A) : Prop :=
 ∃ t : finset A, algebra.adjoin R ↑t = S
 
+lemma fg_adjoin_finset (s : finset A) : (algebra.adjoin R (↑s : set A)).fg :=
+⟨s, rfl⟩
+
 theorem fg_def {S : subalgebra R A} : S.fg ↔ ∃ t : set A, set.finite t ∧ algebra.adjoin R t = S :=
 ⟨λ ⟨t, ht⟩, ⟨↑t, set.finite_mem_finset t, ht⟩,
 λ ⟨t, ht1, ht2⟩, ⟨ht1.to_finset, by rwa set.finite.coe_to_finset⟩⟩
 
 theorem fg_bot : (⊥ : subalgebra R A).fg :=
 ⟨∅, algebra.adjoin_empty R A⟩
 
+lemma fg_of_submodule_fg (h : (⊤ : submodule R A).fg) : (⊤ : subalgebra R A).fg :=
+let ⟨s, hs⟩ := h in ⟨s, to_submodule_injective $
+by { rw [algebra.coe_top, eq_top_iff, ← hs, span_le], exact algebra.subset_adjoin }⟩
+
+section
+open_locale classical
+lemma fg_map (S : subalgebra R A) (f : A →ₐ[R] B) (hs : S.fg) : (S.map f).fg :=
+let ⟨s, hs⟩ := hs in ⟨s.image f, by rw [finset.coe_image, algebra.adjoin_image, hs]⟩
+end
+
+lemma fg_of_fg_map (S : subalgebra R A) (f : A →ₐ[R] B) (hf : function.injective f)
+  (hs : (S.map f).fg) : S.fg :=
+let ⟨s, hs⟩ := hs in ⟨s.preimage f $ λ _ _ _ _ h, hf h, map_injective f hf $
+by { rw [← algebra.adjoin_image, finset.coe_preimage, set.image_preimage_eq_of_subset, hs],
+  rw [← alg_hom.coe_range, ← algebra.adjoin_le_iff, hs, ← algebra.map_top], exact map_mono le_top }⟩
+
+lemma fg_top (S : subalgebra R A) : (⊤ : subalgebra R S).fg ↔ S.fg :=
+⟨λ h, by { rw [← S.range_val, ← algebra.map_top], exact fg_map _ _ h },
+λ h, fg_of_fg_map _ S.val subtype.val_injective $ by { rw [algebra.map_top, range_val], exact h }⟩
+
 end subalgebra
 
 variables {R : Type u} {A : Type v} {B : Type w}

src/ring_theory/algebra.lean

@@ -948,9 +948,9 @@ instance algebra : algebra R S :=
   smul_def' := λ c x, subtype.eq $ algebra.smul_def _ _,
   .. (algebra_map R A).cod_srestrict S $ λ x, S.range_le ⟨x, rfl⟩ }
 
-instance to_algebra {R : Type u} {A : Type v} [comm_semiring R] [comm_semiring A]
-  [algebra R A] (S : subalgebra R A) : algebra S A :=
-algebra.of_subsemiring _
+instance to_algebra {R A B : Type*} [comm_semiring R] [comm_semiring A] [semiring B]
+  [algebra R A] [algebra A B] (A₀ : subalgebra R A) : algebra A₀ B :=
+algebra.of_subsemiring A₀
 
 instance nontrivial [nontrivial A] : nontrivial S :=
 subsemiring.nontrivial S
@@ -962,7 +962,8 @@ subsemiring.nontrivial S
 def val : S →ₐ[R] A :=
 by refine_struct { to_fun := (coe : S → A) }; intros; refl
 
-@[simp]
+@[simp] lemma coe_val : (S.val : S → A) = coe := rfl
+
 lemma val_apply (x : S) : S.val x = (x : A) := rfl
 
 /-- Convert a `subalgebra` to `submodule` -/
@@ -1019,10 +1020,18 @@ def comap' (S : subalgebra R B) (f : A →ₐ[R] B) : subalgebra R A :=
     from (f.commutes r).symm ▸ S.algebra_map_mem r,
   .. subsemiring.comap (f : A →+* B) S,}
 
+lemma map_mono {S₁ S₂ : subalgebra R A} {f : A →ₐ[R] B} :
+  S₁ ≤ S₂ → S₁.map f ≤ S₂.map f :=
+set.image_subset f
+
 theorem map_le {S : subalgebra R A} {f : A →ₐ[R] B} {U : subalgebra R B} :
   map S f ≤ U ↔ S ≤ comap' U f :=
 set.image_subset_iff
 
+lemma map_injective {S₁ S₂ : subalgebra R A} (f : A →ₐ[R] B)
+  (hf : function.injective f) (ih : S₁.map f = S₂.map f) : S₁ = S₂ :=
+ext $ set.ext_iff.1 $ set.image_injective.2 hf $ set.ext $ ext_iff.1 ih
+
 lemma mem_map {S : subalgebra R A} {f : A →ₐ[R] B} {y : B} :
   y ∈ map S f ↔ ∃ x ∈ S, f x = y :=
 subsemiring.mem_map
@@ -1160,6 +1169,17 @@ bot_equiv_of_injective (ring_hom.injective _)
 
 end algebra
 
+namespace subalgebra
+
+variables {R : Type u} {A : Type v}
+variables [comm_semiring R] [semiring A] [algebra R A]
+variables (S : subalgebra R A)
+
+lemma range_val : S.val.range = S :=
+ext $ set.ext_iff.1 $ S.val.coe_range.trans subtype.range_val
+
+end subalgebra
+
 section nat
 
 variables (R : Type*) [semiring R]

src/ring_theory/algebra_tower.lean

@@ -47,16 +47,22 @@ end semimodule
 
 section semiring
 variables [comm_semiring R] [comm_semiring S] [semiring A] [semiring B]
-variables [algebra R S] [algebra S A] [algebra R A] [algebra S B] [algebra R B]
-variables {R S A}
+variables [algebra R S] [algebra S A] [algebra S B]
 
-theorem of_algebra_map_eq (h : ∀ x, algebra_map R A x = algebra_map S A (algebra_map R S x)) :
+variables {R S A}
+theorem of_algebra_map_eq [algebra R A]
+  (h : ∀ x, algebra_map R A x = algebra_map S A (algebra_map R S x)) :
   is_scalar_tower R S A :=
 ⟨λ x y z, by simp_rw [algebra.smul_def, ring_hom.map_mul, mul_assoc, h]⟩
 
+variables (R S A)
+
+instance subalgebra (S₀ : subalgebra R S) : is_scalar_tower S₀ S A :=
+of_algebra_map_eq $ λ x, rfl
+
+variables [algebra R A] [algebra R B]
 variables [is_scalar_tower R S A] [is_scalar_tower R S B]
 
-variables (R S A)
 theorem algebra_map_eq :
   algebra_map R A = (algebra_map S A).comp (algebra_map R S) :=
 ring_hom.ext $ λ x, by simp_rw [ring_hom.comp_apply, algebra.algebra_map_eq_smul_one,
@@ -65,6 +71,10 @@ ring_hom.ext $ λ x, by simp_rw [ring_hom.comp_apply, algebra.algebra_map_eq_smu
 theorem algebra_map_apply (x : R) : algebra_map R A x = algebra_map S A (algebra_map R S x) :=
 by rw [algebra_map_eq R S A, ring_hom.comp_apply]
 
+instance subalgebra' (S₀ : subalgebra R S) : is_scalar_tower R S₀ A :=
+@is_scalar_tower.of_algebra_map_eq R S₀ A _ _ _ _ _ _ $ λ _,
+(is_scalar_tower.algebra_map_apply R S A _ : _)
+
 @[ext] lemma algebra.ext {S : Type u} {A : Type v} [comm_semiring S] [semiring A]
   (h1 h2 : algebra S A) (h : ∀ {r : S} {x : A}, (by haveI := h1; exact r • x) = r • x) : h1 = h2 :=
 begin
@@ -108,10 +118,12 @@ instance comap {R S A : Type*} [comm_semiring R] [comm_semiring S] [semiring A]
   [algebra R S] [algebra S A] : is_scalar_tower R S (algebra.comap R S A) :=
 of_algebra_map_eq $ λ x, rfl
 
-instance subsemiring (U : subsemiring S) : is_scalar_tower U S A :=
+-- conflicts with is_scalar_tower.subalgebra
+@[priority 999] instance subsemiring (U : subsemiring S) : is_scalar_tower U S A :=
 of_algebra_map_eq $ λ x, rfl
 
-instance subring {S A : Type*} [comm_ring S] [ring A] [algebra S A]
+-- conflicts with is_scalar_tower.subalgebra
+@[priority 999] instance subring {S A : Type*} [comm_ring S] [ring A] [algebra S A]
   (U : set S) [is_subring U] : is_scalar_tower U S A :=
 of_algebra_map_eq $ λ x, rfl
 
@@ -121,21 +133,19 @@ instance of_ring_hom {R A B : Type*} [comm_semiring R] [comm_semiring A] [comm_s
   @is_scalar_tower R A B _ (f.to_ring_hom.to_algebra.to_has_scalar) _ :=
 by { letI := (f : A →+* B).to_algebra, exact of_algebra_map_eq (λ x, (f.commutes x).symm) }
 
-end semiring
-
-section comm_semiring
-variables [comm_semiring R] [comm_semiring A] [algebra R A]
-variables [comm_semiring B] [algebra A B] [algebra R B] [is_scalar_tower R A B]
+instance polynomial : is_scalar_tower R S (polynomial A) :=
+of_algebra_map_eq $ λ x, congr_arg polynomial.C $ algebra_map_apply R S A x
 
-instance subalgebra (S : subalgebra R A) : is_scalar_tower R S A :=
-of_algebra_map_eq $ λ x, rfl
+variables (R S A)
+theorem aeval_apply (x : A) (p : polynomial R) : polynomial.aeval x p =
+  polynomial.aeval x (polynomial.map (algebra_map R S) p) :=
+by rw [polynomial.aeval_def, polynomial.aeval_def, polynomial.eval₂_map, algebra_map_eq R S A]
 
-instance polynomial : is_scalar_tower R A (polynomial B) :=
-of_algebra_map_eq $ λ x, congr_arg polynomial.C $ algebra_map_apply R A B x
+end semiring
 
-theorem aeval_apply (x : B) (p : polynomial R) : polynomial.aeval x p =
-  polynomial.aeval x (polynomial.map (algebra_map R A) p) :=
-by rw [polynomial.aeval_def, polynomial.aeval_def, polynomial.eval₂_map, algebra_map_eq R A B]
+section comm_semiring
+variables [comm_semiring R] [comm_semiring A] [comm_semiring B]
+variables [algebra R A] [algebra A B] [algebra R B] [is_scalar_tower R A B]
 
 lemma algebra_map_aeval (x : A) (p : polynomial R) :
   algebra_map A B (polynomial.aeval x p) = polynomial.aeval (algebra_map A B x) p :=
@@ -246,6 +256,17 @@ by { ext z, exact ⟨λ ⟨⟨x, y, _, h1⟩, h2⟩, ⟨y, h2 ▸ h1⟩, λ ⟨y
 
 end is_scalar_tower
 
+section
+open_locale classical
+lemma algebra.fg_trans' {R S A : Type*} [comm_ring R] [comm_ring S] [comm_ring A]
+  [algebra R S] [algebra S A] [algebra R A] [is_scalar_tower R S A]
+  (hRS : (⊤ : subalgebra R S).fg) (hSA : (⊤ : subalgebra S A).fg) :
+  (⊤ : subalgebra R A).fg :=
+let ⟨s, hs⟩ := hRS, ⟨t, ht⟩ := hSA in ⟨s.image (algebra_map S A) ∪ t,
+by rw [finset.coe_union, finset.coe_image, algebra.adjoin_union, algebra.adjoin_algebra_map, hs,
+    algebra.map_top, is_scalar_tower.range_under_adjoin, ht, subalgebra.res_top]⟩
+end
+
 namespace submodule
 
 open is_scalar_tower
@@ -379,3 +400,66 @@ theorem is_basis.smul_repr_mk
 by simp [is_basis.smul_repr]
 
 end ring
+
+section artin_tate
+
+variables (C : Type*)
+variables [comm_ring A] [comm_ring B] [comm_ring C]
+variables [algebra A B] [algebra B C] [algebra A C] [is_scalar_tower A B C]
+
+open finset submodule
+open_locale classical
+
+lemma exists_subalgebra_of_fg (hAC : (⊤ : subalgebra A C).fg) (hBC : (⊤ : submodule B C).fg) :
+  ∃ B₀ : subalgebra A B, B₀.fg ∧ (⊤ : submodule B₀ C).fg :=
+begin
+  cases hAC with x hx,
+  cases hBC with y hy, have := hy,
+  simp_rw [eq_top_iff', mem_span_finset] at this, choose f hf,
+  let s : finset B := (finset.product (x ∪ (y * y)) y).image (function.uncurry f),
+  have hsx : ∀ (xi ∈ x) (yj ∈ y), f xi yj ∈ s := λ xi hxi yj hyj,
+    show function.uncurry f (xi, yj) ∈ s,
+    from mem_image_of_mem _ $ mem_product.2 ⟨mem_union_left _ hxi, hyj⟩,
+  have hsy : ∀ (yi yj yk ∈ y), f (yi * yj) yk ∈ s := λ yi yj yk hyi hyj hyk,
+    show function.uncurry f (yi * yj, yk) ∈ s,
+    from mem_image_of_mem _ $ mem_product.2 ⟨mem_union_right _ $ finset.mul_mem_mul hyi hyj, hyk⟩,
+  have hxy : ∀ xi ∈ x, xi ∈ span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C) :=
+    λ xi hxi, hf xi ▸ sum_mem _ (λ yj hyj, smul_mem
+      (span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C))
+      ⟨f xi yj, algebra.subset_adjoin $ hsx xi hxi yj hyj⟩
+      (subset_span $ mem_insert_of_mem hyj)),
+  have hyy : span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C) *
+      span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C) ≤
+    span (algebra.adjoin A (↑s : set B)) (↑(insert 1 y : finset C) : set C),
+  { rw [span_mul_span, span_le, coe_insert], rintros _ ⟨yi, yj, rfl | hyi, rfl | hyj, rfl⟩,
+    { rw mul_one, exact subset_span (set.mem_insert _ _) },
+    { rw one_mul, exact subset_span (set.mem_insert_of_mem _ hyj) },
+    { rw mul_one, exact subset_span (set.mem_insert_of_mem _ hyi) },
+    { rw ← hf (yi * yj), exact (submodule.mem_coe _).2 (sum_mem _ $ λ yk hyk, smul_mem
+        (span (algebra.adjoin A (↑s : set B)) (insert 1 ↑y : set C))
+        ⟨f (yi * yj) yk, algebra.subset_adjoin $ hsy yi yj yk hyi hyj hyk⟩
+        (subset_span $ set.mem_insert_of_mem _ hyk : yk ∈ _)) } },
+  refine ⟨algebra.adjoin A (↑s : set B), subalgebra.fg_adjoin_finset _, insert 1 y, _⟩,
+  refine restrict_scalars'_injective _ _ (_ : restrict_scalars' A _ = _),
+  rw [restrict_scalars'_top, eq_top_iff, ← algebra.coe_top, ← hx, algebra.adjoin_eq_span, span_le],
+  refine λ r hr, monoid.in_closure.rec_on hr hxy (subset_span $ mem_insert_self _ _)
+      (λ p q _ _ hp hq, hyy $ submodule.mul_mem_mul hp hq)
+end
+
+/-- Artin--Tate lemma: if A ⊆ B ⊆ C is a chain of subrings of commutative rings, and
+A is noetherian, and C is algebra-finite over A, and C is module-finite over B,
+then B is algebra-finite over A.
+
+References: Atiyah--Macdonald Proposition 7.8; Stacks 00IS; Altman--Kleiman 16.17. -/
+theorem fg_of_fg_of_fg [is_noetherian_ring A]
+  (hAC : (⊤ : subalgebra A C).fg) (hBC : (⊤ : submodule B C).fg)
+  (hBCi : function.injective (algebra_map B C)) :
+  (⊤ : subalgebra A B).fg :=
+let ⟨B₀, hAB₀, hB₀C⟩ := exists_subalgebra_of_fg A B C hAC hBC in
+algebra.fg_trans' (B₀.fg_top.2 hAB₀) $ subalgebra.fg_of_submodule_fg $
+have is_noetherian_ring B₀, from is_noetherian_ring_of_fg hAB₀,
+have is_noetherian B₀ C, by exactI is_noetherian_of_fg_of_noetherian' hB₀C,
+by exactI fg_of_injective (is_scalar_tower.to_alg_hom B₀ B C).to_linear_map
+  (linear_map.ker_eq_bot.2 hBCi)
+
+end artin_tate