The transpose on stable morphisms

A map of modules lifts to a square between projective presentations. Transposing that square reverses the map. Passing to the projective stable category makes this independent of the lift: the difference of two lifts factors through the dual of the first presenting projective. When that projective is finitely generated, its opposite dual is projective too.

This file constructs the resulting additive map on stable Hom groups. It preserves identities and reverses composition, providing the morphism part of the stable transpose duality. Presentations are explicit parameters; the construction does not choose presentations for all modules or assert the stable equivalence itself.

The stable categories used here are the existing projective stable quotients for the canonical exact structures on ModuleCat. The source diagram needs only a zero composite; exactness and surjectivity are required of the target presentation. No minimality, finite length, commutativity, or field hypothesis is needed.

Main results

• TauCeti.AuslanderReitenTranspose.stableMap: the additive map on stable Hom groups.
• TauCeti.AuslanderReitenTranspose.stableMap_quotient_map: computation using any lift.
• TauCeti.AuslanderReitenTranspose.stableMap_id: identities are preserved.
• TauCeti.AuslanderReitenTranspose.stableMap_comp: composition is reversed.

References

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

noncomputable def TauCeti.AuslanderReitenTranspose.stableMap {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₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {π : P₀ →ₗ[A] M} {ρ : Q₀ →ₗ[A] N} [Small.{v, u} A] (hp : π ∘ₗ p = 0) (hq : Function.Exact ⇑q ⇑ρ) (hρ : Function.Surjective ⇑ρ) : ((ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧M ⟶ (ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧N) →+ ((ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).projectiveStableFunctor.obj ↧(AuslanderReitenTranspose q) ⟶ (ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).projectiveStableFunctor.obj ↧(AuslanderReitenTranspose p))

The transpose on stable morphisms, as an additive map from stable maps M → N to stable maps Tr q → Tr p. The presentations need not be minimal.

Equations

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

theorem TauCeti.AuslanderReitenTranspose.stableMap_quotient_map {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₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {π : P₀ →ₗ[A] M} {ρ : Q₀ →ₗ[A] N} [Small.{v, u} A] (hp : π ∘ₗ p = 0) (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₁) : (stableMap hp hq hρ) ((ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.map (ModuleCat.ofHom f)) = (ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).projectiveStableFunctor.map (ModuleCat.ofHom (map f₀ f₁ hf₁))

Any square lifting a module map computes its stable transpose, independently of the chosen lift and of the representative of the stable module map.

@[simp]

theorem TauCeti.AuslanderReitenTranspose.stableMap_id {A : Type u} [Ring A] {M P₀ P₁ : Type v} [AddCommGroup M] [Module A M] [AddCommGroup P₀] [Module A P₀] [AddCommGroup P₁] [Module A P₁] [Module.Projective A P₀] [Module.Projective A P₁] [Module.Finite A P₁] {p : P₁ →ₗ[A] P₀} {π : P₀ →ₗ[A] M} [Small.{v, u} A] (hex : Function.Exact ⇑p ⇑π) (hπ : Function.Surjective ⇑π) : (stableMap ⋯ hex hπ) (CategoryTheory.CategoryStruct.id ((ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧M)) = CategoryTheory.CategoryStruct.id ((ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).projectiveStableFunctor.obj ↧(AuslanderReitenTranspose p))

Transposition preserves the identity stable morphism.

theorem TauCeti.AuslanderReitenTranspose.stableMap_comp {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₁] {p : P₁ →ₗ[A] P₀} {q : Q₁ →ₗ[A] Q₀} {π : P₀ →ₗ[A] M} {ρ : Q₀ →ₗ[A] N} [Small.{v, u} A] [Module.Projective A Q₀] [Module.Projective A Q₁] [Module.Finite A Q₁] {L R₀ R₁ : Type v} [AddCommGroup L] [Module A L] [AddCommGroup R₀] [Module A R₀] [AddCommGroup R₁] [Module A R₁] {r : R₁ →ₗ[A] R₀} {σ : R₀ →ₗ[A] L} (hp : π ∘ₗ p = 0) (hq : Function.Exact ⇑q ⇑ρ) (hρ : Function.Surjective ⇑ρ) (hr : Function.Exact ⇑r ⇑σ) (hσ : Function.Surjective ⇑σ) (f : (ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧M ⟶ (ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧N) (g : (ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧N ⟶ (ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj ↧L) : (stableMap hp hr hσ) (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp ((stableMap ⋯ hr hσ) g) ((stableMap hp hq hρ) f)

Transposition reverses composition of stable morphisms.