diff --git a/Mathlib.lean b/Mathlib.lean index fa3e268ef489d1..db3ba322d4c21d 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -6136,7 +6136,8 @@ public import Mathlib.RingTheory.MvPowerSeries.Order public import Mathlib.RingTheory.MvPowerSeries.PiTopology public import Mathlib.RingTheory.MvPowerSeries.Substitution public import Mathlib.RingTheory.MvPowerSeries.Trunc -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic +public import Mathlib.RingTheory.Nakayama.SpanRank public import Mathlib.RingTheory.Nilpotent.Basic public import Mathlib.RingTheory.Nilpotent.Defs public import Mathlib.RingTheory.Nilpotent.Exp diff --git a/Mathlib/Algebra/Module/SpanRank.lean b/Mathlib/Algebra/Module/SpanRank.lean index f894195d05c718..d5ef194f4d2a1b 100644 --- a/Mathlib/Algebra/Module/SpanRank.lean +++ b/Mathlib/Algebra/Module/SpanRank.lean @@ -257,21 +257,114 @@ end Submodule section map universe u -section Submodule +namespace Submodule + +section Semilinear -variable {R : Type*} {M N : Type u} [Semiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] - [Module R N] (f : M →ₗ[R] N) (p : Submodule R M) +variable {R S : Type*} {M N : Type u} [Semiring R] [Semiring S] + [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module S N] -lemma Submodule.spanRank_map_le : (p.map f).spanRank ≤ p.spanRank := by +lemma spanRank_map_le {σ : R →+* S} [RingHomSurjective σ] + (f : M →ₛₗ[σ] N) (p : Submodule R M) : (p.map f).spanRank ≤ p.spanRank := by rw [← generators_card p, FG.spanRank_le_iff_exists_span_set_card_le] exact ⟨f '' p.generators, Cardinal.mk_image_le, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦ ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩ -variable {p} in -lemma Submodule.spanFinrank_map_le_of_fg (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := +lemma spanFinrank_map_le_of_fg {σ : R →+* S} [RingHomSurjective σ] + (f : M →ₛₗ[σ] N) {p : Submodule R M} (hp : p.FG) : (p.map f).spanFinrank ≤ p.spanFinrank := (Cardinal.toNat_le_iff_le_of_lt_aleph0 (spanRank_finite_iff_fg.mpr (FG.map f hp)) (spanRank_finite_iff_fg.mpr hp)).2 (p.spanRank_map_le f) +variable {M₁ : Submodule R M} {N₁ : Submodule S N} + +lemma spanRank_le_spanRank_of_map_eq {σ : R →+* S} [RingHomSurjective σ] + (f : M →ₛₗ[σ] N) (h_map : map f M₁ = N₁) : N₁.spanRank ≤ M₁.spanRank := by + rcases exists_span_set_card_eq_spanRank M₁ with ⟨s, hscard, hsspan⟩ + rw [FG.spanRank_le_iff_exists_span_set_card_le] + use f '' s + constructor + · rw [← hscard]; exact Cardinal.mk_image_le + · rw [span_image', hsspan, h_map] + +lemma spanRank_le_spanRank_of_range_eq {σ : R →+* S} [RingHomSurjective σ] + (f : M₁ →ₛₗ[σ] N) (h_range : LinearMap.range f = N₁) : N₁.spanRank ≤ M₁.spanRank := by + -- obtain the spanning set of submodule `M₁` + rcases exists_span_set_card_eq_spanRank M₁ with ⟨s, hscard, hsspan⟩ + rw [FG.spanRank_le_iff_exists_span_set_card_le] + -- lift the set to a `Set M₁` + lift s to Set M₁ using show s ⊆ M₁ by rw [← hsspan]; exact subset_span + rw [Cardinal.mk_image_eq Subtype.val_injective] at hscard + change span R (M₁.subtype '' s) = M₁ at hsspan + rw [span_image] at hsspan + apply_fun comap M₁.subtype at hsspan + rw [comap_map_eq_of_injective (subtype_injective M₁) (span R s), comap_subtype_self] at hsspan + -- transfer the lifted set via `f` to get a spanning set of `N₁` + use f '' s + constructor + · grw [Cardinal.mk_image_le]; rw [hscard] + · rw [span_image, hsspan, map_top, h_range] + +lemma spanRank_le_spanRank_of_surjective {σ : R →+* S} [RingHomSurjective σ] + (f : M₁ →ₛₗ[σ] N₁) (h_surj : Function.Surjective f) : N₁.spanRank ≤ M₁.spanRank := by + apply spanRank_le_spanRank_of_range_eq (N₁.subtype.comp f) + rw [LinearMap.range_comp, LinearMap.range_eq_top_of_surjective f h_surj, map_top, range_subtype] + +lemma spanRank_eq_spanRank_of_addEquiv (σ : R →+* S) [RingHomSurjective σ] + (e : M₁ ≃+ N₁) (hm : ∀ (r : R) (m : M₁), e (r • m) = (σ r) • (e m)) : + M₁.spanRank = N₁.spanRank := by + -- recover the one-side linear map + let e_toLinearMap : M₁ →ₛₗ[σ] N₁ := { + toFun := e.toFun, + map_add' := e.map_add', + map_smul' := hm + } + have e_toLinearMap_apply : ∀ x, e_toLinearMap x = e x := by intro x; rfl + have e_toLinearMap_injective : Function.Injective e_toLinearMap := e.injective + have e_toLinearMap_e_symm_cancel : e_toLinearMap ∘ e.symm = id := by unfold e_toLinearMap; simp + apply le_antisymm + · -- obtain the spanning set of submodule `N₁` + rcases exists_span_set_card_eq_spanRank N₁ with ⟨s, hscard, hsspan⟩ + rw [FG.spanRank_le_iff_exists_span_set_card_le] + -- lift the set to a `Set N₁` + lift s to Set N₁ using show s ⊆ N₁ by rw [← hsspan]; exact subset_span + rw [Cardinal.mk_image_eq Subtype.val_injective] at hscard + change span S (N₁.subtype '' s) = N₁ at hsspan + rw [span_image] at hsspan + apply_fun comap N₁.subtype at hsspan + rw [comap_map_eq_of_injective (subtype_injective N₁) (span S s), comap_subtype_self] at hsspan + -- transfer the lifted set via `e.symm` to get a spanning set of `M₁` + use (M₁.subtype ∘ e.symm) '' s + constructor + · grw [Cardinal.mk_image_le]; rw [hscard] + · rw [Set.image_comp, span_image] + conv => rhs; rw [← map_subtype_top M₁] + congr + ext x; simp only [mem_top, iff_true] + rw [← apply_mem_span_image_iff_mem_span e_toLinearMap_injective, + ← Set.image_comp, e_toLinearMap_e_symm_cancel, e_toLinearMap_apply, Set.image_id, hsspan] + exact mem_top + · apply spanRank_le_spanRank_of_surjective e_toLinearMap e.surjective + +lemma spanRank_eq_spanRank_of_equiv' + (σ : R →+* S) {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] + (e : M₁ ≃ₛₗ[σ] N₁) : M₁.spanRank = N₁.spanRank := + le_antisymm + (spanRank_le_spanRank_of_surjective e.symm.toLinearMap e.symm.surjective) + (spanRank_le_spanRank_of_surjective e.toLinearMap e.surjective) + +end Semilinear + +section Linear + +variable {R : Type*} {M N : Type u} +variable [Semiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] +variable {M₁ : Submodule R M} {N₁ : Submodule R N} + +lemma spanRank_eq_spanRank_of_equiv (e : M₁ ≃ₗ[R] N₁) : M₁.spanRank = N₁.spanRank := + spanRank_eq_spanRank_of_equiv' _ e + +end Linear + end Submodule section Ideal diff --git a/Mathlib/RingTheory/Ideal/Cotangent.lean b/Mathlib/RingTheory/Ideal/Cotangent.lean index ee3bdbe8d41e7e..f3b23e0400ca21 100644 --- a/Mathlib/RingTheory/Ideal/Cotangent.lean +++ b/Mathlib/RingTheory/Ideal/Cotangent.lean @@ -5,6 +5,7 @@ Authors: Andrew Yang -/ module +public import Mathlib.Algebra.Module.SpanRank public import Mathlib.Algebra.Module.Torsion.Basic public import Mathlib.Algebra.Ring.Idempotent public import Mathlib.LinearAlgebra.Dimension.Finite @@ -13,14 +14,20 @@ public import Mathlib.LinearAlgebra.FiniteDimensional.Defs public import Mathlib.RingTheory.Filtration public import Mathlib.RingTheory.Ideal.Operations public import Mathlib.RingTheory.LocalRing.ResidueField.Basic -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic +public import Mathlib.RingTheory.Nakayama.SpanRank /-! # The module `I ⧸ I ^ 2` In this file, we provide special API support for the module `I ⧸ I ^ 2`. The official -definition is a quotient module of `I`, but the alternative definition as an ideal of `R ⧸ I ^ 2` is -also given, and the two are `R`-equivalent as in `Ideal.cotangentEquivIdeal`. +definition is a quotient module of `I`, but there are two alternative definitions: + +- as an ideal of `R ⧸ I ^ 2`, +- as the image of `I` under the `R`-module quotient map `R → R / (I ^ 2)` + +They are shown to be `R`-linear equivalent to the official definition via +`Ideal.cotangentEquivIdeal` and `Ideal.cotangentEquivSubmodule` respectively. Additional support is also given to the cotangent space `m ⧸ m ^ 2` of a local ring. @@ -219,6 +226,19 @@ lemma mapCotangent_toCotangent (I₁ : Ideal A) (I₂ : Ideal B) (f : A →ₐ[R] B) (h : I₁ ≤ I₂.comap f) (x : I₁) : Ideal.mapCotangent I₁ I₂ f h (Ideal.toCotangent I₁ x) = Ideal.toCotangent I₂ ⟨f x, h x.2⟩ := rfl +/-- `I ⧸ I ^ 2` as the image of `I` under the `R`-module quotient map `R → R / (I ^ 2)`. -/ +def cotangentSubmodule (I : Ideal R) : Submodule R (R ⧸ I ^ 2) := + Submodule.map (I ^ 2).mkQ I + +/-- +The linear equivalence of the two definitions of `I / I ^ 2`, +either as a quotient of `I` by its submodule `I • ⊤`, +or the image of `I` under the `R`-module quotient map `R → R / (I ^ 2)`. +-/ +noncomputable def cotangentEquivSubmodule (I : Ideal R) : + I.Cotangent ≃ₗ[R] (Submodule.map (I ^ 2).mkQ I) := by + rw [pow_two]; exact Submodule.quotientIdealSubmoduleEquivMap I I + end Ideal namespace IsLocalRing @@ -264,6 +284,15 @@ lemma CotangentSpace.span_image_eq_top_iff [IsNoetherianRing R] {s : Set (maxima · simp only [Ideal.toCotangent_apply, Submodule.restrictScalars_top, Submodule.map_span] · exact Ideal.Quotient.mk_surjective +/-- +In a local ring, the dimension of the cotangent space is equal to +the span rank of the maximal ideal, if the maximal ideal is finitely generated. +-/ +theorem rank_cotangentSpace_eq_spanrank_maximalIdeal (hm : (maximalIdeal R).FG) : + Module.rank (ResidueField R) (CotangentSpace R) = (maximalIdeal R).spanRank := by + rw [Submodule.spanRank_eq_spanRank_quotient_ideal_quotientIdealSubmodule + hm (maximalIdeal_le_jacobson _), Submodule.rank_eq_spanRank_of_free] + open Module lemma finrank_cotangentSpace_eq_zero_iff [IsNoetherianRing R] : diff --git a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean index 9fc2c0018e22c4..2061162a6b52ab 100644 --- a/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean +++ b/Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean @@ -9,7 +9,7 @@ public import Mathlib.RingTheory.HopkinsLevitzki public import Mathlib.RingTheory.Ideal.GoingDown public import Mathlib.RingTheory.Ideal.Height public import Mathlib.RingTheory.Localization.Submodule -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic /-! # Krull's Height Theorem diff --git a/Mathlib/RingTheory/LocalRing/Module.lean b/Mathlib/RingTheory/LocalRing/Module.lean index 221f6cbd2021c6..0ec6c9f18c70b6 100644 --- a/Mathlib/RingTheory/LocalRing/Module.lean +++ b/Mathlib/RingTheory/LocalRing/Module.lean @@ -14,7 +14,7 @@ public import Mathlib.RingTheory.Ideal.Quotient.ChineseRemainder public import Mathlib.RingTheory.LocalProperties.Exactness public import Mathlib.RingTheory.LocalRing.ResidueField.Basic public import Mathlib.RingTheory.LocalRing.ResidueField.Ideal -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic public import Mathlib.RingTheory.Support /-! diff --git a/Mathlib/RingTheory/LocalRing/Quotient.lean b/Mathlib/RingTheory/LocalRing/Quotient.lean index 7c7a454fc1bbc6..e69228691ac34a 100644 --- a/Mathlib/RingTheory/LocalRing/Quotient.lean +++ b/Mathlib/RingTheory/LocalRing/Quotient.lean @@ -13,7 +13,7 @@ public import Mathlib.RingTheory.Ideal.Over public import Mathlib.RingTheory.Ideal.Quotient.Index public import Mathlib.RingTheory.LocalRing.ResidueField.Defs public import Mathlib.RingTheory.LocalRing.RingHom.Basic -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic /-! diff --git a/Mathlib/RingTheory/Nakayama.lean b/Mathlib/RingTheory/Nakayama/Basic.lean similarity index 67% rename from Mathlib/RingTheory/Nakayama.lean rename to Mathlib/RingTheory/Nakayama/Basic.lean index 4079c8d0325610..cd7738c5d1915e 100644 --- a/Mathlib/RingTheory/Nakayama.lean +++ b/Mathlib/RingTheory/Nakayama/Basic.lean @@ -29,7 +29,7 @@ This file contains some alternative statements of Nakayama's Lemma as found in * `Submodule.smul_le_of_le_smul_of_le_jacobson_bot` - Statement (4) in [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV). -* `Submodule.le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot` - Statement (8) in +* `Submodule.exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot` - Statement (8) in [Stacks: Nakayama's Lemma](https://stacks.math.columbia.edu/tag/00DV). Note that a version of Statement (1) in @@ -184,10 +184,13 @@ lemma exists_sub_one_mem_and_smul_le_of_fg_of_le_sup {I : Ideal R} | add _ _ _ _ hx hy => exact N.add_mem hx hy | zero => exact N.zero_mem -/-- **Nakayama's Lemma** - Statement (8) in -[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). -/ -@[stacks 00DV "(8)"] -theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot +/-- +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`t` is a set of `M` whose span image under the quotient map `M → M / (I • N)` +contains the image of `N`, then `N` is contained in the span of `t`. +-/ +lemma le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot {I : Ideal R} {N : Submodule R M} {t : Set M} (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (htspan : map (I • N).mkQ N ≤ map (I • N).mkQ (span R t)) : N ≤ span R t := by @@ -198,4 +201,96 @@ theorem le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot grw [sup_comm, ← htspan] simp only [le_sup_right] +/-- +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`t` is a set of `M` whose span image under the quotient map `M → M / (I • N)` +is the image of `N`, then `t` spans `N`. +-/ +lemma span_eq_of_map_mkQ_span_eq_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} {t : Set M} + (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (htspan : map (I • N).mkQ (span R t) = map (I • N).mkQ N) : + span R t = N := by + symm; apply le_antisymm + · apply le_span_of_map_mkQ_le_map_mkQ_span_of_le_jacobson_bot hN hIjac htspan.ge + · apply_fun comap (I • N).mkQ at htspan + simp only [comap_map_mkQ, smul_le_right, sup_of_le_right] at htspan + rw [← htspan]; apply le_sup_right + +/- +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`s` is a set of `M / (I • N)` that spans the quotient image of `N`, +then any set `t` of `M` in bijection with `s` via the quotient map spans `N`. +-/ +theorem span_eq_of_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} (s : Set (M ⧸ (I • N))) + (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (hsspan : span R s = map (I • N).mkQ N) : + ∀ (t : Set M) (e : t ≃ s), (∀ x : t, e x = (I • N).mkQ x) → span R t = N := by + intro t e he + apply span_eq_of_map_mkQ_span_eq_map_mkQ_of_le_jacobson_bot hN hIjac + rw [← hsspan, map_span] + congr; ext y + constructor + · rintro ⟨x, hx, rfl⟩; rw [← he ⟨x, hx⟩]; simp + · intro hy; use (e.symm ⟨y, hy⟩).val + exact ⟨by simp, by rw [← he]; simp⟩ + +/-- +**Nakayama's Lemma** - Statement (8) in +[Stacks 00DV](https://stacks.math.columbia.edu/tag/00DV). + +If `N` is a finitely generated `R`-submodule of `M`, +`I` is an ideal contained in the Jacobson radical of `R`, +`s` is a set of `M / (I • N)` that spans the quotient image of `N`, +then there exists a spanning set `t` of `N` in bijection with `s` via the quotient map. +-/ +@[stacks 00DV "(8)"] +theorem exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} (s : Set (M ⧸ (I • N))) + (hN : N.FG) (hIjac : I ≤ jacobson ⊥) (hsspan : span R s = map (I • N).mkQ N) : + ∃ (t : Set M) (e : t ≃ s), (∀ x : t, e x = (I • N).mkQ x) ∧ span R t = N := by + let t := Quotient.out '' s + let e : t ≃ s := { + toFun := by intro ⟨x, hx⟩; use (I • N).mkQ x; rcases hx with ⟨y, hy, rfl⟩; simpa using hy + invFun := by intro ⟨y, hy⟩; use Quotient.out y; simpa [t] using hy + left_inv := by rintro ⟨x, y, hy, rfl⟩; simp + right_inv := by intro ⟨y, hy⟩; simp + } + use t, e + constructor + · intros; simp [e] + · apply span_eq_of_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + s hN hIjac hsspan t e (by intros; simp [e]) + +/-- +The linear equivalence of the two definitions of `N / I • N`, +either as a quotient of `N` by its submodule `I • ⊤`, +or the image of `N` under the `R`-module quotient map `M → M / (I • N)`. +-/ +noncomputable def quotientIdealSubmoduleEquivMap (N : Submodule R M) (I : Ideal R) : + (N ⧸ (I • ⊤ : Submodule R N)) ≃ₗ[R] (map (I • N).mkQ N) := by + -- TODO: find a better place for this equivalence + refine LinearEquiv.ofBijective ?_ ⟨?_, ?_⟩ + · refine Submodule.liftQ _ ?_ ?_ + · exact { + toFun x := by + rcases x with ⟨x, hx⟩ + use ((I • N).mkQ x), x, hx + map_add' := by simp + map_smul' := by simp + } + · intro x hx + rw [mem_smul_top_iff] at hx + simp [hx] + · rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot'] + intro x hx + induction x using Submodule.Quotient.induction_on with | H x => + simp only [mkQ_apply, liftQ_apply, LinearMap.coe_mk, AddHom.coe_mk, mk_eq_zero, + Quotient.mk_eq_zero] at hx + simp only [Quotient.mk_eq_zero, mem_smul_top_iff, hx] + · rintro ⟨_, ⟨x, hx, rfl⟩⟩ + use Quotient.mk ⟨x, hx⟩ + simp + end Submodule diff --git a/Mathlib/RingTheory/Nakayama/SpanRank.lean b/Mathlib/RingTheory/Nakayama/SpanRank.lean new file mode 100644 index 00000000000000..b0516def8bef39 --- /dev/null +++ b/Mathlib/RingTheory/Nakayama/SpanRank.lean @@ -0,0 +1,76 @@ +/- +Copyright (c) 2025 Xingyu Zhong. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Xingyu Zhong +-/ +module + +public import Mathlib.RingTheory.Nakayama.Basic +public import Mathlib.Algebra.Module.SpanRank +public import Mathlib.Algebra.Module.Torsion.Basic + +/-! +# Nakayama's lemma and `Submodule.spanRank` + +This file states some versions of Nakayama's lemma in terms of `Submodule.spanRank`. +-/ + +@[expose] public section + +variable {R M : Type*} [CommRing R] [AddCommGroup M] [Module R M] + +namespace Submodule + +/-- +The span rank of an `R`-submodule `N` of `M` is equal to +the span rank of the `R`-submodule `N / (I • N)` of `M / (I • N)`, +provided that `N` is finitely generated and `I` is contained in the Jacobson radical of `R`. + +Here `N / (I • N)` is the image of `N` under the `R`-module quotient map `M → M / (I • N)`. +-/ +theorem spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot + {I : Ideal R} {N : Submodule R M} + (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : + N.spanRank = (map (I • N).mkQ N).spanRank := by + apply le_antisymm + · rcases exists_span_set_card_eq_spanRank (map (I • N).mkQ N) with ⟨s, ⟨hscard, hsspan⟩⟩ + rcases exists_set_equiv_eq_mkQ_span_of_span_eq_map_mkQ_of_le_jacobson_bot + s hN hIjac hsspan with ⟨t, e, heq, htspan⟩ + rw [FG.spanRank_le_iff_exists_span_set_card_le] + use t, (by rw [← hscard, Equiv.cardinal_eq]; exact e), htspan + · exact spanRank_le_spanRank_of_map_eq (mkQ (I • N)) (by dsimp) + +/-- +The span rank of an `R`-submodule `N` of `M` is equal to +the span rank of the `R`-module `N / (I • N)`, +provided that `N` is finitely generated and `I` is contained in the Jacobson radical of `R`. + +Here `N / (I • N)` is obtained by directly taking the quotient of `N` by the its submodule `I • ⊤`. +-/ +theorem spanRank_eq_spanRank_quotientIdealSubmodule + {I : Ideal R} {N : Submodule R M} + (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : + N.spanRank = (⊤ : Submodule R (N ⧸ (I • ⊤ : Submodule R N))).spanRank := by + rw [spanRank_eq_spanRank_map_mkQ_of_le_jacobson_bot hN hIjac] + apply spanRank_eq_spanRank_of_equiv + symm + exact LinearEquiv.trans + (Submodule.topEquiv : _ ≃ₗ[R] (N ⧸ (I • ⊤ : Submodule R N))) + (quotientIdealSubmoduleEquivMap N I) + +/-- +The span rank of an `R`-submodule `N` of `M` is equal to +the span rank of the `R / I`-module `N / (I • N)`, +provided that `N` is finitely generated and `I` is contained in the Jacobson radical of `R`. + +Here `N / (I • N)` is obtained by directly taking the quotient of `N` by the its submodule `I • ⊤`. +-/ +theorem spanRank_eq_spanRank_quotient_ideal_quotientIdealSubmodule + {I : Ideal R} {N : Submodule R M} + (hN : N.FG) (hIjac : I ≤ Ideal.jacobson ⊥) : + N.spanRank = (⊤ : Submodule (R ⧸ I) (N ⧸ (I • ⊤ : Submodule R N))).spanRank := by + rw [spanRank_eq_spanRank_quotientIdealSubmodule hN hIjac] + exact spanRank_eq_spanRank_of_addEquiv (Ideal.Quotient.mk I) + (LinearEquiv.toAddEquiv (LinearEquiv.refl R _)) (by intros; rfl) + +end Submodule diff --git a/Mathlib/RingTheory/Regular/RegularSequence.lean b/Mathlib/RingTheory/Regular/RegularSequence.lean index d8d713cb8d654f..383a8256446d60 100644 --- a/Mathlib/RingTheory/Regular/RegularSequence.lean +++ b/Mathlib/RingTheory/Regular/RegularSequence.lean @@ -7,7 +7,7 @@ module public import Mathlib.RingTheory.Artinian.Module public import Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic public import Mathlib.RingTheory.Regular.IsSMulRegular /-! diff --git a/Mathlib/RingTheory/Support.lean b/Mathlib/RingTheory/Support.lean index 3c761758e71ee3..76fe1670bf1131 100644 --- a/Mathlib/RingTheory/Support.lean +++ b/Mathlib/RingTheory/Support.lean @@ -7,7 +7,7 @@ module public import Mathlib.RingTheory.Ideal.Colon public import Mathlib.RingTheory.Localization.Finiteness -public import Mathlib.RingTheory.Nakayama +public import Mathlib.RingTheory.Nakayama.Basic public import Mathlib.RingTheory.QuotSMulTop public import Mathlib.RingTheory.Spectrum.Prime.Basic