Transport of the zigzag laws along isomorphisms

An isomorphism is a section–retraction pair whose composite idempotent is the identity, so the adjointness condition of the transfer is vacuous and the zigzag laws pass across without any further hypothesis.

noncomputable def RS.ModDualityDatum.transferIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (i : Q ≅ P) (i' : Q' ≅ P') : ModDualityDatum A Q Q'

Transport of a duality datum along isomorphisms of the two modules.

Equations

• RS.ModDualityDatum.transferIso A d₀ i i' = RS.ModDualityDatum.transfer A d₀ i.hom i'.hom i.inv i'.inv

theorem RS.transferIso_adj {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (i : Q ≅ P) (i' : Q' ≅ P') : CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.comp i'.inv i'.hom) (CategoryTheory.CategoryStruct.id P)) d₀.pair = CategoryTheory.CategoryStruct.comp (modTensorMap A (CategoryTheory.CategoryStruct.id P') (CategoryTheory.CategoryStruct.comp i.inv i.hom)) d₀.pair

The adjointness condition of the transfer is vacuous for isomorphisms: both composite idempotents are identities.

theorem RS.modZigzagDatum_transferIso {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.Preadditive D] [CategoryTheory.MonoidalPreadditive D] [CategoryTheory.Limits.HasFiniteBiproducts D] [CategoryTheory.Limits.HasCoequalizers D] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorLeft Z)] [∀ (Z : D), CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair (CategoryTheory.MonoidalCategory.tensorRight Z)] (A : D) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] {P P' Q Q' : CategoryTheory.Mod D A} (d₀ : ModDualityDatum A P P') (i : Q ≅ P) (i' : Q' ≅ P') (hz₀ : ModZigzagDatum A d₀) : ModZigzagDatum A (ModDualityDatum.transferIso A d₀ i i')

The zigzag laws transport along isomorphisms.