NYLL
Module

RegularLocalFiniteFreeResolution.lean

Nyll.SchemeTheory.RingTheory.RegularLocalFiniteFreeResolution
14 declarations indexed from sourceView source ↗

Module documentation

Finite free resolutions over regular local rings

The depth argument and the resolution construction are extracted from the attributed source above, independently of its subsequent localization and unique factorization argument. The ring hypothesis here is only regular local.

Imports7
Imported by2

Declarations

lemma

length_le_depth

L40 ↗
SchemeTheory.RegularLocalResolution.P2mAB.DepthLemma.length_le_depth
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
lemma length_le_depth {M : Type*} [AddCommGroup M] [Module R M] {rs : List R}
    (h1 : IsWeaklyRegular M rs) (h2 : ∀ r ∈ rs, r ∈ maximalIdeal R) :
    (rs.length : ℕ∞) ≤ Module.depth R M
lemma

exists_isSMulRegular_of_one_le_depth

L45 ↗
SchemeTheory.RegularLocalResolution.P2mAB.DepthLemma.exists_isSMulRegular_of_one_le_depth
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
lemma exists_isSMulRegular_of_one_le_depth {M : Type*} [AddCommGroup M] [Module R M]
    (h : 1 ≤ Module.depth R M) : ∃ x ∈ maximalIdeal R, IsSMulRegular M x
lemma

not_isAssociatedPrime_of_isSMulRegular

L59 ↗
SchemeTheory.RegularLocalResolution.P2mAB.DepthLemma.not_isAssociatedPrime_of_isSMulRegular
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
lemma not_isAssociatedPrime_of_isSMulRegular [IsNoetherianRing R]
    {M : Type*} [AddCommGroup M] [Module R M]
    {x : R} (hx : x ∈ maximalIdeal R) (hreg : IsSMulRegular M x) :
    ¬ IsAssociatedPrime (maximalIdeal R) M
theorem

core

L74 ↗
SchemeTheory.RegularLocalResolution.P2mAB.DepthLemma.core
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem core [IsNoetherianRing R] (n : ℕ) :
    ∀ {K F M : Type*} [AddCommGroup K] [Module R K] [AddCommGroup F] [Module R F]
      [Module.Finite R F] [AddCommGroup M] [Module R M]
      (f : K →ₗ[R] F) (g : F →ₗ[R] M), Function.Injective f → Function.Exact f g →
      Function.Surjective g →
      (n : ℕ∞) ≤ Module.depth R F → (n : ℕ∞) ≤ Module.depth R M + 1 →
      (n : ℕ∞) ≤ Module.depth R K
theorem

min_depth_depth_add_one_le_depth_of_exact

L147 ↗
SchemeTheory.RegularLocalResolution.P2mAB.DepthLemma.min_depth_depth_add_one_le_depth_of_exact
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace DepthLemma
variable {R : Type*} [CommRing R] [IsLocalRing R]
Lean source · statement
theorem min_depth_depth_add_one_le_depth_of_exact
    {R : Type*} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
    {K F M : Type*} [AddCommGroup K] [Module R K] [AddCommGroup F] [Module R F]
    [Module.Finite R F] [AddCommGroup M] [Module R M]
    (f : K →ₗ[R] F) (g : F →ₗ[R] M) (hf : Function.Injective f) (hfg : Function.Exact f g)
    (hg : Function.Surjective g) :
    min (Module.depth R F) (Module.depth R M + 1) ≤ Module.depth R K
def

HasFFR

L176 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.HasFFR
Documentation

The module admits a finite free resolution of length at most the specified bound.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
Lean source · full declaration
def HasFFR (R : Type u) [CommRing R] : ℕ → (K : Type u) → [AddCommGroup K] → [Module R K] → Prop
  | 0, K, _, _ => Module.Finite R K ∧ Module.Free R K
  | n + 1, K, _, _ => ∃ (k : ℕ) (f : (Fin k → R) →ₗ[R] K),
      Function.Surjective f ∧ HasFFR R n (LinearMap.ker f)
lemma

hasFFR_zero_iff

L183 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.hasFFR_zero_iff
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · statement
lemma hasFFR_zero_iff (K : Type u) [AddCommGroup K] [Module R K] :
    HasFFR R 0 K ↔ Module.Finite R K ∧ Module.Free R K
lemma

hasFFR_succ_iff

L186 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.hasFFR_succ_iff
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · statement
lemma hasFFR_succ_iff (n : ℕ) (K : Type u) [AddCommGroup K] [Module R K] :
    HasFFR R (n + 1) K ↔ ∃ (k : ℕ) (f : (Fin k → R) →ₗ[R] K),
      Function.Surjective f ∧ HasFFR R n (LinearMap.ker f)
lemma

length_le_depth

L194 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.length_le_depth
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section depth
variable [IsLocalRing R]
Lean source · statement
lemma length_le_depth {M : Type*} [AddCommGroup M] [Module R M] {rs : List R}
    (h1 : IsWeaklyRegular M rs) (h2 : ∀ r ∈ rs, r ∈ maximalIdeal R) :
    (rs.length : ℕ∞) ≤ Module.depth R M
lemma

exists_isWeaklyRegular_of_le_depth

L199 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.exists_isWeaklyRegular_of_le_depth
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section depth
variable [IsLocalRing R]
Lean source · statement
lemma exists_isWeaklyRegular_of_le_depth {M : Type*} [AddCommGroup M] [Module R M] (n : ℕ)
    (h : (n : ℕ∞) ≤ Module.depth R M) :
    ∃ rs : List R, IsWeaklyRegular M rs ∧ (∀ r ∈ rs, r ∈ maximalIdeal R) ∧ n ≤ rs.length
lemma

depth_eq_top_of_subsingleton

L217 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.depth_eq_top_of_subsingleton
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section depth
variable [IsLocalRing R]
Lean source · statement
lemma depth_eq_top_of_subsingleton (M : Type*) [AddCommGroup M] [Module R M] [Subsingleton M] :
    Module.depth R M = ⊤
lemma

le_depth_pi

L232 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.le_depth_pi
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
Lean source · statement
lemma le_depth_pi [IsRegularLocalRing R] (d : ℕ) (hd : ringKrullDim R = d) (k : ℕ) :
    (d : ℕ∞) ≤ Module.depth R (Fin k → R)
theorem

hasFFR_of_le_depth

L250 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.hasFFR_of_le_depth
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section syzygy
variable [IsRegularLocalRing R]
Lean source · statement
theorem hasFFR_of_le_depth (d : ℕ) (hd : ringKrullDim R = d) :
    ∀ n : ℕ, n ≤ d → ∀ (K : Type u) [AddCommGroup K] [Module R K] [Module.Finite R K],
      ((d - n : ℕ) : ℕ∞) ≤ Module.depth R K → HasFFR R n K
theorem

hasFFR

L285 ↗
SchemeTheory.RegularLocalResolution.P2mAB.StablyFree.hasFFR
Source context 8 commands

Surrounding namespaces, section variables, and local commands at this declaration.

open IsLocalRing RingTheory.Sequence
universe u
namespace SchemeTheory.RegularLocalResolution
namespace P2mAB
namespace StablyFree
variable {R : Type u} [CommRing R]
section syzygy
variable [IsRegularLocalRing R]
Lean source · statement
theorem hasFFR (d : ℕ) (hd : ringKrullDim R = d) (K : Type u) [AddCommGroup K] [Module R K]
    [Module.Finite R K] : HasFFR R d K

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.