Tensor products and duals of finite projective modules

The full subcategory of ModuleCat R on finite projective modules inherits its symmetric monoidal structure: the tensor product and the unit module remain finite projective. Linear dualization is a contravariant endofunctor of this subcategory, and the evaluation map identifies each module with its double dual. These constructions provide the affine tensor and dual operations to be compared with finite locally free sheaves on a scheme.

The object property finiteProjectiveModules is defined in the Cartan-map development. This file uses that same property, so the affine vector-bundle category and the category used for algebraic K₀ have the same objects and morphisms.

instance TauCeti.finiteProjectiveModules_isMonoidal (R : Type u) [CommRing R] : (finiteProjectiveModules R).IsMonoidal

Finite projective modules contain the tensor unit and are closed under tensor products.

@[instance_reducible]

instance TauCeti.finiteProjectiveModulesSymmetricCategory (R : Type u) [CommRing R] : CategoryTheory.SymmetricCategory (finiteProjectiveModules R).FullSubcategory

The symmetric monoidal structure on finite projective modules is inherited from ModuleCat R.

Equations

• TauCeti.finiteProjectiveModulesSymmetricCategory R = (TauCeti.finiteProjectiveModules R).fullSymmetricSubcategory

def TauCeti.FiniteProjectiveModules.dual (R : Type u) [CommRing R] (M : (finiteProjectiveModules R).FullSubcategory) : (finiteProjectiveModules R).FullSubcategory

The linear dual of a finite projective module is finite projective.

Equations

• TauCeti.FiniteProjectiveModules.dual R M = { obj := ↧(Module.Dual R ↑M.obj), property := ⋯ }

@[simp]

theorem TauCeti.FiniteProjectiveModules.dual_obj (R : Type u) [CommRing R] (M : (finiteProjectiveModules R).FullSubcategory) : (dual R M).obj = ↧(Module.Dual R ↑M.obj)

def TauCeti.FiniteProjectiveModules.dualMap (R : Type u) [CommRing R] {M N : (finiteProjectiveModules R).FullSubcategory} (f : M ⟶ N) : dual R N ⟶ dual R M

A map of finite projective modules induces the transpose map between their duals.

Equations

• TauCeti.FiniteProjectiveModules.dualMap R f = CategoryTheory.ObjectProperty.homMk (ModuleCat.ofHom (ModuleCat.Hom.hom f.hom).dualMap)

@[simp]

theorem TauCeti.FiniteProjectiveModules.dualMap_hom (R : Type u) [CommRing R] {M N : (finiteProjectiveModules R).FullSubcategory} (f : M ⟶ N) : (dualMap R f).hom = ModuleCat.ofHom (ModuleCat.Hom.hom f.hom).dualMap

def TauCeti.FiniteProjectiveModules.dualFunctor (R : Type u) [CommRing R] : CategoryTheory.Functor (finiteProjectiveModules R).FullSubcategoryᵒᵖ (finiteProjectiveModules R).FullSubcategory

Linear dualization reverses arrows in the category of finite projective modules.

Equations

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

@[simp]

theorem TauCeti.FiniteProjectiveModules.dualFunctor_obj (R : Type u) [CommRing R] (M : (finiteProjectiveModules R).FullSubcategoryᵒᵖ) : (dualFunctor R).obj M = dual R (Opposite.unop M)

@[simp]

theorem TauCeti.FiniteProjectiveModules.dualFunctor_map (R : Type u) [CommRing R] {M N : (finiteProjectiveModules R).FullSubcategoryᵒᵖ} (f : M ⟶ N) : (dualFunctor R).map f = dualMap R f.unop

noncomputable def TauCeti.FiniteProjectiveModules.evalIso (R : Type u) [CommRing R] (M : (finiteProjectiveModules R).FullSubcategory) : M ≅ dual R (dual R M)

A finite projective module is naturally isomorphic to its double dual.

Equations

• TauCeti.FiniteProjectiveModules.evalIso R M = (TauCeti.finiteProjectiveModules R).isoMk (Module.evalEquiv R ↑M.obj).toModuleIso

@[simp]

theorem TauCeti.FiniteProjectiveModules.evalIso_hom_hom (R : Type u) [CommRing R] (M : (finiteProjectiveModules R).FullSubcategory) : (evalIso R M).hom.hom = (Module.evalEquiv R ↑M.obj).toModuleIso.hom

The underlying module isomorphism of the double-dual map is the evaluation equivalence.

theorem TauCeti.FiniteProjectiveModules.evalIso_naturality (R : Type u) [CommRing R] {M N : (finiteProjectiveModules R).FullSubcategory} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp f (evalIso R N).hom = CategoryTheory.CategoryStruct.comp (evalIso R M).hom (dualMap R (dualMap R f))

The double-dual identification commutes with maps of finite projective modules.

theorem TauCeti.FiniteProjectiveModules.evalIso_naturality_assoc (R : Type u) [CommRing R] {M N : (finiteProjectiveModules R).FullSubcategory} (f : M ⟶ N) {Z : (finiteProjectiveModules R).FullSubcategory} (h : dual R (dual R N) ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (evalIso R N).hom h) = CategoryTheory.CategoryStruct.comp (evalIso R M).hom (CategoryTheory.CategoryStruct.comp (dualMap R (dualMap R f)) h)

The double-dual identification commutes with maps of finite projective modules.

noncomputable def TauCeti.FiniteProjectiveModules.evalNatIso (R : Type u) [CommRing R] : CategoryTheory.Functor.id (finiteProjectiveModules R).FullSubcategory ≅ (dualFunctor R).rightOp.comp (dualFunctor R)

Double-dual evaluation as a natural isomorphism on finite projective modules.

Equations

• TauCeti.FiniteProjectiveModules.evalNatIso R = CategoryTheory.NatIso.ofComponents (TauCeti.FiniteProjectiveModules.evalIso R) ⋯

@[simp]

theorem TauCeti.FiniteProjectiveModules.evalNatIso_hom_app (R : Type u) [CommRing R] (M : (finiteProjectiveModules R).FullSubcategory) : (evalNatIso R).hom.app M = (evalIso R M).hom

The forward component of evalNatIso is double-dual evaluation.

@[simp]

theorem TauCeti.FiniteProjectiveModules.evalNatIso_inv_app (R : Type u) [CommRing R] (M : (finiteProjectiveModules R).FullSubcategory) : (evalNatIso R).inv.app M = (evalIso R M).inv

The inverse component of evalNatIso is inverse double-dual evaluation.