Naturality of double-transpose recovery

Transposing a square between finite-projective presenting maps twice gives a covariant map. The canonical recovery of their cokernels commutes with this map. For augmented presentations, recovery therefore identifies the twice-transposed square with the original map of presented modules.

These identities make the double-transpose recovery compatible with morphisms, as required for the Auslander–Bridger stable duality. They hold for arbitrary, possibly noncommutative rings and do not require minimal presentations. Scalars on the second transpose are identified with the original scalars through the double-opposite equivalence.

References

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

theorem TauCeti.doubleTransposeCokernelEquiv_symm_mk_naturality (A : Type u_1) [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [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₀} (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (x : P₀) : (AuslanderReitenTranspose.map (LinearMap.lcomp Aᵐᵒᵖ A f₁) (LinearMap.lcomp Aᵐᵒᵖ A f₀) ⋯) ((doubleTransposeCokernelEquiv A p).symm (Submodule.Quotient.mk x)) = (doubleTransposeCokernelEquiv A q).symm (Submodule.Quotient.mk (f₀ x))

Double transposition carries the recovered class of a presenting vector to the recovered class of its image under the original presentation square.

theorem TauCeti.doubleTransposeCokernelEquiv_naturality (A : Type u_1) [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [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₀} (f₀ : P₀ →ₗ[A] Q₀) (f₁ : P₁ →ₗ[A] Q₁) (hf : f₀ ∘ₗ p = q ∘ₗ f₁) (z : AuslanderReitenTranspose (LinearMap.lcomp Aᵐᵒᵖ A p)) : (doubleTransposeCokernelEquiv A q) ((AuslanderReitenTranspose.map (LinearMap.lcomp Aᵐᵒᵖ A f₁) (LinearMap.lcomp Aᵐᵒᵖ A f₀) ⋯) z) = (p.range.mapQ q.range f₀ ⋯) ((doubleTransposeCokernelEquiv A p) z)

The canonical double-transpose recovery commutes with the map on cokernels induced by a presentation square.

theorem TauCeti.doubleTransposePresentationEquiv_symm_naturality (A : Type u_1) [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [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₀} {M : Type u_6} {N : Type u_7} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] {π : 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₁) (y : M) : (AuslanderReitenTranspose.map (LinearMap.lcomp Aᵐᵒᵖ A f₁) (LinearMap.lcomp Aᵐᵒᵖ A f₀) ⋯) ((doubleTransposePresentationEquiv A p π hp hπ).symm y) = (doubleTransposePresentationEquiv A q ρ hq hρ).symm (f y)

Inverse double-transpose recovery commutes with a lift of a module map.

theorem TauCeti.doubleTransposePresentationEquiv_naturality (A : Type u_1) [Ring A] {P₀ : Type u_2} {P₁ : Type u_3} {Q₀ : Type u_4} {Q₁ : Type u_5} [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₀} {M : Type u_6} {N : Type u_7} [AddCommGroup M] [Module A M] [AddCommGroup N] [Module A N] {π : 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₁) (z : AuslanderReitenTranspose (LinearMap.lcomp Aᵐᵒᵖ A p)) : (doubleTransposePresentationEquiv A q ρ hq hρ) ((AuslanderReitenTranspose.map (LinearMap.lcomp Aᵐᵒᵖ A f₁) (LinearMap.lcomp Aᵐᵒᵖ A f₀) ⋯) z) = f ((doubleTransposePresentationEquiv A p π hp hπ) z)

Double-transpose recovery identifies a twice-transposed lift with its original module map. In particular, the recovered map depends only on the module map, not on its presentation lifts.