Fullness of the stable transpose

Every map between transposes of finite projective presentations is induced by a square between the original presentations. Consequently the contravariant transpose functor on finitely presented stable modules is full. This is the fullness half of the Auslander–Bridger stable duality; faithfulness and essential surjectivity are separate results.

The lifting statement is stronger than stable fullness: it realizes an actual module map between transposes, before passing to the projective stable quotient. Neither minimality nor a Noetherian hypothesis is needed, and the coefficient ring may be noncommutative.

Use AuslanderReitenTranspose.exists_map_eq to realize a map between transposes by a presentation square, and AuslanderReitenTranspose.exists_lift_map_eq to obtain a map between the presented modules. AuslanderReitenTranspose.stableMap_surjective gives preimages on stable Hom groups for fixed presentations. The Full instances for stableTransposeFunctor and stableTranspose make CategoryTheory.Functor.preimage available for stable morphisms between their images, with CategoryTheory.Functor.map_preimage identifying their transposes with the given morphisms.

References

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

theorem TauCeti.AuslanderReitenTranspose.exists_map_eq {A : Type u} [Ring A] {P₀ : Type u_3} {P₁ : Type u_4} {Q₀ : Type u_5} {Q₁ : Type u_6} [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [AddCommGroup Q₀] [Module A Q₀] [AddCommGroup Q₁] [Module A Q₁] [Module.Projective A Q₀] [Module.Finite A Q₀] [Module.Projective A Q₁] [Module.Finite A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} (h : AuslanderReitenTranspose q →ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p) : ∃ (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁), map f₀ f₁ hf = h

Every map Tr q → Tr p, with q an arrow between finite projectives, comes from a square from p to q. The modules of p are arbitrary. This is an equality of actual module maps, not merely of stable classes.

theorem TauCeti.AuslanderReitenTranspose.exists_lift_map_eq {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.Projective A Q₀] [Module.Finite A Q₀] [Module.Projective A Q₁] [Module.Finite A Q₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {π : P₀ →ₗ[A] M} {ρ : Q₀ →ₗ[A] N} (hp : Function.Exact ⇑p ⇑π) (hπ : Function.Surjective ⇑π) (h : AuslanderReitenTranspose q →ₗ[Aᵐᵒᵖ] AuslanderReitenTranspose p) (hq : ρ ∘ₗ q = 0) : ∃ (f : M →ₗ[A] N) (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (_ : ρ ∘ₗ f₀ = f ∘ₗ π) (hf₁ : f₀ ∘ₗ p = q ∘ₗ f₁), map f₀ f₁ hf₁ = h

A map Tr q → Tr p is the transpose of a lift of some map between the presented modules, provided the modules of q are finite projective. The diagram ending in M need only be exact and surjective, and the diagram ending in N need only have zero composite.

theorem TauCeti.AuslanderReitenTranspose.stableMap_surjective {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.Projective A P₀] [Module.Projective A P₁] [Module.Finite A P₁] [Module.Projective A Q₀] [Module.Finite A Q₀] [Module.Projective A Q₁] [Module.Finite 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.Surjective ⇑(stableMap ⋯ hq hρ)

Transposition is surjective on stable Hom groups for finite projective presentations.

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

The stable transpose functor attached to any family of finite projective presentations is full.

instance TauCeti.instFullFinitelyPresentedStableModuleOppositeMulOppositeStableTranspose {A : Type u} [Ring A] : (stableTranspose A).Full

The Auslander–Bridger transpose with chosen presentations is full.