The Auslander–Bridger stable equivalence

Transposition gives an additive equivalence between finitely presented stable left modules and the opposite category of finitely presented stable right modules over an arbitrary ring. Its inverse takes the cokernel of the A-valued dual of a right projective presentation. The inverse's maps are uniquely characterized by transposing them back, using the canonical double-transpose recovery. Both composites are naturally isomorphic to the identity.

stableTransposeEquivalence accepts independent choices of left and right presentations. Its forward functor is stableTransposeFunctor; its inverse has the explicit right-transpose objects, rather than objects chosen by abstract essential surjectivity. The morphisms remain those of the existing stable quotient, modulo maps through arbitrary projectives.

References

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

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

Transposition is an equivalence for every family of finite projective presentations.

instance TauCeti.instIsEquivalenceFinitelyPresentedStableModuleOppositeMulOppositeStableTranspose {A : Type u} [Ring A] : (stableTranspose A).IsEquivalence

The transpose using chosen finite projective presentations is an equivalence.

@[reducible, inline]

noncomputable abbrev TauCeti.FiniteProjectivePresentation.stableRightTransposeObj {A : Type u} [Ring A] {N : FinitelyPresentedStableModule Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N.obj.as) : FinitelyPresentedStableModule A

The cokernel of the dual right presentation, as a finitely presented stable left module.

Equations

• Q.stableRightTransposeObj = { obj := (TauCeti.ExactStructure.abelian (ModuleCat A)).projectiveStableFunctor.obj Q.rightTranspose, property := ⋯ }

noncomputable def TauCeti.FiniteProjectivePresentation.stableTransposeRightIso {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) {N : FinitelyPresentedStableModule Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N.obj.as) : (stableTransposeFunctor P).obj Q.stableRightTransposeObj ≅ Opposite.op N

Transposition of the dual right presentation recovers the original stable right module. The comparison also accounts for the left presentation chosen by the forward functor.

Equations

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

theorem TauCeti.FiniteProjectivePresentation.stableTransposeRightIso_def {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) {N : FinitelyPresentedStableModule Aᵐᵒᵖ} (Q : FiniteProjectivePresentation N.obj.as) : stableTransposeRightIso P Q = CategoryTheory.eqToIso ⋯ ≪≫ ((P Q.stableRightTransposeObj).stableTransposeIso Q.rightTransposePresentation ≪≫ CategoryTheory.ObjectProperty.isoMk (fun (M : (ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).ProjectiveStableCategory) => Module.FinitePresentation Aᵐᵒᵖ ↑M.as) ((ExactStructure.abelian (ModuleCat Aᵐᵒᵖ)).projectiveStableFunctor.mapIso (rightDoubleTransposePresentationEquiv A Q.p Q.π ⋯ ⋯).toModuleIso)).symm.op

The stable recovery compares the chosen left presentation with the dual right presentation, then applies the existing double-transpose recovery.

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

The inverse transpose, with the cokernels of dual right presentations as its objects. Fullness and faithfulness uniquely determine its maps from double-transpose recovery.

Equations

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

@[simp]

theorem TauCeti.stableTransposeInverse_obj {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) (N : (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ) : (stableTransposeInverse P Q).obj N = (Q (Opposite.unop N)).stableRightTransposeObj

Inverse transposition takes the cokernel of the chosen dual right presentation.

noncomputable def TauCeti.stableTransposeInverseRecoveryIso {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) (N : (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ) : (stableTransposeFunctor P).obj ((stableTransposeInverse P Q).obj N) ≅ N

Transposing an inverse-transpose object recovers the original stable right module.

Equations

• TauCeti.stableTransposeInverseRecoveryIso P Q N = ⋯.mpr (TauCeti.FiniteProjectivePresentation.stableTransposeRightIso P (Q (Opposite.unop N)))

theorem TauCeti.stableTransposeInverseRecoveryIso_def {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) (N : (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ) : stableTransposeInverseRecoveryIso P Q N = CategoryTheory.eqToIso ⋯ ≪≫ FiniteProjectivePresentation.stableTransposeRightIso P (Q (Opposite.unop N))

Inverse recovery is the dual-presentation comparison after the inverse's object equation.

@[simp]

theorem TauCeti.stableTransposeFunctor_map_inverse {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) {N L : (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ} (f : N ⟶ L) : (stableTransposeFunctor P).map ((stableTransposeInverse P Q).map f) = CategoryTheory.CategoryStruct.comp (stableTransposeInverseRecoveryIso P Q N).hom (CategoryTheory.CategoryStruct.comp f (stableTransposeInverseRecoveryIso P Q L).inv)

Transposing an inverse-transpose map gives the original map conjugated by recovery.

instance TauCeti.instAdditiveOppositeFinitelyPresentedStableModuleMulOppositeStableTransposeInverse {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) : (stableTransposeInverse P Q).Additive

Inverse transposition preserves addition of stable morphisms.

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

Double-transpose recovery is a natural isomorphism on stable right modules.

Equations

• TauCeti.stableTransposeCounitIso P Q = CategoryTheory.NatIso.ofComponents (TauCeti.stableTransposeInverseRecoveryIso P Q) ⋯

@[simp]

theorem TauCeti.stableTransposeCounitIso_app {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) (N : (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ) : (stableTransposeCounitIso P Q).app N = stableTransposeInverseRecoveryIso P Q N

The counit is the comparison induced by the dual right presentation and its recovery.

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

Double transposition is naturally the identity on stable left modules.

Equations

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

@[simp]

theorem TauCeti.stableTransposeUnitIso_app {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) (M : FinitelyPresentedStableModule A) : (stableTransposeUnitIso P Q).app M = (stableTransposeFunctor P).preimageIso (stableTransposeInverseRecoveryIso P Q ((stableTransposeFunctor P).obj M)).symm

The unit lifts inverse recovery through the fully faithful transpose functor.

noncomputable def TauCeti.stableTransposeEquivalence {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) : FinitelyPresentedStableModule A ≌ (FinitelyPresentedStableModule Aᵐᵒᵖ)ᵒᵖ

The Auslander–Bridger equivalence, with left and right transpose functors and their canonical double-transpose comparisons. It holds over any ring.

Equations

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

@[simp]

theorem TauCeti.stableTransposeEquivalence_functor {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) : (stableTransposeEquivalence P Q).functor = stableTransposeFunctor P

The forward functor of the stable equivalence is transposition.

@[simp]

theorem TauCeti.stableTransposeEquivalence_inverse {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) : (stableTransposeEquivalence P Q).inverse = stableTransposeInverse P Q

The inverse functor has the explicit dual right-presentation cokernels as objects.

@[simp]

theorem TauCeti.stableTransposeEquivalence_unitIso {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) : (stableTransposeEquivalence P Q).unitIso = stableTransposeUnitIso P Q ≪≫ CategoryTheory.eqToIso ⋯

The unit of the stable equivalence is the lifted inverse recovery.

@[simp]

theorem TauCeti.stableTransposeEquivalence_counitIso {A : Type u} [Ring A] (P : (M : FinitelyPresentedStableModule A) → FiniteProjectivePresentation M.obj.as) (Q : (N : FinitelyPresentedStableModule Aᵐᵒᵖ) → FiniteProjectivePresentation N.obj.as) : (stableTransposeEquivalence P Q).counitIso = CategoryTheory.eqToIso ⋯ ≪≫ stableTransposeCounitIso P Q

The counit of the stable equivalence is the natural double-transpose recovery.