The stable transpose functor

The Auslander–Bridger transpose is an additive contravariant functor on finitely presented modules modulo maps factoring through projectives. Choosing a finite projective presentation at each module constructs this functor; changing the presentations gives a natural isomorphism. The comparison maps are the stable transposes of the identity maps of the presented modules.

The objects and morphisms here form a full subcategory of the existing projective stable quotient of ModuleCat. In particular, the quotient kills maps factoring through arbitrary projectives. No Noetherian, commutativity, or minimality hypothesis is needed.

Main definitions

• TauCeti.FinitelyPresentedStableModule: finitely presented modules in the projective stable quotient.
• TauCeti.stableTransposeFunctor: the functor attached to a family of presentations.
• TauCeti.stableTransposeFunctorIso: natural independence of that family.
• TauCeti.stableTranspose: the functor obtained by choosing finite projective presentations.

References

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

@[reducible, inline]

abbrev TauCeti.FinitelyPresentedStableModule (A : Type u) [Ring A] : Type (max u (v + 1))

Finitely presented modules, with morphisms taken modulo maps through projective modules. This is a full subcategory of the projective stable quotient of ModuleCat.

Equations

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

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteProjectivePresentation.stableTransposeObj {A : Type u} [Ring A] {M : ModuleCat A} (P : FiniteProjectivePresentation M) : FinitelyPresentedStableModule Aᵐᵒᵖ

The transpose of a finite projective presentation, as a finitely presented stable module over the opposite ring.

Equations

• P.stableTransposeObj = { obj := (TauCeti.ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).projectiveStableFunctor.obj ↧(TauCeti.AuslanderReitenTranspose P.p), property := ⋯ }

@[simp]

theorem TauCeti.FiniteProjectivePresentation.stableTransposeObj_obj {A : Type u} [Ring A] {M : ModuleCat A} (P : FiniteProjectivePresentation M) : P.stableTransposeObj.obj = (ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).projectiveStableFunctor.obj ↧(AuslanderReitenTranspose P.p)

The underlying stable object of a transposed presentation.

noncomputable def TauCeti.FiniteProjectivePresentation.stableTransposeIso {A : Type u} [Ring A] {M : ModuleCat A} (P Q : FiniteProjectivePresentation M) : P.stableTransposeObj ≅ Q.stableTransposeObj

Two presentations of the same module give canonically isomorphic stable transposes. Both directions are computed by transposing the identity of the presented module.

Equations

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

@[simp]

theorem TauCeti.FiniteProjectivePresentation.stableTransposeIso_hom {A : Type u} [Ring A] {M : ModuleCat A} (P Q : FiniteProjectivePresentation M) : (P.stableTransposeIso Q).hom.hom = (AuslanderReitenTranspose.stableMap ⋯ ⋯ ⋯) (CategoryTheory.CategoryStruct.id ((ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj M))

The comparison of two stable transposes is induced by the identity of the module.

@[simp]

theorem TauCeti.FiniteProjectivePresentation.stableTransposeIso_inv {A : Type u} [Ring A] {M : ModuleCat A} (P Q : FiniteProjectivePresentation M) : (P.stableTransposeIso Q).inv.hom = (AuslanderReitenTranspose.stableMap ⋯ ⋯ ⋯) (CategoryTheory.CategoryStruct.id ((ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj M))

The inverse comparison is induced by the same identity with the presentations exchanged.

@[simp]

theorem TauCeti.FiniteProjectivePresentation.stableTransposeIso_refl {A : Type u} [Ring A] {M : ModuleCat A} (P : FiniteProjectivePresentation M) : P.stableTransposeIso P = CategoryTheory.Iso.refl P.stableTransposeObj

Comparing a presentation with itself gives the identity isomorphism.

@[simp]

theorem TauCeti.FiniteProjectivePresentation.stableTransposeIso_trans {A : Type u} [Ring A] {M : ModuleCat A} (P Q R : FiniteProjectivePresentation M) : P.stableTransposeIso Q ≪≫ Q.stableTransposeIso R = P.stableTransposeIso R

Presentation comparisons compose coherently.

noncomputable def TauCeti.stableTransposeFunctor {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) : CategoryTheory.Functor (FinitelyPresentedStableModule A) (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ

The additive contravariant transpose functor determined by finite projective presentations. Contravariance is expressed by taking values in the opposite stable category.

Equations

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

@[simp]

theorem TauCeti.stableTransposeFunctor_obj {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (M : FinitelyPresentedStableModule A) : (stableTransposeFunctor P).obj M = Opposite.op (P M).stableTransposeObj

The object assigned by the transpose functor is the transpose of its chosen presentation.

@[simp]

theorem TauCeti.stableTransposeFunctor_map {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) {M N : FinitelyPresentedStableModule A} (f : M ⟶ N) : (stableTransposeFunctor P).map f = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.ObjectProperty.homMk ((AuslanderReitenTranspose.stableMap ⋯ ⋯ ⋯) f.hom)).op (CategoryTheory.eqToHom ⋯))

The map assigned by the transpose functor is the stable transpose of the underlying map, after identifying its objects with the transposed presentations.

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

The stable transpose functor preserves sums of morphisms.

noncomputable def TauCeti.stableTransposeFunctorIso {A : Type u} [Ring A] (P Q : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) : stableTransposeFunctor P ≅ stableTransposeFunctor Q

Changing finite projective presentations gives a natural isomorphism of transpose functors.

Equations

• TauCeti.stableTransposeFunctorIso P Q = CategoryTheory.NatIso.ofComponents (fun (M : TauCeti.FinitelyPresentedStableModule A) => ((Q M).stableTransposeIso (P M)).op) ⋯

@[simp]

theorem TauCeti.stableTransposeFunctorIso_app {A : Type u} [Ring A] (P Q : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (M : FinitelyPresentedStableModule A) : (stableTransposeFunctorIso P Q).app M = CategoryTheory.eqToIso ⋯ ≪≫ ((Q M).stableTransposeIso (P M)).op ≪≫ (CategoryTheory.eqToIso ⋯).symm

The component of the natural comparison is the identity-induced presentation comparison.

noncomputable def TauCeti.stableTranspose (A : Type u) [Ring A] : CategoryTheory.Functor (FinitelyPresentedStableModule A) (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ

The Auslander–Bridger transpose on finitely presented stable modules, using chosen finite projective presentations. The result is independent of the choices by TauCeti.stableTransposeFunctorIso.

Equations

• TauCeti.stableTranspose A = TauCeti.stableTransposeFunctor fun (M : TauCeti.FinitelyPresentedStableModule A) => TauCeti.FiniteProjectivePresentation.ofFinitePresentation

theorem TauCeti.stableTranspose_def (A : Type u) [Ring A] : stableTranspose A = stableTransposeFunctor fun (M : FinitelyPresentedStableModule A) => FiniteProjectivePresentation.ofFinitePresentation

The transpose is the functor constructed from the chosen finite projective presentations.

instance TauCeti.instAdditiveFinitelyPresentedStableModuleOppositeMulOppositeStableTranspose (A : Type u) [Ring A] : (stableTranspose A).Additive

The transpose using chosen presentations is additive.