feat(Ideal/IsPrincipalPowQuotient): R/I equiv I^n/I^(n+1) (#15426)

Co-authored-by: Yakov Pechersky <ffxen158@gmail.com>

Author: pechersky

Mathlib.lean

@@ -4048,6 +4048,7 @@ import Mathlib.RingTheory.Ideal.Cotangent
 import Mathlib.RingTheory.Ideal.IdempotentFG
 import Mathlib.RingTheory.Ideal.IsPrimary
 import Mathlib.RingTheory.Ideal.IsPrincipal
+import Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient
 import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.Ideal.MinimalPrime
 import Mathlib.RingTheory.Ideal.Norm

Mathlib/RingTheory/Ideal/IsPrincipalPowQuotient.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2024 Yakov Pechersky. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yakov Pechersky
+-/
+import Mathlib.LinearAlgebra.Isomorphisms
+import Mathlib.RingTheory.Ideal.Operations
+import Mathlib.RingTheory.Ideal.Quotient
+
+/-!
+# Quotients of powers of principal ideals
+
+This file deals with taking quotients of powers of principal ideals.
+
+## Main definitions and results
+
+* `Ideal.quotEquivPowQuotPowSucc`: for a principal ideal `I`, `R ⧸ I ≃ₗ[R] I ^ n ⧸ I ^ (n + 1)`
+
+## Implementation details
+
+At site of usage, calling `LinearEquiv.toEquiv` can cause timeouts in the search for a complex
+synthesis like `Module 𝒪[K] 𝓀[k]`, so the plain equiv versions are provided.
+
+These equivs are defined here as opposed to in the quotients file since they cannot be
+formed as ring equivs.
+
+-/
+
+
+namespace Ideal
+
+section IsPrincipal
+
+variable {R : Type*} [CommRing R] [IsDomain R] {I : Ideal R}
+
+/-- For a principal ideal `I`, `R ⧸ I ≃ₗ[R] I ^ n ⧸ I ^ (n + 1)`. To convert into a form
+that uses the ideal of `R ⧸ I ^ (n + 1)`, compose with
+`Ideal.powQuotPowSuccLinearEquivMapMkPowSuccPow`. -/
+noncomputable
+def quotEquivPowQuotPowSucc (h : I.IsPrincipal) (h': I ≠ ⊥) (n : ℕ) :
+    (R ⧸ I) ≃ₗ[R] (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) := by
+  let f : (I ^ n : Ideal R) →ₗ[R] (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) :=
+    Submodule.mkQ _
+  let ϖ := h.principal'.choose
+  have hI : I = Ideal.span {ϖ} := h.principal'.choose_spec
+  have hϖ : ϖ ^ n ∈ I ^ n := hI ▸ (Ideal.pow_mem_pow (Ideal.mem_span_singleton_self _) n)
+  let g : R →ₗ[R] (I ^ n : Ideal R) := (LinearMap.mulRight R ϖ^n).codRestrict _ fun x ↦ by
+    simp only [LinearMap.pow_mulRight, LinearMap.mulRight_apply, Ideal.submodule_span_eq]
+    -- TODO: change argument of Ideal.pow_mem_of_mem
+    exact Ideal.mul_mem_left _ _ hϖ
+  have : I = LinearMap.ker (f.comp g) := by
+    ext x
+    simp only [LinearMap.codRestrict, LinearMap.pow_mulRight, LinearMap.mulRight_apply,
+      LinearMap.mem_ker, LinearMap.coe_comp, LinearMap.coe_mk, AddHom.coe_mk, Function.comp_apply,
+      Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero, Submodule.mem_smul_top_iff, smul_eq_mul,
+      f, g]
+    constructor <;> intro hx
+    · exact Submodule.mul_mem_mul hx hϖ
+    · rw [← pow_succ', hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
+      obtain ⟨y, hy⟩ := hx
+      rw [mul_comm, pow_succ, mul_assoc, mul_right_inj' (pow_ne_zero _ _)] at hy
+      · rw [hI, Ideal.mem_span_singleton]
+        exact ⟨y, hy⟩
+      · contrapose! h'
+        rw [hI, h', Ideal.span_singleton_eq_bot]
+  let e : (R ⧸ I) ≃ₗ[R] R ⧸ (LinearMap.ker (f.comp g)) :=
+    Submodule.quotEquivOfEq I (LinearMap.ker (f ∘ₗ g)) this
+  refine e.trans ((f.comp g).quotKerEquivOfSurjective ?_)
+  refine (Submodule.mkQ_surjective _).comp ?_
+  rintro ⟨x, hx⟩
+  rw [hI, Ideal.span_singleton_pow, Ideal.mem_span_singleton] at hx
+  refine hx.imp ?_
+  simp [g, LinearMap.codRestrict, eq_comm, mul_comm]
+
+/-- For a principal ideal `I`, `R ⧸ I ≃ I ^ n ⧸ I ^ (n + 1)`. Supplied as a plain equiv to bypass
+typeclass synthesis issues on complex `Module` goals.  To convert into a form
+that uses the ideal of `R ⧸ I ^ (n + 1)`, compose with
+`Ideal.powQuotPowSuccEquivMapMkPowSuccPow`. -/
+noncomputable
+def quotEquivPowQuotPowSuccEquiv (h : I.IsPrincipal) (h': I ≠ ⊥) (n : ℕ) :
+    (R ⧸ I) ≃ (I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R)) :=
+  quotEquivPowQuotPowSucc h h' n
+
+end IsPrincipal
+
+end Ideal

Mathlib/RingTheory/Ideal/QuotientOperations.lean

@@ -938,3 +938,47 @@ theorem quotQuotEquivQuotOfLE_symm_comp_mkₐ (h : I ≤ J) :
 
 end AlgebraQuotient
 end DoubleQuot
+
+namespace Ideal
+
+section PowQuot
+
+variable {R : Type*} [CommRing R] (I : Ideal R) (n : ℕ)
+
+/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
+This definition gives the `R`-linear equivalence between the two. -/
+noncomputable
+def powQuotPowSuccLinearEquivMapMkPowSuccPow :
+    ((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃ₗ[R]
+    Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n) := by
+  refine { LinearMap.codRestrict
+    (Submodule.restrictScalars _ (Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n)))
+    (Submodule.mapQ (I • ⊤) (I ^ (n + 1)) (Submodule.subtype (I ^ n)) ?_) ?_,
+    Equiv.ofBijective _ ⟨?_, ?_⟩ with }
+  · intro
+    simp [Submodule.mem_smul_top_iff, pow_succ']
+  · intro x
+    obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ x
+    simp [Ideal.mem_sup_left hy]
+  · intro a b
+    obtain ⟨⟨x, hx⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ a
+    obtain ⟨⟨y, hy⟩, rfl⟩ := Submodule.Quotient.mk_surjective _ b
+    simp [Ideal.Quotient.eq, Submodule.Quotient.eq, Submodule.mem_smul_top_iff, pow_succ']
+  · intro ⟨x, hx⟩
+    rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective] at hx
+    obtain ⟨y, hy, rfl⟩ := hx
+    refine ⟨Submodule.Quotient.mk ⟨y, hy⟩, ?_⟩
+    simp
+
+/-- `I ^ n ⧸ I ^ (n + 1)` can be viewed as a quotient module and as ideal of `R ⧸ I ^ (n + 1)`.
+This definition gives the equivalence between the two, instead of the `R`-linear equivalence,
+to bypass typeclass synthesis issues on complex `Module` goals. -/
+noncomputable
+def powQuotPowSuccEquivMapMkPowSuccPow :
+    ((I ^ n : Ideal R) ⧸ (I • ⊤ : Submodule R (I ^ n : Ideal R))) ≃
+    Ideal.map (Ideal.Quotient.mk (I ^ (n + 1))) (I ^ n) :=
+  powQuotPowSuccLinearEquivMapMkPowSuccPow I n
+
+end PowQuot
+
+end Ideal