Minimal projective presentations #
A projective presentation of a module M is an exact sequence P₁ → P₀ → M → 0 with P₀ and
P₁ projective. It is minimal when both of its maps are as small as they can be: P₀ → M is a
projective cover (TauCeti.IsProjectiveCover) and P₁ covers the syzygy ker (P₀ → M), again as
a projective cover. This file supplies the predicate TauCeti.IsMinimalProjectivePresentation and
the comparison theorem that makes it useful.
The minimality is packaged as two superfluous kernels rather than as a nested
TauCeti.IsProjectiveCover, because the second cover is a map into the submodule ker p₀ and
carrying its corestriction around in the definition would make every consumer corestrict as well.
TauCeti.IsMinimalProjectivePresentation.isProjectiveCover_codRestrict reads the definition back
in the corestricted form, and TauCeti.IsProjectiveCover.isMinimalProjectivePresentation builds a
minimal presentation from a pair of covers, so the two readings are interchangeable.
The theorem the notion exists for is that a minimal projective presentation is a quotient of every
projective presentation: given any projective presentation of the same module there are
surjections from it onto the minimal one commuting with both maps
(TauCeti.IsMinimalProjectivePresentation.exists_surjective). Applying that to a second minimal
presentation and reading the surjections back through the uniqueness of projective covers makes
them isomorphisms, so a minimal projective presentation is unique up to isomorphism of the whole
diagram (TauCeti.IsMinimalProjectivePresentation.exists_linearEquiv). That uniqueness is what
lets a construction be made from a minimal presentation: the Auslander-Reiten transpose Tr M,
the cokernel of Hom(−, A) applied to a minimal projective presentation of M, is well defined
because of it.
Existence is a separate matter, exactly as for projective covers: it is a condition on the ring,
discharged over a semiprimary ring in
TauCeti/Algebra/Module/MinimalProjectivePresentation/Existence.lean by covering M and then
covering its syzygy. Nothing here assumes it; every statement is conditional on a presentation being
given, and TauCeti.IsProjectiveCover.isMinimalProjectivePresentation is the step that turns two
covers into one presentation.
What is proved here about the size of a presentation is that a noetherian middle term forces a
finitely generated left-hand source (TauCeti.IsMinimalProjectivePresentation.finite): the syzygy
cut out of a noetherian module is finitely generated, and the left-hand source covers that. Neither
the ring nor the presented module is constrained; over a noetherian ring presenting a finitely
generated module the middle term is finitely generated, hence noetherian, which is how a consumer
gets there. This is the finiteness a construction made from a presentation needs — the
Auslander-Reiten transpose is the cokernel of Hom(−, A) applied to one, and its vanishing
criterion asks for a finitely generated P₁.
The file is layered by the coefficients each part needs, as
TauCeti/Algebra/Module/ProjectiveCover/Basic.lean is. The predicate itself and the two cover-form
readings of it need only a semiring and additive monoids. The degeneration over a projective
module needs the presented module to be an additive group, that being what uniqueness of covers
needs. The comparison and uniqueness theorems need a ring, which the syzygy forces rather than the
proofs choosing it: they apply the cover statements of
TauCeti/Algebra/Module/ProjectiveCover/Basic.lean to the syzygy ker p₀ as the covered module,
and those are stated for a covered module that is
an additive group. A submodule of an additive group is itself an additive group only once the
scalars form a ring — Submodule.addCommGroup is a [Ring R] instance, and over a semiring a
submodule need not be closed under negation, as ℕ ⊆ ℤ shows — so over a semiring
↥(LinearMap.ker p₀) carries no AddCommGroup structure at all.
Main definitions #
TauCeti.IsMinimalProjectivePresentation p₁ p₀:p₀is a projective cover ofM, the source ofp₁is projective,range p₁ = ker p₀, andker p₁is superfluous.
Main results #
TauCeti.IsMinimalProjectivePresentation.exact: the two maps do form a presentation.TauCeti.IsMinimalProjectivePresentation.isProjectiveCover_codRestrictandTauCeti.IsProjectiveCover.isMinimalProjectivePresentation: minimality read asp₁being a projective cover of the syzygy, in both directions.TauCeti.IsMinimalProjectivePresentation.exists_surjective: a minimal projective presentation is a quotient of every projective presentation, by a pair of surjections commuting with the maps.TauCeti.IsMinimalProjectivePresentation.bijective_of_comp_eqandTauCeti.IsMinimalProjectivePresentation.exists_linearEquiv: uniqueness, first as bijectivity of any pair of comparison maps between two minimal presentations and then as an isomorphism of the whole diagram. The accompanying isomorphism of syzygies needs neither left-hand map and so is stated one layer down, asTauCeti.IsProjectiveCover.nonempty_linearEquiv_kerfor the two right-hand covers.TauCeti.IsMinimalProjectivePresentation.bijective_of_projective,TauCeti.IsMinimalProjectivePresentation.eq_zero_of_projectiveandTauCeti.IsMinimalProjectivePresentation.subsingleton_of_projective: over a projective module the presentation degenerates,P₀ ≅ MandP₁ = 0.TauCeti.IsMinimalProjectivePresentation.range_le_jacobsonandTauCeti.IsMinimalProjectivePresentation.ker_le_jacobson: both kernels sit inside the radical, the standard quantitative form of minimality.TauCeti.IsMinimalProjectivePresentation.finite: a minimal projective presentation whose middle term is noetherian has a finitely generated left-hand source.
References #
This implements the projective half of sublayer 6B, "minimal projective/injective presentations",
of Layer 6 of
the quiver-representations roadmap,
the prerequisite it names for the transpose Tr and the Auslander-Reiten translate τ = D Tr
("it is well-defined only up to projectives, through minimal presentations and duality on
finite-dimensional modules"). The injective co-presentation is the remaining half, as the injective
envelope is the remaining half of TauCeti/Algebra/Module/ProjectiveCover/Basic.lean.
- M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section I.2 and Section IV.1.
- I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Cambridge University Press (2006), Section I.5 and Section IV.2.
A minimal projective presentation P₁ → P₀ → M → 0 of M: the sequence is exact at P₀
and at M, both sources are projective, and both maps are minimal — p₀ is a projective cover of
M, and p₁ has superfluous kernel, so that it is a projective cover of the syzygy ker p₀
(TauCeti.IsMinimalProjectivePresentation.isProjectiveCover_codRestrict).
Only the exactness at P₀, range p₁ = ker p₀, is recorded: exactness at M is the surjectivity
of p₀, which the projective cover already carries.
- isProjectiveCover : IsProjectiveCover p₀
The right-hand map is a projective cover of the presented module.
- projective : Module.Projective R P₁
The left-hand source is projective.
Exactness at
P₀.- isSuperfluous_ker : IsSuperfluous p₁.ker
Minimality of the left-hand map: it covers the syzygy without slack.
Instances For
The presenting map of a minimal projective presentation is onto.
A minimal projective presentation is a presentation: the sequence P₁ → P₀ → M is exact at
P₀.
Replacing the presented module by an isomorphic module preserves minimality.
The left-hand map of a presentation lands in the syzygy.
Minimality of the left-hand map, in cover form: corestricted to the syzygy ker p₀, the
map p₁ is a projective cover of it. This is the reading of the definition that
TauCeti.IsProjectiveCover.isMinimalProjectivePresentation inverts.
Two projective covers make a minimal projective presentation. Given a projective cover p₀
of M and a projective cover c of its syzygy ker p₀, following c by the inclusion of the
syzygy presents M minimally. This is the only way a minimal presentation is ever built, so
existence of minimal presentations is exactly existence of the two covers.
A projective module presents itself. In a minimal projective presentation of a projective module the presenting map is already an isomorphism, being a projective cover of a module that covers itself.
The syzygy of a projective module vanishes, so the left-hand map of a minimal projective presentation of it is zero.
Minimality forces the left-hand source of a minimal projective presentation of a projective module to vanish as well, not merely the map out of it.
A minimal projective presentation is a quotient of every projective presentation. If
Q₁ →ₗ Q₀ ↠ M is any projective presentation of M — projective sources, exact at Q₀, onto M
— then it maps onto a minimal projective presentation of M by a pair of surjections
commuting with both maps.
Both surjectivities are the minimality of the target: the first is that a projective cover receives every projective presentation by a surjection, and the second is the same statement for the induced map on syzygies, which is onto because the first one is.
Uniqueness of the minimal projective presentation, in comparison-map form. A pair of maps
between the sources of two minimal projective presentations of M that commutes with the presenting
maps and with the two left-hand maps consists of two isomorphisms; no further hypothesis on the pair
is needed.
Each is bijective because it compares two projective covers of the same module — of M on the
right, and of the syzygy on the left, the two syzygies being identified by the right-hand map.
Uniqueness of the minimal projective presentation. Two minimal projective presentations of the same module are isomorphic as diagrams: there are linear equivalences of both sources commuting with the presenting map and with the two syzygy maps.
The comparison surjections come from
TauCeti.IsMinimalProjectivePresentation.exists_surjective, and
TauCeti.IsMinimalProjectivePresentation.bijective_of_comp_eq turns them into isomorphisms.
Minimality, quantitatively, on the right: the image of the left-hand map — equivalently the
syzygy — lies in the radical of P₀. A presentation whose image escaped the radical could be
shrunk.
Minimality, quantitatively, on the left: the kernel of the left-hand map lies in the
radical of P₁.
A minimal projective presentation over a noetherian middle term is finitely generated on the
left. If P₀ is a noetherian module then the left-hand source P₁ of a minimal projective
presentation with middle term P₀ is finitely generated: noetherianity of P₀ is exactly what
makes the syzygy ker p₀ finitely generated, and P₁ covers that syzygy
(TauCeti.IsProjectiveCover.finite).
Nothing is assumed of the ring or of the presented module. A consumer over a noetherian ring
presenting a finitely generated M supplies IsNoetherian R P₀ from
have : Module.Finite R P₀ := h.isProjectiveCover.finite, the middle term being finitely generated
over any ring.