From 97025d7f6bff8c6dd12fcccdce102d6e0eee778a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 30 Jul 2023 12:30:36 +0530 Subject: [PATCH 1/4] feat: short complexes in functor categories --- Mathlib.lean | 1 + .../ShortComplex/FunctorEquivalence.lean | 78 +++++++++++++++++++ .../Limits/Preserves/Shapes/Zero.lean | 3 + 3 files changed, 82 insertions(+) create mode 100644 Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean diff --git a/Mathlib.lean b/Mathlib.lean index c41cdc78ab79b..2119b21bf78d6 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -220,6 +220,7 @@ import Mathlib.Algebra.Homology.ModuleCat import Mathlib.Algebra.Homology.Opposite import Mathlib.Algebra.Homology.QuasiIso import Mathlib.Algebra.Homology.ShortComplex.Basic +import Mathlib.Algebra.Homology.ShortComplex.FunctorEquivalence import Mathlib.Algebra.Homology.ShortComplex.Homology import Mathlib.Algebra.Homology.ShortComplex.LeftHomology import Mathlib.Algebra.Homology.ShortComplex.RightHomology diff --git a/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean b/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean new file mode 100644 index 0000000000000..09db227fa71be --- /dev/null +++ b/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2023 Joël Riou. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joël Riou +-/ +import Mathlib.Algebra.Homology.ShortComplex.Basic + +/-! +# Short complexes in functor categories + +In this file, it is shown that if `J` and `C` are two categories (such +that `C` has zero morphisms), then there is an equivalence of categories +`ShortComplex.functorEquivalence J C : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. + +-/ + +namespace CategoryTheory + +open Limits + +variable (J C : Type _) [Category J] [Category C] [HasZeroMorphisms C] + +namespace ShortComplex + +namespace FunctorEquivalence + +attribute [local simp] ShortComplex.Hom.comm₁₂ ShortComplex.Hom.comm₂₃ + +/-- The obvious functor `(ShortComplex (J ⥤ C)) ⥤ (J ⥤ ShortComplex C)`. -/ +@[simps] +def functor : (ShortComplex (J ⥤ C)) ⥤ (J ⥤ ShortComplex C) where + obj S := + { obj := fun j => S.map ((evaluation J C).obj j) + map := fun f => S.mapNatTrans ((evaluation J C).map f) } + map φ := + { app := fun j => ((evaluation J C).obj j).mapShortComplex.map φ } + +/-- The obvious functor `(J ⥤ ShortComplex C) ⥤ (ShortComplex (J ⥤ C))`. -/ +@[simps] +def inverse : (J ⥤ ShortComplex C) ⥤ (ShortComplex (J ⥤ C)) where + obj F := + { f := whiskerLeft F π₁Toπ₂ + g := whiskerLeft F π₂Toπ₃ + zero := by aesop_cat } + map φ := Hom.mk (whiskerRight φ π₁) (whiskerRight φ π₂) (whiskerRight φ π₃) + (by aesop_cat) (by aesop_cat) + +/-- The unit isomorphism of the equivalence +`ShortComplex.functorEquivalence : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. -/ +@[simps!] +def unitIso : 𝟭 _ ≅ functor J C ⋙ inverse J C := + NatIso.ofComponents (fun _ => isoMk + (NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)) + (NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)) + (NatIso.ofComponents (fun _ => Iso.refl _) (by aesop_cat)) + (by aesop_cat) (by aesop_cat)) (by aesop_cat) + +/-- The counit isomorphism of the equivalence +`ShortComplex.functorEquivalence : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. -/ +@[simps!] +def counitIso : inverse J C ⋙ functor J C ≅ 𝟭 _:= + NatIso.ofComponents (fun _ => NatIso.ofComponents + (fun _ => isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _) + (by aesop_cat) (by aesop_cat)) (by aesop_cat)) (by aesop_cat) + +end FunctorEquivalence + +/-- The obvious equivalence `(ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. -/ +@[simps] +def functorEquivalence : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C) where + functor := FunctorEquivalence.functor J C + inverse := FunctorEquivalence.inverse J C + unitIso := FunctorEquivalence.unitIso J C + counitIso := FunctorEquivalence.counitIso J C + +end ShortComplex + +end CategoryTheory diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean index e3fdc86c126f9..77df756cf51d2 100644 --- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean +++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean @@ -101,6 +101,9 @@ instance (priority := 100) preservesZeroMorphisms_of_full (F : C ⥤ D) [Full F] _ = 0 := by rw [F.map_comp, F.image_preimage, comp_zero] #align category_theory.functor.preserves_zero_morphisms_of_full CategoryTheory.Functor.preservesZeroMorphisms_of_full +instance preservesZeroMorphisms_evaluation (j : D) : + PreservesZeroMorphisms ((evaluation D C).obj j) where + end ZeroMorphisms section ZeroObject From 0e170c22b6554a7e63884854d079073e132d580e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 30 Jul 2023 12:32:21 +0530 Subject: [PATCH 2/4] better name --- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean index 77df756cf51d2..f998f0aa2745a 100644 --- a/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean +++ b/Mathlib/CategoryTheory/Limits/Preserves/Shapes/Zero.lean @@ -101,7 +101,7 @@ instance (priority := 100) preservesZeroMorphisms_of_full (F : C ⥤ D) [Full F] _ = 0 := by rw [F.map_comp, F.image_preimage, comp_zero] #align category_theory.functor.preserves_zero_morphisms_of_full CategoryTheory.Functor.preservesZeroMorphisms_of_full -instance preservesZeroMorphisms_evaluation (j : D) : +instance preservesZeroMorphisms_evaluation_obj (j : D) : PreservesZeroMorphisms ((evaluation D C).obj j) where end ZeroMorphisms From f4019129824207531fe84c6fd611669cbabf6ef6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Sun, 30 Jul 2023 12:34:53 +0530 Subject: [PATCH 3/4] removed unneccesary parentheses --- .../ShortComplex/FunctorEquivalence.lean | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean b/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean index 09db227fa71be..eee9bef73f466 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean @@ -26,18 +26,18 @@ namespace FunctorEquivalence attribute [local simp] ShortComplex.Hom.comm₁₂ ShortComplex.Hom.comm₂₃ -/-- The obvious functor `(ShortComplex (J ⥤ C)) ⥤ (J ⥤ ShortComplex C)`. -/ +/-- The obvious functor `ShortComplex (J ⥤ C) ⥤ J ⥤ ShortComplex C`. -/ @[simps] -def functor : (ShortComplex (J ⥤ C)) ⥤ (J ⥤ ShortComplex C) where +def functor : ShortComplex (J ⥤ C) ⥤ J ⥤ ShortComplex C where obj S := { obj := fun j => S.map ((evaluation J C).obj j) map := fun f => S.mapNatTrans ((evaluation J C).map f) } map φ := { app := fun j => ((evaluation J C).obj j).mapShortComplex.map φ } -/-- The obvious functor `(J ⥤ ShortComplex C) ⥤ (ShortComplex (J ⥤ C))`. -/ +/-- The obvious functor `(J ⥤ ShortComplex C) ⥤ ShortComplex (J ⥤ C)`. -/ @[simps] -def inverse : (J ⥤ ShortComplex C) ⥤ (ShortComplex (J ⥤ C)) where +def inverse : (J ⥤ ShortComplex C) ⥤ ShortComplex (J ⥤ C) where obj F := { f := whiskerLeft F π₁Toπ₂ g := whiskerLeft F π₂Toπ₃ @@ -46,7 +46,7 @@ def inverse : (J ⥤ ShortComplex C) ⥤ (ShortComplex (J ⥤ C)) where (by aesop_cat) (by aesop_cat) /-- The unit isomorphism of the equivalence -`ShortComplex.functorEquivalence : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. -/ +`ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`. -/ @[simps!] def unitIso : 𝟭 _ ≅ functor J C ⋙ inverse J C := NatIso.ofComponents (fun _ => isoMk @@ -56,7 +56,7 @@ def unitIso : 𝟭 _ ≅ functor J C ⋙ inverse J C := (by aesop_cat) (by aesop_cat)) (by aesop_cat) /-- The counit isomorphism of the equivalence -`ShortComplex.functorEquivalence : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. -/ +`ShortComplex.functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`. -/ @[simps!] def counitIso : inverse J C ⋙ functor J C ≅ 𝟭 _:= NatIso.ofComponents (fun _ => NatIso.ofComponents @@ -65,9 +65,9 @@ def counitIso : inverse J C ⋙ functor J C ≅ 𝟭 _:= end FunctorEquivalence -/-- The obvious equivalence `(ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. -/ +/-- The obvious equivalence `ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`. -/ @[simps] -def functorEquivalence : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C) where +def functorEquivalence : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C where functor := FunctorEquivalence.functor J C inverse := FunctorEquivalence.inverse J C unitIso := FunctorEquivalence.unitIso J C From 2cfb049b363e2535792c59d294ddb350b4e55cd8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Jo=C3=ABl=20Riou?= Date: Mon, 31 Jul 2023 13:54:04 +0530 Subject: [PATCH 4/4] removed unnecessary parentheses --- Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean b/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean index eee9bef73f466..140895149c529 100644 --- a/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean +++ b/Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean @@ -10,7 +10,7 @@ import Mathlib.Algebra.Homology.ShortComplex.Basic In this file, it is shown that if `J` and `C` are two categories (such that `C` has zero morphisms), then there is an equivalence of categories -`ShortComplex.functorEquivalence J C : (ShortComplex (J ⥤ C)) ≌ (J ⥤ ShortComplex C)`. +`ShortComplex.functorEquivalence J C : ShortComplex (J ⥤ C) ≌ J ⥤ ShortComplex C`. -/