Projective summands of the Auslander–Reiten transpose

The transpose of a finite minimal projective presentation has no nonzero projective retract. This removes the projective ambiguity in the stable transpose construction: when passing back to actual modules, a minimal transpose contributes no projective summands. In particular, such a transpose is projective exactly when it is zero.

The results hold over an arbitrary ring. Only the two presenting projectives need be finitely generated; no finiteness is required of the projective retract. More generally, the statements apply to any map between finite projectives whose kernel is superfluous, without specifying an augmentation to a presented module.

References

• M. Auslander, I. Reiten, S. O. Smalø, Representation Theory of Artin Algebras, Cambridge University Press (1995), Section IV.1.

theorem TauCeti.IsSuperfluous.subsingleton_of_retract_auslanderReitenTranspose {A : Type u_1} {P₀ : Type u_2} {P₁ : Type u_3} [Ring A] [AddCommMonoid P₀] [Module A P₀] [Module.Finite A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] [Module.Finite A P₁] [Module.Projective A P₁] {p₁ : P₁ →ₗ[A] P₀} (h : IsSuperfluous p₁.ker) {Q : Type u_4} [AddCommMonoid Q] [Module Aᵐᵒᵖ Q] [Module.Projective Aᵐᵒᵖ Q] (r : AuslanderReitenTranspose p₁ →ₗ[Aᵐᵒᵖ] Q) (s : Q →ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p₁) (hrs : r ∘ₗ s = LinearMap.id) : Subsingleton Q

The transpose of a map between finite projectives with superfluous kernel has no nonzero projective retract. In particular, this applies to finite minimal presentations.

@[simp]

theorem TauCeti.IsSuperfluous.projective_auslanderReitenTranspose_iff_subsingleton {A : Type u_1} {P₀ : Type u_2} {P₁ : Type u_3} [Ring A] [AddCommMonoid P₀] [Module A P₀] [Module.Finite A P₀] [Module.Projective A P₀] [AddCommGroup P₁] [Module A P₁] [Module.Finite A P₁] [Module.Projective A P₁] {p₁ : P₁ →ₗ[A] P₀} (h : IsSuperfluous p₁.ker) : Module.Projective Aᵐᵒᵖ (AuslanderReitenTranspose p₁) ↔ Subsingleton (AuslanderReitenTranspose p₁)

The transpose of a map between finite projectives with superfluous kernel is projective exactly when it is zero.