feat(ring_theory/artinian): localization maps of artinian rings are surjective (#15736)

The proof is by Junyan, I just tidied it up a little, and also the `ring_theory/artinian` file a little bit, in order to fit the results more smoothly.

Co-authored-by: Junyan Xu <junyanxumath@gmail.com>



Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>

Author: ericrbg

src/ring_theory/artinian.lean

@@ -3,17 +3,8 @@ Copyright (c) 2021 Chris Hughes. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Hughes
 -/
-import linear_algebra.basic
-import linear_algebra.prod
-import linear_algebra.pi
-import data.set_like.fintype
-import linear_algebra.linear_independent
-import tactic.linarith
-import algebra.algebra.basic
-import ring_theory.noetherian
-import ring_theory.jacobson_ideal
-import ring_theory.nilpotent
 import ring_theory.nakayama
+import data.set_like.fintype
 
 /-!
 # Artinian rings and modules
@@ -55,7 +46,8 @@ class is_artinian (R M) [semiring R] [add_comm_monoid M] [module R M] : Prop :=
 (well_founded_submodule_lt [] : well_founded ((<) : submodule R M → submodule R M → Prop))
 
 section
-variables {R : Type*} {M : Type*} {P : Type*} {N : Type*}
+variables {R M P N : Type*}
+
 variables [ring R] [add_comm_group M] [add_comm_group P] [add_comm_group N]
 variables [module R M] [module R P] [module R N]
 open is_artinian
@@ -117,8 +109,9 @@ is_artinian_of_range_eq_ker
   linear_map.snd_surjective
   (linear_map.range_inl R M P)
 
-@[instance, priority 100]
-lemma is_artinian_of_fintype [fintype M] : is_artinian R M :=
+@[priority 100]
+instance is_artinian_of_finite [finite M] : is_artinian R M :=
+let ⟨_⟩ := nonempty_fintype M in by exactI
 ⟨fintype.well_founded_of_trans_of_irrefl _⟩
 
 local attribute [elab_as_eliminator] fintype.induction_empty_option
@@ -151,7 +144,8 @@ end
 
 open is_artinian submodule function
 
-section
+section ring
+
 variables {R M : Type*} [ring R] [add_comm_group M] [module R M]
 
 theorem is_artinian_iff_well_founded :
@@ -201,24 +195,26 @@ theorem monotone_stabilizes_iff_artinian :
   (∀ (f : ℕ →o (submodule R M)ᵒᵈ), ∃ n, ∀ m, n ≤ m → f n = f m) ↔ is_artinian R M :=
 by { rw is_artinian_iff_well_founded, exact well_founded.monotone_chain_condition.symm }
 
-theorem is_artinian.monotone_stabilizes [is_artinian R M] (f : ℕ →o (submodule R M)ᵒᵈ) :
-  ∃ n, ∀ m, n ≤ m → f n = f m :=
+namespace is_artinian
+
+variables [is_artinian R M]
+
+theorem monotone_stabilizes (f : ℕ →o (submodule R M)ᵒᵈ) : ∃ n, ∀ m, n ≤ m → f n = f m :=
 monotone_stabilizes_iff_artinian.mpr ‹_› f
 
 /-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
-lemma is_artinian.induction [is_artinian R M] {P : submodule R M → Prop}
-  (hgt : ∀ I, (∀ J < I, P J) → P I) (I : submodule R M) : P I :=
-well_founded.recursion (well_founded_submodule_lt R M) I hgt
+lemma induction {P : submodule R M → Prop} (hgt : ∀ I, (∀ J < I, P J) → P I) (I : submodule R M) :
+  P I :=
+(well_founded_submodule_lt R M).recursion I hgt
 
 /--
 For any endomorphism of a Artinian module, there is some nontrivial iterate
 with disjoint kernel and range.
 -/
-theorem is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top
-  [I : is_artinian R M] (f : M →ₗ[R] M) : ∃ n : ℕ, n ≠ 0 ∧ (f ^ n).ker ⊔ (f ^ n).range = ⊤ :=
+theorem exists_endomorphism_iterate_ker_sup_range_eq_top (f : M →ₗ[R] M) :
+  ∃ n : ℕ, n ≠ 0 ∧ (f ^ n).ker ⊔ (f ^ n).range = ⊤ :=
 begin
-  obtain ⟨n, w⟩ := monotone_stabilizes_iff_artinian.mpr I
-    (f.iterate_range.comp ⟨λ n, n+1, λ n m w, by linarith⟩),
+  obtain ⟨n, w⟩ := monotone_stabilizes (f.iterate_range.comp ⟨λ n, n+1, λ n m w, by linarith⟩),
   specialize w ((n + 1) + n) (by linarith),
   dsimp at w,
   refine ⟨n + 1, nat.succ_ne_zero _, _⟩,
@@ -236,28 +232,25 @@ begin
 end
 
 /-- Any injective endomorphism of an Artinian module is surjective. -/
-theorem is_artinian.surjective_of_injective_endomorphism [is_artinian R M]
-  (f : M →ₗ[R] M) (s : injective f) : surjective f :=
+theorem surjective_of_injective_endomorphism (f : M →ₗ[R] M) (s : injective f) : surjective f :=
 begin
-  obtain ⟨n, ne, w⟩ := is_artinian.exists_endomorphism_iterate_ker_sup_range_eq_top f,
+  obtain ⟨n, ne, w⟩ := exists_endomorphism_iterate_ker_sup_range_eq_top f,
   rw [linear_map.ker_eq_bot.mpr (linear_map.iterate_injective s n), bot_sup_eq,
     linear_map.range_eq_top] at w,
   exact linear_map.surjective_of_iterate_surjective ne w,
 end
 
 /-- Any injective endomorphism of an Artinian module is bijective. -/
-theorem is_artinian.bijective_of_injective_endomorphism [is_artinian R M]
-  (f : M →ₗ[R] M) (s : injective f) : bijective f :=
-⟨s, is_artinian.surjective_of_injective_endomorphism f s⟩
+theorem bijective_of_injective_endomorphism (f : M →ₗ[R] M) (s : injective f) : bijective f :=
+⟨s, surjective_of_injective_endomorphism f s⟩
 
 /--
 A sequence `f` of submodules of a artinian module,
 with the supremum `f (n+1)` and the infinum of `f 0`, ..., `f n` being ⊤,
 is eventually ⊤.
 -/
-lemma is_artinian.disjoint_partial_infs_eventually_top [I : is_artinian R M]
-  (f : ℕ → submodule R M) (h : ∀ n, disjoint
-    (partial_sups (order_dual.to_dual ∘ f) n) (order_dual.to_dual (f (n+1)))) :
+lemma disjoint_partial_infs_eventually_top (f : ℕ → submodule R M)
+  (h : ∀ n, disjoint (partial_sups (order_dual.to_dual ∘ f) n) (order_dual.to_dual (f (n+1)))) :
   ∃ n : ℕ, ∀ m, n ≤ m → f m = ⊤  :=
 begin
   -- A little off-by-one cleanup first:
@@ -269,18 +262,48 @@ begin
     { apply w,
       exact nat.succ_le_succ_iff.mp p }, },
 
