Faithfulness of the stable transpose

The Auslander–Bridger transpose detects maps factoring through projective modules: a map between finitely presented modules vanishes in the projective stable category if and only if its transpose does. Consequently the stable transpose functor is faithful.

The detection statement uses arbitrary finite projective presentations. It follows from recovering the original map after two transpositions. More precisely, if a transposed map factors through a projective, the original map factors through the degree-zero projective of the target presentation. No commutativity, Noetherian, or minimality assumption is needed.

References

• M. Auslander, M. Bridger, Stable module theory, Mem. Amer. Math. Soc. 94 (1969), Section 2.1.

theorem TauCeti.AuslanderReitenTranspose.exists_comp_eq_of_map_factor {A : Type u} [Ring A] {M : Type u_1} {N : Type u_2} {P₀ : Type u_3} {P₁ : Type u_4} {Q₀ : Type u_5} {Q₁ : Type u_6} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] [Module.Finite A P₀] [Module.Projective A P₀] [Module.Finite A P₁] [Module.Projective A P₁] [Module.Finite A Q₀] [Module.Projective A Q₀] [Module.Finite A Q₁] [Module.Projective A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {π : P₀ →ₗ[A] M} {ρ : Q₀ →ₗ[A] N} (hp : Function.Exact ⇑p ⇑π) (hπ : Function.Surjective ⇑π) (hq : Function.Exact ⇑q ⇑ρ) (hρ : Function.Surjective ⇑ρ) (f : M →ₗ[A] N) (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf₀ : ρ ∘ₗ f₀ = f ∘ₗ π) (hf₁ : f₀ ∘ₗ p = q ∘ₗ f₁) {C : Type u_7} [AddCommGroup C] [Module Aᵐᵒᵖ C] [Module.Projective Aᵐᵒᵖ C] (i : AuslanderReitenTranspose q →ₗ[Aᵐᵒᵖ] C) (j : C →ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p) (hfactor : map f₀ f₁ hf₁ = j ∘ₗ i) : ∃ (a : M →ₗ[A] Q₀), ρ ∘ₗ a = f

If the transpose of a presentation lift factors through a projective right module, the original module map factors through the target presentation's degree-zero projective.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.stableMap_eq_zero_iff {A : Type u} [Ring A] {M N P₀ P₁ Q₀ Q₁ : Type v} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] [Module.Finite A P₀] [Module.Projective A P₀] [Module.Finite A P₁] [Module.Projective A P₁] [Module.Finite A Q₀] [Module.Projective A Q₀] [Module.Finite A Q₁] [Module.Projective A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {π : P₀ →ₗ[A] M} {ρ : Q₀ →ₗ[A] N} [Small.{v, u} A] (hp : Function.Exact ⇑p ⇑π) (hπ : Function.Surjective ⇑π) (hq : Function.Exact ⇑q ⇑ρ) (hρ : Function.Surjective ⇑ρ) (f : (ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧M ⟶ (ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧N) : (stableMap ⋯ hq hρ) f = 0 ↔ f = 0

Stable transposition reflects zero morphisms between finite projective presentations.

theorem TauCeti.AuslanderReitenTranspose.stableMap_injective {A : Type u} [Ring A] {M N P₀ P₁ Q₀ Q₁ : Type v} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] [Module.Finite A P₀] [Module.Projective A P₀] [Module.Finite A P₁] [Module.Projective A P₁] [Module.Finite A Q₀] [Module.Projective A Q₀] [Module.Finite A Q₁] [Module.Projective A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {π : P₀ →ₗ[A] M} {ρ : Q₀ →ₗ[A] N} [Small.{v, u} A] (hp : Function.Exact ⇑p ⇑π) (hπ : Function.Surjective ⇑π) (hq : Function.Exact ⇑q ⇑ρ) (hρ : Function.Surjective ⇑ρ) : Function.Injective ⇑(stableMap ⋯ hq hρ)

Stable transposition is injective on stable Hom groups.

instance TauCeti.stableTransposeFunctor_faithful {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) : (stableTransposeFunctor P).Faithful

The transpose attached to any family of finite projective presentations is faithful.

instance TauCeti.stableTranspose_faithful {A : Type u} [Ring A] : (stableTranspose A).Faithful

The Auslander–Bridger stable transpose on finitely presented modules is faithful.