Algebraic hyperplane restriction

For a finite module over a commutative ring, surjectivity of multiplication by an element forces the module support to avoid the corresponding principal hypersurface. The proof is the determinant trick and is independent of any filtered or differential-operator application.

@[reducible, inline]

abbrev AlgebraicAnalysis.HyperplaneRestriction.Restriction {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (x : R) : Type u_2

Degree-zero restriction to the principal hypersurface defined by x.

Equations

• AlgebraicAnalysis.HyperplaneRestriction.Restriction x = (M ⧸ Ideal.span {x} • ⊤)

theorem AlgebraicAnalysis.HyperplaneRestriction.restriction_subsingleton_iff_smul_surjective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : R} : Subsingleton (Restriction x) ↔ Function.Surjective fun (m : M) => x • m

Restriction vanishes exactly when multiplication by x is surjective.

theorem AlgebraicAnalysis.HyperplaneRestriction.restriction_subsingleton_of_smul_surjective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {x : R} (hx : Function.Surjective fun (m : M) => x • m) : Subsingleton (Restriction x)

theorem AlgebraicAnalysis.HyperplaneRestriction.exists_annihilator_sub_one_mem_span_of_smul_surjective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (hx : Function.Surjective fun (m : M) => x • m) : ∃ (r : R), r - 1 ∈ Ideal.span {x} ∧ ∀ (m : M), r • m = 0

Determinant-trick certificate for a surjective scalar action.

theorem AlgebraicAnalysis.HyperplaneRestriction.not_mem_support_of_smul_surjective_of_mem {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (hx : Function.Surjective fun (m : M) => x • m) (p : PrimeSpectrum R) (hxp : x ∈ p.asIdeal) : p ∉ Module.support R M

A support prime containing x is impossible when x acts surjectively.

theorem AlgebraicAnalysis.HyperplaneRestriction.support_disjoint_zeroLocus_of_smul_surjective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (hx : Function.Surjective fun (m : M) => x • m) : Disjoint (Module.support R M) (PrimeSpectrum.zeroLocus {x})

The support of a finite module with surjective x-action avoids V(x).

theorem AlgebraicAnalysis.HyperplaneRestriction.support_disjoint_zeroLocus_of_restriction_subsingleton {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (hx : Subsingleton (Restriction x)) : Disjoint (Module.support R M) (PrimeSpectrum.zeroLocus {x})

Restriction-vanishing form of support exclusion.

theorem AlgebraicAnalysis.HyperplaneRestriction.support_subset_compl_zeroLocus_of_smul_surjective {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Finite R M] {x : R} (hx : Function.Surjective fun (m : M) => x • m) : Module.support R M ⊆ (PrimeSpectrum.zeroLocus {x})ᶜ

Complement-inclusion form of support exclusion.