-  obtain ⟨n, w⟩ := monotone_stabilizes_iff_artinian.mpr I (partial_sups (order_dual.to_dual ∘ f)),
-  exact ⟨n, λ m p, (h m).eq_bot_of_ge $ sup_eq_left.1 $ (w (m + 1) $ le_add_right p).symm.trans $
-    w m p⟩
+  obtain ⟨n, w⟩ := monotone_stabilizes (partial_sups (order_dual.to_dual ∘ f)),
+  refine ⟨n, λ m p, _⟩,
+  exact (h m).eq_bot_of_ge (sup_eq_left.1 $ (w (m + 1) $ le_add_right p).symm.trans $ w m p)
 end
 
-universe w
-variables {N : Type w} [add_comm_group N] [module R N]
+end is_artinian
+
+end ring
+
+section comm_ring
+
+variables {R : Type*} (M : Type*) [comm_ring R] [add_comm_group M] [module R M] [is_artinian R M]
+
+namespace is_artinian
+
+lemma range_smul_pow_stabilizes (r : R) : ∃ n : ℕ, ∀ m, n ≤ m →
+  (r^n • linear_map.id : M →ₗ[R] M).range = (r^m • linear_map.id).range :=
+monotone_stabilizes
+⟨λ n, (r^n • linear_map.id : M →ₗ[R] M).range,
+ λ n m h x ⟨y, hy⟩, ⟨r ^ (m - n) • y,
+   by { dsimp at ⊢ hy, rw [←smul_assoc, smul_eq_mul, ←pow_add, ←hy, add_tsub_cancel_of_le h] }⟩⟩
+
+variables {M}
+
+lemma exists_pow_succ_smul_dvd (r : R) (x : M) :
+  ∃ (n : ℕ) (y : M), r ^ n.succ • y = r ^ n • x :=
+begin
+  obtain ⟨n, hn⟩ := is_artinian.range_smul_pow_stabilizes M r,
+  simp_rw [set_like.ext_iff] at hn,
+  exact ⟨n, by simpa using hn n.succ n.le_succ (r ^ n • x)⟩,
+end
+
+end is_artinian
+
+end comm_ring
 
 -- TODO: Prove this for artinian modules
 -- /--
 -- If `M ⊕ N` embeds into `M`, for `M` noetherian over `R`, then `N` is trivial.
 -- -/
