ModuleAlgebra.lean`

34 declarations, 0 contain sorry, 0 declared as axioms

Height-one membership into free targets, minimal covers, graded Nakayama, reverse projectivity, saturated edge kernels and strict Hilbert detection.

theorem OAI.KLInvariance.EdgeLattice.finsupp_divide line 17

theorem OAI.KLInvariance.EdgeLattice.basis_divide line 35

Source documentation

In a free module, divisibility can be checked on a basis.

private theorem basis_divide {E : Type*} [AddCommGroup E] [Module R E]
    {ι : Type*} (b : Module.Basis ι R E) (p : R) (m : E)
    (h : ∀ i, p ∣ b.repr m i) : ∃ n : E, p • n = m := by
…

theorem OAI.KLInvariance.EdgeLattice.mem_of_prime_local_membership line 45
Source documentation
Scalar-denominator formulation of the height-one intersection property. A generic-span witness and local denominators away from each prime element force membership in a free target, with no reflexivity hypothesis on a source.
```
theorem mem_of_prime_local_membership
    {E : Type*} [AddCommGroup E] [Module R E] [Module.IsTorsionFree R E]
    (M : Submodule R E) [Module.Free R M] (x : E)
    (hgeneric : ∃ c : R, c ≠ 0 ∧ c • x ∈ M)
    (hlocal : ∀ p : R, Prime p → ∃ a : R, ¬p ∣ a ∧ a • x ∈ M) : x ∈ M := by
…
```

theorem OAI.KLInvariance.EdgeLattice.exists_denominator_of_localized_mem line 89

Source documentation

A localization membership can be written with a scalar denominator outside its prime, without requiring a choice of basis in the ambient module.

theorem exists_denominator_of_localized_mem
    {E : Type*} [AddCommGroup E] [Module R E]
    (M : Submodule R E) (P : Ideal R) [P.IsPrime] (x : E)
    (hx : LocalizedModule.mk x (1 : P.primeCompl) ∈ M.localized P.primeCompl) :
    ∃ a : R, a ∉ P ∧ a • x ∈ M := by
…

theorem OAI.KLInvariance.EdgeLattice.mem_iff_localized_at_height_one line 106

theorem OAI.KLInvariance.EdgeLattice.eq_iInf_height_one_localizations line 129

Source documentation

Equality with the intersection of preimages of all height-one localizations. It includes the field case: an empty height-one intersection is the full module.

theorem eq_iInf_height_one_localizations
    [IsNoetherianRing R]
    {E : Type*} [AddCommGroup E] [Module R E] [Module.IsTorsionFree R E]
    (M : Submodule R E) [Module.Free R M]
    (hgeneric : ∀ x : E, ∃ c : R, c ≠ 0 ∧ c • x ∈ M) :
    M = ⨅ (P : PrimeSpectrum R) (_ : P.asIdeal.height = 1),
      ((M.localized P.asIdeal.primeCompl).restrictScalars R).comap
        (LocalizedModule.mkLinearMap P.asIdeal.primeCompl E) := by
…

theorem OAI.KLInvariance.LocalCover.lift_surjective line 165

Source documentation

A lift through a minimal free cover is automatically surjective. This is the exact Nakayama step of plane-localized BMP decomposition.

theorem lift_surjective [Module.Finite R P]
    (π : P →ₗ[R] N) (φ : B →ₗ[R] N) (g : B →ₗ[R] P)
    (hφ : Function.Surjective φ) (hg : π.comp g = φ)
    (hmin : LinearMap.ker π ≤ IsLocalRing.maximalIdeal R • (⊤ : Submodule R P)) :
    Function.Surjective g := by
…

def OAI.KLInvariance.LocalCover.splitEquiv line 184
Source documentation
An explicit linear equivalence for a split surjection, with the kernel as the second summand. It is used below to produce the local sheaf summand.
```
noncomputable def splitEquiv (g : B →ₗ[R] P) (s : P →ₗ[R] B)
    (hs : g.comp s = LinearMap.id) : B ≃ₗ[R] P × LinearMap.ker g := by
