Dual right presentations

Dualizing a finite projective right presentation with values in the regular module A gives a finite projective left presentation of its cokernel. The cokernel is finitely presented over an arbitrary ring.

The A-valued dual makes the inverse Auslander–Bridger transpose an actual left A-module, without transporting a module over the double opposite. rightTransposePresentation retains the presenting projectives and maps so that the canonical recovery is available to the stable equivalence.

References

• M. Auslander, M. Bridger, Stable module theory, Section 2.1.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteProjectivePresentation.rightTranspose {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) : ModuleCat A

The transpose of a right presentation, with duals valued in A so that the result is an actual left A-module rather than a module over the double opposite.

Equations

• Q.rightTranspose = ↧((↑Q.P₁ →ₗ[Aᵐᵒᵖ] A) ⧸ (LinearMap.lcomp A A Q.p).range)

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteProjectivePresentation.rightTransposePresentation {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) : FiniteProjectivePresentation Q.rightTranspose

The finite projective presentation of a right transpose obtained by dualizing its right presentation. The abbreviation keeps the dual modules and their maps definitionally identifiable for double-transpose recovery.

Equations

• One or more equations did not get rendered due to their size.

instance TauCeti.FiniteProjectivePresentation.instFinitePresentationCarrierRightTranspose {A : Type u} [Ring A] {N : ModuleCat Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N) : Module.FinitePresentation A ↑Q.rightTranspose

A right transpose is finitely presented over an arbitrary ring.