feat(Mathlib/RingTheory/Ideal/Cotangent): dimension of cotangent spaces

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

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

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] :

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

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
 
 /-!

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
 
 /-!
 

Mathlib/RingTheory/Nakayama.lean → 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