Documentation

TauCeti.Algebra.Category.FGModuleCat.Dual

Duality for finitely generated projective modules #

Over a commutative ring R the algebraic dual of a module M is Module.Dual R M, the hom module into R. When M is finitely generated and projective, so is its dual, and the evaluation pairing Module.evalEquiv identifies M with its double dual. Over a field this is the familiar reflexivity of finite-dimensional vector spaces.

Because FGModuleCat R keeps finite generation as part of its objects, a finitely generated projective module is an object of FGModuleCat R and its dual is one as well. This file packages the algebraic dual as a contravariant operation on the objects and morphisms of FGModuleCat R, so that constructions which dualize, such as the duality for matrix factorizations, are written once at the module level.

The crossed-transpose calculations that dualizing a curved pair of maps needs are curvature equations, and they are proved in TauCeti.Algebra.Homology.Curved.Dual beside the duals whose differential equations they are.

Main definitions #

FGModuleCat.dual: the dual of a finitely generated projective module, as an object of FGModuleCat R.
FGModuleCat.dualMap: the transpose of a morphism, contravariantly.
FGModuleCat.dualEvalIso: the isomorphism from the double dual back to the module.

The bodies of FGModuleCat.dualMap and FGModuleCat.dualEvalIso are not exposed; the results below describe them.

Main results #

FGModuleCat.dualMap_hom: the underlying module map of a transpose is the dual map of the underlying module map.
FGModuleCat.dualMap_id, FGModuleCat.dualMap_comp, FGModuleCat.dualMap_smul, FGModuleCat.dualMap_neg, FGModuleCat.dualMap_zero, FGModuleCat.dualMap_add, FGModuleCat.dualMap_sub: transposing is contravariant and compatible with the additive and R-linear structure on morphisms.
FGModuleCat.dualEvalIso_hom, FGModuleCat.dualEvalIso_inv: the underlying module maps of the double dual isomorphism and its inverse are the two halves of the evaluation pairing.
FGModuleCat.dualEvalIso_hom_naturality: the double dual isomorphism is natural, i.e. it intertwines the double transpose of a morphism with the morphism itself.

@[reducible, inline]

abbrev FGModuleCat.dual (R : Type u) [CommRing R] (M : FGModuleCat R) [Module.Projective R ↑M] :

The dual of a finitely generated projective module, as an object of FGModuleCat R.

Equations

FGModuleCat.dual R M = ↧(Module.Dual R ↑M)

Instances For

instance FGModuleCat.instProjectiveCarrierDual (R : Type u) [CommRing R] (M : FGModuleCat R) [Module.Projective R ↑M] :

Module.Projective R ↑(dual R M)

The underlying module of a dual is projective.

@[simp]

theorem FGModuleCat.dual_obj (R : Type u) [CommRing R] (M : FGModuleCat R) [Module.Projective R ↑M] :

↑(dual R M).obj = Module.Dual R ↑M

The underlying module of a dual is the module dual Module.Dual R M.

def FGModuleCat.dualMap {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f : M ⟶ N) :

dual R N ⟶ dual R M

The transpose of a morphism of finitely generated projective modules.

Equations

FGModuleCat.dualMap f = FGModuleCat.ofHom (ModuleCat.Hom.hom f.hom).dualMap

Instances For

@[simp]

theorem FGModuleCat.dualMap_hom {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f : M ⟶ N) :

ModuleCat.Hom.hom (dualMap f).hom = (ModuleCat.Hom.hom f.hom).dualMap

The underlying module map of a transpose is the dual map of the underlying module map.

@[simp]

theorem FGModuleCat.dualMap_id {R : Type u} [CommRing R] {M : FGModuleCat R} [Module.Projective R ↑M] :

dualMap (CategoryTheory.CategoryStruct.id M) = CategoryTheory.CategoryStruct.id (dual R M)

The transpose of the identity is the identity.

@[simp]

theorem FGModuleCat.dualMap_comp {R : Type u} [CommRing R] {M N P : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] [Module.Projective R ↑P] (f : M ⟶ N) (g : N ⟶ P) :

dualMap (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (dualMap g) (dualMap f)

The transpose of a composite is the composite of the transposes in the opposite order.

@[simp]

theorem FGModuleCat.dualMap_smul {R : Type u} [CommRing R] (a : R) {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f : M ⟶ N) :

dualMap (a • f) = a • dualMap f

The transpose of a scalar multiple of a morphism is the same scalar multiple of the transpose.

@[simp]

theorem FGModuleCat.dualMap_neg {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f : M ⟶ N) :

dualMap (-f) = -dualMap f

The transpose of a negated morphism is the negation of the transpose.

@[simp]

theorem FGModuleCat.dualMap_zero {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] :

The transpose of the zero morphism is the zero morphism.

@[simp]

theorem FGModuleCat.dualMap_add {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f g : M ⟶ N) :

dualMap (f + g) = dualMap f + dualMap g

The transpose of a sum of morphisms is the sum of the transposes.

@[simp]

theorem FGModuleCat.dualMap_sub {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f g : M ⟶ N) :

dualMap (f - g) = dualMap f - dualMap g

The transpose of a difference of morphisms is the difference of the transposes.

noncomputable def FGModuleCat.dualEvalIso {R : Type u} [CommRing R] (M : FGModuleCat R) [Module.Projective R ↑M] :

dual R (dual R M) ≅ M

A double dual is canonically isomorphic to the original module, by the evaluation pairing.

Equations

M.dualEvalIso = (ModuleCat.isFG R).isoMk (Module.evalEquiv R ↑M).symm.toModuleIso

Instances For

@[simp]

theorem FGModuleCat.dualEvalIso_hom {R : Type u} [CommRing R] (M : FGModuleCat R) [Module.Projective R ↑M] :

ModuleCat.Hom.hom M.dualEvalIso.hom.hom = ↑(Module.evalEquiv R ↑M).symm

The underlying module map of the double dual isomorphism is the inverse of the evaluation pairing.

@[simp]

theorem FGModuleCat.dualEvalIso_inv {R : Type u} [CommRing R] (M : FGModuleCat R) [Module.Projective R ↑M] :

ModuleCat.Hom.hom M.dualEvalIso.inv.hom = ↑(Module.evalEquiv R ↑M)

The underlying module map of the inverse of the double dual isomorphism is the evaluation pairing itself.

@[simp]

theorem FGModuleCat.dualEvalIso_hom_naturality {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f : M ⟶ N) :

CategoryTheory.CategoryStruct.comp (dualMap (dualMap f)) N.dualEvalIso.hom = CategoryTheory.CategoryStruct.comp M.dualEvalIso.hom f

The double dual isomorphism is natural: it intertwines the double transpose of a morphism with the morphism itself.

@[simp]

theorem FGModuleCat.dualEvalIso_hom_naturality_assoc {R : Type u} [CommRing R] {M N : FGModuleCat R} [Module.Projective R ↑M] [Module.Projective R ↑N] (f : M ⟶ N) {Z : FGModuleCat R} (h : N ⟶ Z) :

CategoryTheory.CategoryStruct.comp (dualMap (dualMap f)) (CategoryTheory.CategoryStruct.comp N.dualEvalIso.hom h) = CategoryTheory.CategoryStruct.comp M.dualEvalIso.hom (CategoryTheory.CategoryStruct.comp f h)

The double dual isomorphism is natural: it intertwines the double transpose of a morphism with the morphism itself.