…
```

theorem OAI.KLInvariance.LocalCover.exists_split_minimal_cover line 206

Source documentation

The full minimal-cover splitting required at each descending vertex. The new kernel is proved finite free over the local ring, not introduced as a free summand hypothesis.

theorem exists_split_minimal_cover [Module.Free R B] [Module.Finite R B]
    [Module.Free R P] [Module.Finite R P]
    (π : P →ₗ[R] N) (φ : B →ₗ[R] N)
    (hπ : Function.Surjective π) (hφ : Function.Surjective φ)
    (hmin : LinearMap.ker π ≤ IsLocalRing.maximalIdeal R • (⊤ : Submodule R P)) :
    ∃ (g : B →ₗ[R] P) (e : B ≃ₗ[R] P × LinearMap.ker g),
      Function.Surjective g ∧ π.comp g = φ ∧
      Module.Free R (LinearMap.ker g) ∧ Module.Finite R (LinearMap.ker g) ∧
      ∀ b, (e b).1 = g b ∧ π (e b).1 = φ b := by
…

theorem OAI.KLInvariance.ReverseFiltration.kernel_projective_of_presentation line 246

Source documentation

The kernel of a surjection from a projective module is projective if the target has an actual length-one projective presentation.

theorem kernel_projective_of_presentation
    [Module.Projective R F] [Module.Projective R E]
    (f : F →ₗ[R] I) (g : E →ₗ[R] I)
    (hf : Function.Surjective f) (hg : Function.Surjective g)
    [Module.Projective R (LinearMap.ker g)] :
    Module.Projective R (LinearMap.ker f) := by
…

def OAI.KLInvariance.Graded.component line 280
def OAI.KLInvariance.Graded.positiveIdeal line 286
theorem OAI.KLInvariance.Graded.subsingleton_of_positiveIdeal_smul_eq_top line 293
Source documentation
A bounded-below internally graded module which equals its positive-ideal multiple is zero. This is the exact graded Nakayama vanishing step used to remove the complementary kernel in the source's free-cover construction.
```
theorem subsingleton_of_positiveIdeal_smul_eq_top
    (𝓐 : ℤ → Submodule k A) (𝓜 : ℤ → Submodule k M)
    [DirectSum.Decomposition 𝓜] [SetLike.GradedSMul 𝓐 𝓜]
    (d₀ : ℤ) (hbound : ∀ j < d₀, 𝓜 j = ⊥)
    (hgen : positiveIdeal 𝓐 • (⊤ : Submodule A M) = ⊤) :
    Subsingleton M := by
…
```
Mentions: OAI.KLInvariance.Graded.positiveIdeal
theorem OAI.KLInvariance.EdgeImage.kernel_saturated line 381
Source documentation
The simultaneous vanishing conditions are saturated with respect to α when multiplication by α is injective on their target.
```
theorem kernel_saturated (f : B →ₗ[A] D) (α : A)
    (hα : Function.Injective (fun x : D => α • x)) (b : B) :
    α • b ∈ LinearMap.ker f ↔ b ∈ LinearMap.ker f := by
…
```
theorem OAI.KLInvariance.EdgeImage.reduced_kernel_injective line 394
Source documentation
Reducing the saturated kernel modulo α introduces no additional relations. This is the injectivity behind L/αL ≃ J.
```
theorem reduced_kernel_injective (f : B →ₗ[A] D) (α : A)
    (hα : Function.Injective (fun x : D => α • x)) :
    Function.Injective (QuotSMulTop.map α (LinearMap.ker f).subtype) := by
…
```

def OAI.KLInvariance.EdgeImage.reducedInclusion line 413

Source documentation

The inclusion after reduction, viewed over the actual factor ring.

def reducedInclusion (f : B →ₗ[A] D) (α : A) :
    QuotSMulTop α (LinearMap.ker f) →ₗ[A ⧸ Ideal.span {α}] QuotSMulTop α B :=
…

theorem OAI.KLInvariance.EdgeImage.range_reducedInclusion_free line 420
Source documentation
Freeness of the later-edge kernel proves freeness of its actual edge image over A/(α), not merely generic freeness.
```
theorem range_reducedInclusion_free (f : B →ₗ[A] D) (α : A)
    (hα : Function.Injective (fun x : D => α • x))
    [Module.Free A (LinearMap.ker f)] :
    Module.Free (A ⧸ Ideal.span {α}) (LinearMap.range (reducedInclusion f α)) := by
…
```
Mentions: OAI.KLInvariance.EdgeImage.reducedInclusion

theorem OAI.KLInvariance.Graded.positive_smul_kernel_of_minimal_split line 441

Source documentation

If a split cover is minimal modulo I, its complementary kernel equals its own I-multiple. This is the exact input to the graded Nakayama step.

theorem positive_smul_kernel_of_minimal_split
    (I : Ideal A) (f : F →ₗ[A] P) (s : P →ₗ[A] F)
    (hs : f.comp s = LinearMap.id)
    (hmin : LinearMap.ker f ≤ I • (⊤ : Submodule A F)) :
    I • (⊤ : Submodule A (LinearMap.ker f)) = ⊤ := by
…

theorem OAI.KLInvariance.Graded.bijective_of_graded_minimal_split line 468

Source documentation

Minimality makes a split free cover an isomorphism in the bounded-below graded situation. Its kernel is not assumed to vanish.

theorem bijective_of_graded_minimal_split
    {k : Type*} [CommRing k] [Algebra k A]
    (𝓐 : ℤ → Submodule k A) (f : F →ₗ[A] P) (s : P →ₗ[A] F)
    (hs : f.comp s = LinearMap.id)
    (hmin : LinearMap.ker f ≤ positiveIdeal 𝓐 • (⊤ : Submodule A F))
    [Module k (LinearMap.ker f)] [IsScalarTower k A (LinearMap.ker f)]
    (𝓚 : ℤ → Submodule k (LinearMap.ker f))
    [DirectSum.Decomposition 𝓚] [SetLike.GradedSMul 𝓐 𝓚]
    (d₀ : ℤ) (hbound : ∀ j < d₀, 𝓚 j = ⊥) : Function.Bijective f := by
…

Mentions: OAI.KLInvariance.Graded.positiveIdeal

def OAI.KLInvariance.Hilbert.piece line 500
Source documentation
The actual degree-n vector space of a submodule, expressed in the fixed ambient homogeneous piece.
```
def piece (𝓜 : ℤ → Submodule k M) (S : Submodule k M) (n : ℤ) :
    Submodule k (𝓜 n) := S.comap (𝓜 n).subtype
