Conjugation of a Serre functor by a linear equivalence

This module keeps equivalence transport in the linear Serre core. It does not require a shift or a triangulated structure.

Main definitions

SerreFunctorData.conj D Φ is Serre duality on Φ.inverse ⋙ D.S ⋙ Φ.functor: the inverse moves both Hom arguments into the category where D.eta applies. SerreFunctorData.transportIso D Φ then uses uniqueness of Serre duality to identify Φ.functor ⋙ D.S with D.S ⋙ Φ.functor.

Main results

SerreFunctorData.transportIso_refl identifies its specialization to the identity equivalence with the canonical functor unitors. SerreFunctorData.conj_eta_trans and SerreFunctorData.conj_trans_uniqueIso_hom_app_eq_id give the duality and canonical comparison laws for a composite linear equivalence. SerreFunctorData.trace_transport shows that transport preserves the Serre trace. SerreFunctorData.transportIso_isoCompat makes transport natural in an isomorphism of equivalence functors, and SerreFunctorData.transportIso_trans identifies transport through a composite with successive transport.

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.conj {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (Φ : C ≌ C) [Φ.functor.Additive] [Functor.Linear k Φ.functor] : SerreFunctorData k C

Conjugation by a linear autoequivalence preserves Serre duality.

Equations

• D.conj Φ = { S := Φ.inverse.comp (D.S.comp Φ.functor), eta := CategoryTheory.SerreFunctor.SerreFunctorData.etaConj✝ D Φ, naturality_left := ⋯, naturality_right := ⋯ }

noncomputable def CategoryTheory.SerreFunctor.SerreFunctorData.transportIso {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (Φ : C ≌ C) [Φ.functor.Additive] [Functor.Linear k Φ.functor] : Φ.functor.comp D.S ≅ D.S.comp Φ.functor

A linear autoequivalence commutes with the chosen Serre functor up to a canonical natural isomorphism, by uniqueness of Serre duality.

Equations

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

theorem CategoryTheory.SerreFunctor.SerreFunctorData.conj_eta_trans {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (Φ Ψ : C ≌ C) [Φ.functor.Additive] [Functor.Linear k Φ.functor] [Ψ.functor.Additive] [Functor.Linear k Ψ.functor] (A B : C) (φ : Module.Dual k (A ⟶ B)) : ((D.conj (Φ.trans Ψ)).eta A B) φ = (((D.conj Φ).conj Ψ).eta A B) φ

Inverse Hom preimages for a composite equivalence run in reverse order; its composite counit then identifies the two transported Serre duality maps.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.conj_trans_uniqueIso_hom_app_eq_id {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (Φ Ψ : C ≌ C) [Φ.functor.Additive] [Functor.Linear k Φ.functor] [Ψ.functor.Additive] [Functor.Linear k Ψ.functor] (A : C) : ((D.conj (Φ.trans Ψ)).uniqueIso ((D.conj Φ).conj Ψ)).hom.app A = CategoryStruct.id ((D.conj (Φ.trans Ψ)).S.obj A)

Equality of the transported duality maps forces the canonical comparison between composite and successive conjugation to be the identity on each object.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.transportIso_refl {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) : D.transportIso Equivalence.refl = D.S.leftUnitor ≪≫ D.S.rightUnitor.symm

Reflexive η compatibility and Serre uniqueness normalize transport by the identity equivalence to the functor unitors. This states no shift coherence.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.trace_transport {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (Φ : C ≌ C) [Φ.functor.Additive] [Functor.Linear k Φ.functor] (X : C) (x : X ⟶ D.S.obj X) : (D.trace (Φ.functor.obj X)) (CategoryStruct.comp (Φ.functor.map x) ((D.transportIso Φ).inv.app X)) = (D.trace X) x

Transport by a linear autoequivalence preserves the Serre trace. The inverse component sends the mapped morphism into the Serre target at the image.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.transportIso_isoCompat {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (Φ : C ≌ C) [Φ.functor.Additive] [Functor.Linear k Φ.functor] (Ψ : C ≌ C) [Ψ.functor.Additive] [Functor.Linear k Ψ.functor] (e : Φ.functor ≅ Ψ.functor) (A : C) : CategoryStruct.comp (e.hom.app (D.S.obj A)) ((D.transportIso Ψ).inv.app A) = CategoryStruct.comp ((D.transportIso Φ).inv.app A) (D.S.map (e.hom.app A))

Transport is natural in an isomorphism of linear equivalence functors. The comparison is detected by the nondegenerate Serre pairing and trace.

theorem CategoryTheory.SerreFunctor.SerreFunctorData.transportIso_trans {k : Type w} [Field k] {C : Type u} [Category.{v, u} C] [Preadditive C] [Linear k C] (D : SerreFunctorData k C) (Φ : C ≌ C) [Φ.functor.Additive] [Functor.Linear k Φ.functor] (Ψ : C ≌ C) [Ψ.functor.Additive] [Functor.Linear k Ψ.functor] (A : C) : (D.transportIso (Φ.trans Ψ)).inv.app A = CategoryStruct.comp (Ψ.functor.map ((D.transportIso Φ).inv.app A)) ((D.transportIso Ψ).inv.app (Φ.functor.obj A))

Compare both transports through the Serre pairing: trace preservation and full faithfulness determine their inverse components without expanding composite unit and counit maps.