Opposite duals of finite projective modules

For a left module M over a possibly noncommutative semiring R, the dual Hom_R(M, R) is a left Rᵐᵒᵖ-module, with scalars acting on the values on the right. This file proves that this dual is finite projective when M is finite projective. In particular, the duals of the projectives in a finite projective presentation are again finite projectives, as required when forming the Auslander–Bridger transpose.

Main results

• TauCeti.oppositeDual_free: the opposite dual of a finite free module is free.
• TauCeti.oppositeDual_projective: the opposite dual of a finite projective module is projective.
• TauCeti.oppositeDual_finite: the opposite dual of a finite projective module is finite.

References

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

instance TauCeti.oppositeDual_free {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Free R M] : Module.Free Rᵐᵒᵖ (Module.Dual R M)

The dual of a finite free left module is free over the opposite semiring.

instance TauCeti.oppositeDual_projective {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.Projective Rᵐᵒᵖ (Module.Dual R M)

The dual of a finite projective left module is projective over the opposite semiring.

instance TauCeti.oppositeDual_finite {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Finite R M] [Module.Projective R M] : Module.Finite Rᵐᵒᵖ (Module.Dual R M)

The dual of a finite projective left module is finitely generated over the opposite semiring.