Documentation

LeanPool.Stafford38.AlgebraicAnalysis.Module.PrincipalKoszulPositivity

Positivity for a principal Koszul quotient #

Stable power torsion contributes equally to kernel and cokernel length. After removing it, local Nakayama gives a positive residual cokernel when a support prime avoids the scalar. The proof retains embedded torsion; it does not infer injectivity from minimal-prime avoidance.

source
@[reducible, inline]
abbrev AlgebraicAnalysis.PrincipalKoszulPositivity.scalarEnd {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] (x : R) :
E →ₗ[R] E

Scalar multiplication, viewed as a linear endomorphism.

Equations
Instances For
    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.exists_stable_kernel_power {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] [IsNoetherian R E] (f : Module.End R E) :
    ∃ (n : ℕ), LinearMap.ker (f ^ n) = LinearMap.ker (f ^ (n + 1))

    The x-power torsion in a Noetherian module is already the kernel of one finite power of x. This is the stabilization step needed before passing to the quotient on which x acts injectively; it does not discard embedded torsion.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.exists_stable_kernel_power_smul {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] [IsNoetherian R E] (x : R) :
    ∃ (n : ℕ), (scalarEnd x ^ n).ker = (scalarEnd x ^ (n + 1)).ker

    Specialization of kernel stabilization to multiplication by a scalar.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.isArtinian_kernel_power {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] (f : Module.End R E) [IsArtinian R ↥(LinearMap.ker f)] (n : ℕ) :
    IsArtinian R ↥(LinearMap.ker (f ^ n))

    Finite-length coordinate kernel controls all finite power-torsion layers. The Artinian assertion is the nontrivial half; Noetherianity is inherited from the ambient finite module in the applications.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.quotient_by_stable_kernel_power_injective {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] (f : Module.End R E) (n : ℕ) (hstable : LinearMap.ker (f ^ n) = LinearMap.ker (f ^ (n + 1))) :
    Function.Injective ⇑((LinearMap.ker (f ^ n)).mapQ (LinearMap.ker (f ^ n)) f ⋯)

    Once two consecutive power kernels agree, the induced endomorphism on the quotient by the stabilized kernel is injective.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.length_cokernel_eq_kernel_add_regular_quotient {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] (f : Module.End R E) (T : Submodule R E) [IsNoetherian R ↥T] [IsArtinian R ↥T] (hT : Submodule.comap f T = T) :
    Module.length R (E ⧸ LinearMap.range f) = Module.length R ↥(LinearMap.ker f) + Module.length R (E ⧸ T ⊔ LinearMap.range f)

    Removing a finite-length invariant submodule on which all failure of injectivity is concentrated preserves the principal Koszul Euler length. The hypothesis T.comap f = T says precisely that the quotient action is injective; it does not assert injectivity on the original module.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.scalar_range_ne_top_of_mem_maximalIdeal {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] [IsLocalRing R] [Module.Finite R E] [Nontrivial E] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) :
    (scalarEnd x).range ≠ ⊤

    A maximal-ideal scalar has a proper image on a nonzero finite module.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.length_cokernel_smul_gt_length_kernel_smul {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] [IsLocalRing R] [Module.Finite R E] [Nontrivial E] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) (hinj : Function.Injective ⇑(scalarEnd x)) (_hfinite : IsFiniteLength R (E ⧸ (scalarEnd x).range)) :
    Module.length R (E ⧸ (scalarEnd x).range) > Module.length R ↥(scalarEnd x).ker

    If multiplication by x is injective on a nonzero finite local module and its cokernel has finite length, then the cokernel has strictly larger length than the kernel. The quotient is nonzero by Nakayama, so the conclusion is genuine positivity rather than an axiom-shaped length assumption.

    This is only the regular (torsion-free) specialization of the stabilized x-power-torsion cancellation argument. Minimal-support avoidance alone does not imply its injectivity hypothesis when embedded torsion is present.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.length_cokernel_smul_gt_kernel_of_finite_torsion {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] [IsLocalRing R] [Module.Finite R E] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) (T : Submodule R E) [IsNoetherian R ↥T] [IsArtinian R ↥T] (hT : Submodule.comap (scalarEnd x) T = T) (hproper : T ≠ ⊤) :
    Module.length R (E ⧸ (scalarEnd x).range) > Module.length R ↥(scalarEnd x).ker

    Embedded scalar-power torsion may be retained: after its finite-length Euler contribution is cancelled, any nonzero regular quotient contributes strictly positively by Nakayama.

    source
    theorem AlgebraicAnalysis.PrincipalKoszulPositivity.length_cokernel_smul_gt_kernel_of_support_prime {R : Type u} {E : Type v} [CommRing R] [AddCommGroup E] [Module R E] [IsLocalRing R] [Module.Finite R E] [IsNoetherian R E] {x : R} (hx : x ∈ IsLocalRing.maximalIdeal R) [IsArtinian R ↥(scalarEnd x).ker] (P : Ideal R) (hP : P.IsPrime) (hann : Module.annihilator R E ≤ P) (hxP : x ∉ P) :
    Module.length R (E ⧸ (scalarEnd x).range) > Module.length R ↥(scalarEnd x).ker

    Principal Koszul positivity, including embedded torsion. A support prime not containing x guarantees a nonzero regular quotient; finite length of the coordinate kernel makes the discarded power torsion finite length.