Double dualization of a projective presentation #
For a map f : P₁ → P₀ between finitely generated projective left modules over a ring A,
dualization gives a right-linear map f* : Hom_A(P₀, A) → Hom_A(P₁, A). Dualizing again,
with values in the right regular module A, gives f**. Evaluation identifies its cokernel
with the cokernel of f. Thus, for a projective presentation P₁ → P₀ → M → 0, the
cokernel after two dualizations is canonically M.
This is the involutivity calculation behind the Auslander--Bridger transpose: using the
dual presentation to transpose Tr M returns M. Comparison with another projective
presentation then gives involutivity up to projective summands. Here we expose the canonical
calculation on the presenting maps; no minimality or finite-length hypothesis is needed.
The double-dual equivalences use codomain A with its right action and are left A-linear.
The double-transpose equivalences use the transpose's actual codomain Aᵐᵒᵖ and are
semilinear along the canonical ring equivalence Aᵐᵒᵖᵐᵒᵖ ≃+* A. Thus they apply to
noncommutative rings without changing the transpose's module instances.
For a right presentation, rightDoubleTransposePresentationEquiv instead dualizes into
A itself. Its recovery is Aᵐᵒᵖ-linear, which lets left presentations realize prescribed
right modules as their transposes.
References #
- M. Auslander, M. Bridger, Stable module theory, Mem. Amer. Math. Soc. 94 (1969), Section 2.1.
The cokernel of the twice-dualized presenting map is canonically the original cokernel.
Equations
- TauCeti.doubleDualCokernelEquiv A f = (Submodule.Quotient.equiv f.range (LinearMap.lcomp A A (LinearMap.lcomp Aᵐᵒᵖ A f)).range (TauCeti.opDualEvalEquiv A P₀) ⋯).symm
Instances For
On a representative, double-dual cokernel transport applies inverse evaluation.
The inverse cokernel transport applies evaluation to a representative.
Double dualization returns the presented module. For an exact projective presentation
P₁ → P₀ → M → 0 with finitely generated projectives, the cokernel of the twice-dualized
first map is canonically isomorphic to M.
Equations
- TauCeti.doubleDualPresentationEquiv A f g hexact hsurj = (TauCeti.doubleDualCokernelEquiv A f).trans (hexact.linearEquivOfSurjective hsurj)
Instances For
Double dualization recovers the image of a vector under the presentation's quotient map.
Inverse double-dual presentation transport sends the image of a presenting vector to its evaluation functional.
Transposing the dual of a finite-projective presenting map recovers its cokernel, with the double opposite identified with the original ring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second transpose sends a functional representative to the vector it represents under inverse evaluation, after removing the opposite from its values.
Inverse second-transpose transport sends a vector to its opposite-valued evaluation functional.
Transposing the dual presentation returns the presented module. No minimality or finite-length assumption is required; the two presenting modules must be finite projective.
Equations
- TauCeti.doubleTransposePresentationEquiv A f g hexact hsurj = (TauCeti.doubleTransposeCokernelEquiv A f).trans (hexact.linearEquivOfSurjective hsurj)
Instances For
On representatives the recovered presentation applies the original quotient map to the vector represented by the opposite-valued functional.
Inverse presentation transport sends the image of a presenting vector to its opposite-valued evaluation functional.
Transposing the A-valued dual of a finite projective right presentation returns its
presented module, with no scalar transport through the double opposite.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Recovery from the right double transpose applies the augmentation to inverse evaluation.
Inverse recovery sends the image of a right presenting vector to its evaluation class.