Alphabeta MathHow statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Localisation of modules is exact
Statement
If is a short exact sequence of -modules, then is a short exact sequence of -modules.
Facts & Assumptions
Given: A commutative ring , a multiplicative subset , and a short exact sequence .
Localisation is naturally (Localisation of modules is extension of scalars).
Tensoring a right-exact sequence with a fixed module preserves right exactness (Tensoring is right exact).
Injective module homomorphisms remain injective after localisation (Injective module maps remain injective after localisation).
A short exact sequence is exact, with left map injective and right map surjective (Exact sequences and short exact sequences of modules).
Proof
By [L4], the tail is exact. Using [L1] to identify localisation with tensor product, [L2] gives an exact sequence .
The map is injective by [L4], so [L3] makes injective.
Steps 1.1 and 1.2 show that the localised sequence is short exact.
Depends on
Used by
- Koszul Homology Localises Corollary
- Localisation commutes with kernels images and cokernels Corollary
- localisations of regular local rings are regular Corollary
- Coherent module sheaves Definition
- Delta invariant of a curve singularity Definition
- Finite type and finitely presented module sheaves Definition
- Fitting ideal sheaves Definition
- Strict transform of a closed subscheme Definition
- Fitting ideals of a diagonal two-by-two presentation Example
- Localization of modules gives an exact functor between module categories Example
- A finite presentation reduces localised Hom to the finite free case Lemma
- A killed first Tor obstruction yields flatness after local Noetherian base change Lemma
- Affine-local flatness Lemma
- Affineness from a finite principal cover Lemma
- Blowing up a non-regular point strictly increases the finite normalization subalgebra Lemma
- Closed immersions are affine quotients and survive base change Lemma
- Descent of modules on a finite principal cover Lemma
- Exact principal-open Cech resolution Lemma
- Fibrewise exactness of a finite free complex is open in a flat Cohen-Macaulay family Lemma
- Finite birational algebras descend across a flat completion neighbourhood Lemma
- Finite presentation data descend to Noetherian algebra and module stages Lemma
- Finite relative integral-closure charts for classical quasi-finite morphisms Lemma
- Finite torsion-free modules over Dedekind domains are projective Lemma
- Finite twisted locally free resolutions on projective space Lemma
- Finite-stage descent of finitely presented quasi-coherent sheaves Lemma
- Finite-type field extensions with zero Ω Lemma
- Fitting ideals do not depend on a presentation Lemma
- Fpqc covers are universally submersive Lemma
- Generic freeness over a Noetherian domain Lemma
- Geometric Nakayama for finite-type sheaves Lemma
- Higher direct images localize over an affine base Lemma
- Hypersurface cohomology sequence Lemma
- Integral quasi-coherent algebras over qcqs bases are unions of finite subalgebras Lemma
- Invertible Jacobian minor gives regular parameters in a polynomial fibre Lemma
- koszul euler characteristic first element reduction Lemma
- koszul homology finite length for an ideal of definition Lemma
- Line bundles on a principal localization of a regular local ring are trivial Lemma
- Noetherian devissage for coherent proper pushforward Lemma
- Rationalization is exact and commutes with singular homology Lemma
- Regular hyperplane step for coherent support induction Lemma
…and 22 more results.
Dependency tree · two levels
16 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- A. Altman and S. Kleiman, A Term of Commutative Algebra, 13th ed., Theorem 12.20 (standard reference, not scraped)
- J. S. Milne, A Primer of Commutative Algebra, v4.03, Proposition 5.11 (standard reference, not scraped)