+-- universe w
+-- variables {N : Type w} [add_comm_group N] [module R N]
 -- noncomputable def is_noetherian.equiv_punit_of_prod_injective [is_noetherian R M]
 --   (f : M × N →ₗ[R] M) (i : injective f) : N ≃ₗ[R] punit.{w+1} :=
 -- begin
@@ -294,14 +317,16 @@ variables {N : Type w} [add_comm_group N] [module R N]
 --   exact submodule.bot_equiv_punit,
 -- end
 
-end
-
 /-- A ring is Artinian if it is Artinian as a module over itself.
 
 Strictly speaking, this should be called `is_left_artinian_ring` but we omit the `left_` for
 convenience in the commutative case. For a right Artinian ring, use `is_artinian Rᵐᵒᵖ R`. -/
 class is_artinian_ring (R) [ring R] extends is_artinian R R : Prop
 
+-- TODO: Can we define `is_artinian_ring` in a different way so this isn't needed?
+@[priority 100]
+instance is_artinian_ring_of_finite (R) [ring R] [finite R] : is_artinian_ring R := ⟨⟩
+
 theorem is_artinian_ring_iff {R} [ring R] : is_artinian_ring R ↔ is_artinian R R :=
 ⟨λ h, h.1, @is_artinian_ring.mk _ _⟩
 
@@ -369,22 +394,16 @@ theorem is_artinian_span_of_finite (R) {M} [ring R] [add_comm_group M] [module R
   [is_artinian_ring R] {A : set M} (hA : A.finite) : is_artinian R (submodule.span R A) :=
 is_artinian_of_fg_of_artinian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)
 
-theorem is_artinian_ring_of_surjective (R) [ring R] (S) [ring S]
-  (f : R →+* S) (hf : function.surjective f)
-  [H : is_artinian_ring R] : is_artinian_ring S :=
+theorem function.surjective.is_artinian_ring {R} [ring R] {S} [ring S] {F} [ring_hom_class F R S]
+  {f : F} (hf : function.surjective f) [H : is_artinian_ring R] : is_artinian_ring S :=
 begin
   rw [is_artinian_ring_iff, is_artinian_iff_well_founded] at H ⊢,
-  exact order_embedding.well_founded (ideal.order_embedding_of_surjective f hf) H,
+  exact (ideal.order_embedding_of_surjective f hf).well_founded H,
 end
 
-instance is_artinian_ring_range {R} [ring R] {S} [ring S] (f : R →+* S)
-  [is_artinian_ring R] : is_artinian_ring f.range :=
-is_artinian_ring_of_surjective R f.range f.range_restrict
-  f.range_restrict_surjective
-
-theorem is_artinian_ring_of_ring_equiv (R) [ring R] {S} [ring S]
-  (f : R ≃+* S) [is_artinian_ring R] : is_artinian_ring S :=
-is_artinian_ring_of_surjective R S f.to_ring_hom f.to_equiv.surjective
+instance is_artinian_ring_range {R} [ring R] {S} [ring S] (f : R →+* S) [is_artinian_ring R] :
+  is_artinian_ring f.range :=
+f.range_restrict_surjective.is_artinian_ring
 
 namespace is_artinian_ring
 
@@ -428,4 +447,35 @@ begin
   rwa [← hn (n + 1) (nat.le_succ _)]
 end
 
+section localization
+
+variables (S : submonoid R) (L : Type*) [comm_ring L] [algebra R L] [is_localization S L]
+
+include S
+
+/-- Localizing an artinian ring can only reduce the amount of elements. -/
+theorem localization_surjective : function.surjective (algebra_map R L) :=
+begin
+  intro r',
+  obtain ⟨r₁, s, rfl⟩ := is_localization.mk'_surjective S r',
+  obtain ⟨r₂, h⟩ : ∃ r : R, is_localization.mk' L 1 s = algebra_map R L r,
+  swap, { exact ⟨r₁ * r₂, by rw [is_localization.mk'_eq_mul_mk'_one, map_mul, h]⟩ },
+  obtain ⟨n, r, hr⟩ := is_artinian.exists_pow_succ_smul_dvd (s : R) (1 : R),
+  use r,
+  rw [smul_eq_mul, smul_eq_mul, pow_succ', mul_assoc] at hr,
+  apply_fun algebra_map R L at hr,
+  simp only [map_mul, ←submonoid.coe_pow] at hr,
+  rw [←is_localization.mk'_one L, is_localization.mk'_eq_iff_eq, one_mul, submonoid.coe_one,
+      ←(is_localization.map_units L (s ^ n)).mul_left_cancel hr, map_mul, mul_comm],
+end
+
+lemma localization_artinian : is_artinian_ring L :=
+(localization_surjective S L).is_artinian_ring
+
+/-- `is_artinian_ring.localization_artinian` can't be made an instance, as it would make `S` + `R`
+into metavariables. However, this is safe. -/
+instance : is_artinian_ring (localization S) := localization_artinian S _
+
+end localization
+
 end is_artinian_ring

src/ring_theory/localization/cardinality.lean

@@ -3,9 +3,8 @@ Copyright (c) 2022 Eric Rodriguez. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Rodriguez
 -/
-import ring_theory.integral_domain
-import ring_theory.localization.basic
 import set_theory.cardinal.ordinal
+import ring_theory.artinian
 
 /-!
 # Cardinality of localizations
@@ -23,7 +22,6 @@ submonoid, then your localization is trivial (see `is_localization.unique_of_zer
 
 -/
 
-
 open_locale cardinal non_zero_divisors
 
 universes u v
@@ -34,25 +32,12 @@ variables {R : Type u} [comm_ring R] (S : submonoid R) {L : Type u} [comm_ring L
           [algebra R L] [is_localization S L]
 include S
 
-/-- Localizing a finite ring can only reduce the amount of elements. -/
-lemma algebra_map_surjective_of_fintype [fintype R] : function.surjective (algebra_map R L) :=
-begin
-  classical,
-  haveI : fintype L := is_localization.fintype' S L,
-  intro x,
-  obtain ⟨⟨r, s⟩, h : x * (algebra_map R L) ↑s = (algebra_map R L) r⟩ := is_localization.surj S x,
-  obtain ⟨n, hn, hp⟩ :=
-    (is_of_fin_order_iff_pow_eq_one _).1 (exists_pow_eq_one (is_localization.map_units L s).unit),
-  rw [units.ext_iff, units.coe_pow, is_unit.unit_spec, ←nat.succ_pred_eq_of_pos hn, pow_succ] at hp,
-  exact ⟨r * s ^ (n - 1), by erw [map_mul, map_pow, ←h, mul_assoc, hp, mul_one]⟩
-end
-
 /-- A localization always has cardinality less than or equal to the base ring. -/
 lemma card_le : #L ≤ #R :=
 begin
   classical,
   casesI fintype_or_infinite R,
-  { exact cardinal.mk_le_of_surjective (algebra_map_surjective_of_fintype S) },
+  { exact cardinal.mk_le_of_surjective (is_artinian_ring.localization_surjective S _) },
   erw [←cardinal.mul_eq_self $ cardinal.aleph_0_le_mk R],
   set f : R × R → L := λ aa, is_localization.mk' _ aa.1 (if h : aa.2 ∈ S then ⟨aa.2, h⟩ else 1),
   refine @cardinal.mk_le_of_surjective _ _ f (λ a, _),