Finite presentation of the Auslander–Bridger transpose #
The transpose of an arrow P₁ → P₀ between finite projective left A-modules is a finitely
presented left Aᵐᵒᵖ-module. Thus transposing a finite projective presentation stays within
finitely presented modules even when the ring is not Noetherian. Finite generation of the
transpose needs only finite projectivity of P₁.
These instances complement the presentation comparison in
TauCeti.Algebra.Module.AuslanderReiten.StableTranspose: the dual summands in that comparison
are finite projective, and the transposes themselves are finitely presented.
References #
- M. Auslander, M. Bridger, Stable module theory, Mem. Amer. Math. Soc. 94 (1969), Section 2.1.
instance
TauCeti.AuslanderReitenTranspose.finite
{A : Type u_1}
{P₀ : Type u_2}
{P₁ : Type u_3}
[Ring A]
[AddCommMonoid P₀]
[Module A P₀]
[AddCommMonoid P₁]
[Module A P₁]
[Module.Finite A P₁]
[Module.Projective A P₁]
(f : P₁ →ₗ[A] P₀)
:
The transpose is finitely generated when the source of its presenting arrow is finite projective.
instance
TauCeti.AuslanderReitenTranspose.finitePresentation
{A : Type u_1}
{P₀ : Type u_2}
{P₁ : Type u_3}
[Ring A]
[AddCommMonoid P₀]
[Module A P₀]
[AddCommMonoid P₁]
[Module A P₁]
[Module.Finite A P₁]
[Module.Projective A P₁]
[Module.Finite A P₀]
[Module.Projective A P₀]
(f : P₁ →ₗ[A] P₀)
:
The transpose of an arrow between finite projective modules is finitely presented over the opposite ring.