Support detects the residual after stable scalar torsion #
The support argument is most transparent before localization: the exact
sequence for the power kernel splits support into torsion and residual parts,
and support_quotSMulTop then applies at the larger prime.
@[reducible, inline]
abbrev
AlgebraicAnalysis.StableTorsionResidualSupport.scalarEnd
{R : Type u}
{E : Type v}
[CommRing R]
[AddCommGroup E]
[Module R E]
(x : R)
:
Scalar multiplication by x, viewed as a module endomorphism.
Equations
Instances For
theorem
AlgebraicAnalysis.StableTorsionResidualSupport.residual_nontrivial_of_support
{R : Type u}
{E : Type v}
[CommRing R]
[AddCommGroup E]
[Module R E]
[Module.Finite R E]
(x : R)
(n : ℕ)
(p q : PrimeSpectrum R)
(hp : p ∈ Module.support R E)
(hpq : p ≤ q)
(hxp : x ∉ p.asIdeal)
(hq : q ∈ Module.support R (QuotSMulTop x E))
: