From b728557c5e4aa9512ab007a41df6994375d30a04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 20 Apr 2026 11:16:37 +0200 Subject: [PATCH 1/4] chore(CategoryTheory): fix diamond for the preadditive structure on the opposite category --- Mathlib/Algebra/Homology/Opposite.lean | 5 ++--- Mathlib/CategoryTheory/Preadditive/Opposite.lean | 4 +++- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean index c4532f7c469d0f..ba331860bba056 100644 --- a/Mathlib/Algebra/Homology/Opposite.lean +++ b/Mathlib/Algebra/Homology/Opposite.lean @@ -374,7 +374,6 @@ lemma opcyclesOpIso_hom_naturality : (L.opcyclesOpIso i).hom ≫ (cyclesMap φ i).op := ShortComplex.opcyclesOpIso_hom_naturality ((shortComplexFunctor V c i).map φ) -set_option backward.isDefEq.respectTransparency false in -- This is needed in Algebra/Homology/Embedding/TruncLE.lean @[reassoc] lemma opcyclesOpIso_inv_naturality : (cyclesMap φ i).op ≫ (K.opcyclesOpIso i).inv = @@ -426,10 +425,10 @@ section variable [Preadditive V] -set_option backward.isDefEq.respectTransparency false in +example : Preadditive (HomologicalComplex Vᵒᵖ c) := inferInstance + instance opFunctor_additive : (@opFunctor ι V _ c _).Additive where -set_option backward.isDefEq.respectTransparency false in instance unopFunctor_additive : (@unopFunctor ι V _ c _).Additive where end diff --git a/Mathlib/CategoryTheory/Preadditive/Opposite.lean b/Mathlib/CategoryTheory/Preadditive/Opposite.lean index b231ff0ce9705a..4b5e284f8b0f05 100644 --- a/Mathlib/CategoryTheory/Preadditive/Opposite.lean +++ b/Mathlib/CategoryTheory/Preadditive/Opposite.lean @@ -25,7 +25,9 @@ namespace CategoryTheory variable (C : Type*) [Category* C] [Preadditive C] instance : Preadditive Cᵒᵖ where - homGroup X Y := Equiv.addCommGroup (opEquiv X Y) + homGroup X Y := + { toZero := inferInstance + __ := Equiv.addCommGroup (opEquiv X Y) } add_comp _ _ _ f f' g := Quiver.Hom.unop_inj (Preadditive.comp_add _ _ _ g.unop f.unop f'.unop) comp_add _ _ _ f g g' := Quiver.Hom.unop_inj (Preadditive.add_comp _ _ _ g.unop g'.unop f.unop) From 42710231de74827ac93c9187a354dcb86fde4c57 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 20 Apr 2026 11:20:44 +0200 Subject: [PATCH 2/4] fix --- Mathlib/Algebra/Homology/Opposite.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean index ba331860bba056..70e990dd9e73e7 100644 --- a/Mathlib/Algebra/Homology/Opposite.lean +++ b/Mathlib/Algebra/Homology/Opposite.lean @@ -374,6 +374,7 @@ lemma opcyclesOpIso_hom_naturality : (L.opcyclesOpIso i).hom ≫ (cyclesMap φ i).op := ShortComplex.opcyclesOpIso_hom_naturality ((shortComplexFunctor V c i).map φ) +set_option backward.isDefEq.respectTransparency false in @[reassoc] lemma opcyclesOpIso_inv_naturality : (cyclesMap φ i).op ≫ (K.opcyclesOpIso i).inv = From 3d849876544af51a62b5b9f40e8f60f242402e94 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 20 Apr 2026 11:21:30 +0200 Subject: [PATCH 3/4] fix --- Mathlib/Algebra/Homology/Opposite.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Homology/Opposite.lean b/Mathlib/Algebra/Homology/Opposite.lean index 70e990dd9e73e7..10e5d2d49f745b 100644 --- a/Mathlib/Algebra/Homology/Opposite.lean +++ b/Mathlib/Algebra/Homology/Opposite.lean @@ -374,7 +374,7 @@ lemma opcyclesOpIso_hom_naturality : (L.opcyclesOpIso i).hom ≫ (cyclesMap φ i).op := ShortComplex.opcyclesOpIso_hom_naturality ((shortComplexFunctor V c i).map φ) -set_option backward.isDefEq.respectTransparency false in +set_option backward.isDefEq.respectTransparency false in -- This is needed in Algebra/Homology/Embedding/TruncLE.lean @[reassoc] lemma opcyclesOpIso_inv_naturality : (cyclesMap φ i).op ≫ (K.opcyclesOpIso i).inv = From 7a62c773c044e8f6d74320979cb442793fafc1e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 20 Apr 2026 12:33:53 +0200 Subject: [PATCH 4/4] added test --- Mathlib/CategoryTheory/Preadditive/Opposite.lean | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/Mathlib/CategoryTheory/Preadditive/Opposite.lean b/Mathlib/CategoryTheory/Preadditive/Opposite.lean index 4b5e284f8b0f05..eea96f56183214 100644 --- a/Mathlib/CategoryTheory/Preadditive/Opposite.lean +++ b/Mathlib/CategoryTheory/Preadditive/Opposite.lean @@ -25,12 +25,16 @@ namespace CategoryTheory variable (C : Type*) [Category* C] [Preadditive C] instance : Preadditive Cᵒᵖ where - homGroup X Y := - { toZero := inferInstance - __ := Equiv.addCommGroup (opEquiv X Y) } + homGroup X Y := fast_instance% Equiv.addCommGroup (opEquiv X Y) add_comp _ _ _ f f' g := Quiver.Hom.unop_inj (Preadditive.comp_add _ _ _ g.unop f.unop f'.unop) comp_add _ _ _ f g g' := Quiver.Hom.unop_inj (Preadditive.add_comp _ _ _ g.unop g'.unop f.unop) +/-- Test that the two ways to obtain the `HasZeroMorphisms Cᵒᵖ` instance +from `Preadditive C` are the same. -/ +example : (instPreadditiveOpposite C).preadditiveHasZeroMorphisms = + @Limits.hasZeroMorphismsOpposite C _ Preadditive.preadditiveHasZeroMorphisms := by + with_reducible_and_instances rfl + instance moduleEndLeft {X Y : C} : Module (End X)ᵐᵒᵖ (X ⟶ Y) where smul_add _ _ _ := Preadditive.comp_add _ _ _ _ _ _ smul_zero _ := Limits.comp_zero