```
def OAI.KLInvariance.Hilbert.term line 503
def OAI.KLInvariance.Hilbert.value line 506
lemma OAI.KLInvariance.Hilbert.piece_mono line 509
lemma OAI.KLInvariance.Hilbert.term_nonneg line 513
lemma OAI.KLInvariance.Hilbert.term_mono line 517
lemma OAI.KLInvariance.Hilbert.summable_of_le line 523
theorem OAI.KLInvariance.Hilbert.pieces_eq_of_value_eq line 530
Source documentation
Equality at one positive convergent parameter, with actual inclusion, forces equality of each homogeneous piece.
```
theorem pieces_eq_of_value_eq (𝓜 : ℤ → Submodule k M)
    [∀ n, Module.Finite k (𝓜 n)] {S T : Submodule k M}
    (h : S ≤ T) {q : ℝ} (hq : 0 < q)
    (hT : Summable (term 𝓜 T q)) (hv : value 𝓜 S q = value 𝓜 T q) :
    ∀ n, piece 𝓜 S n = piece 𝓜 T n := by
…
```
Mentions: OAI.KLInvariance.Hilbert.term, OAI.KLInvariance.Hilbert.value, OAI.KLInvariance.Hilbert.piece

theorem OAI.KLInvariance.Hilbert.eq_of_value_eq line 549

Source documentation

No assumption on support codimension is involved. Equality of convergent Hilbert values detects equality with a homogeneous target globally.

theorem eq_of_value_eq (𝓜 : ℤ → Submodule k M) [DirectSum.Decomposition 𝓜]
    [∀ n, Module.Finite k (𝓜 n)] {S T : Submodule k M}
    (h : S ≤ T) (hhom : ∀ n m, m ∈ T → (DirectSum.decompose 𝓜 m n : M) ∈ T)
    {q : ℝ} (hq : 0 < q) (hT : Summable (term 𝓜 T q))
    (hv : value 𝓜 S q = value 𝓜 T q) : S = T := by
…

Mentions: OAI.KLInvariance.Hilbert.term, OAI.KLInvariance.Hilbert.value

lemma OAI.KLInvariance.Hilbert.value_mono line 565
abbrev OAI.KLInvariance.Hilbert.defectPiece line 571
Source documentation
The degree-n piece of the actual quotient T/S.
```
abbrev defectPiece (𝓜 : ℤ → Submodule k M) (S T : Submodule k M) (n : ℤ) :=
…
```
def OAI.KLInvariance.Hilbert.defectTerm line 574
lemma OAI.KLInvariance.Hilbert.defectTerm_eq_sub line 577

theorem OAI.KLInvariance.Hilbert.defect_value_eq_sub line 590

Source documentation

Additivity of convergent Hilbert values for the actual degreewise quotient.

theorem defect_value_eq_sub (𝓜 : ℤ → Submodule k M)
    [∀ n, Module.Finite k (𝓜 n)] {S T : Submodule k M} (h : S ≤ T)
    {q : ℝ} (hq : 0 < q) (hT : Summable (term 𝓜 T q)) :
    Summable (defectTerm 𝓜 S T q) ∧
      ∑' n, defectTerm 𝓜 S T q n = value 𝓜 T q-value 𝓜 S q := by
…

Mentions: OAI.KLInvariance.Hilbert.term, OAI.KLInvariance.Hilbert.defectTerm, OAI.KLInvariance.Hilbert.value

theorem OAI.KLInvariance.Hilbert.defect_value_pos line 603

Source documentation

All proper homogeneous defects have a strictly positive Hilbert series; there is no exception for support in codimension ≥2 or finite length.

theorem defect_value_pos (𝓜 : ℤ → Submodule k M) [DirectSum.Decomposition 𝓜]
    [∀ n, Module.Finite k (𝓜 n)] {S T : Submodule k M}
    (h : S ≤ T) (hne : S ≠ T)
    (hhom : ∀ n m, m ∈ T → (DirectSum.decompose 𝓜 m n : M) ∈ T)
    {q : ℝ} (hq : 0 < q) (hT : Summable (term 𝓜 T q)) :
    0 < ∑' n, defectTerm 𝓜 S T q n := by
…

Mentions: OAI.KLInvariance.Hilbert.term, OAI.KLInvariance.Hilbert.defectTerm