Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat: the homological functor on the homotopy category of cochain complexes in an abelian category #11760

Closed
wants to merge 29 commits into from
Closed
Show file tree
Hide file tree
Changes from 26 commits
Commits
Show all changes
29 commits
Select commit Hold shift + click to select a range
2865b80
feat(CategoryTheory): triangulated subcategories
joelriou Mar 28, 2024
58bd6d3
feat(CategoryTheory/Triangulated): homological functors
joelriou Mar 28, 2024
0fa5280
fixing Mathlib.lean
joelriou Mar 28, 2024
05af53c
coding style
joelriou Mar 28, 2024
6da2115
one more constructor
joelriou Mar 29, 2024
42656e4
feat: the homological functor on the homotopy category of an abelian …
joelriou Mar 29, 2024
73051a1
cleaning up
joelriou Mar 29, 2024
bd494bb
added docstrings
joelriou Mar 29, 2024
7225e05
Merge remote-tracking branch 'origin' into triangulated-subcategory
joelriou Mar 30, 2024
fa0c448
followed @TwoFX suggestions
joelriou Mar 30, 2024
7e48b5f
replaces sets by predicates
joelriou Mar 30, 2024
dd4cd80
fixed coding style
joelriou Mar 30, 2024
f05ab7b
added isIso variants
joelriou Mar 30, 2024
dbde1b9
Merge remote-tracking branch 'origin/triangulated-subcategory' into h…
joelriou Mar 30, 2024
a07dd2f
fixed the build
joelriou Mar 30, 2024
7f09d1e
Merge remote-tracking branch 'origin/homological-functor' into homoto…
joelriou Mar 30, 2024
280bb5f
Merge remote-tracking branch 'origin' into homotopy-category-homologi…
joelriou Mar 31, 2024
5de084d
Merge remote-tracking branch 'origin' into triangulated-subcategory
joelriou Apr 12, 2024
d5c8df7
Merge remote-tracking branch 'origin' into triangulated-subcategory
joelriou Apr 18, 2024
8d93376
fixing names
joelriou Apr 18, 2024
447e037
fixed def of isoClosure
joelriou Apr 18, 2024
79edf14
fixed names
joelriou Apr 18, 2024
4f5cd42
Merge remote-tracking branch 'origin/triangulated-subcategory' into h…
joelriou Apr 18, 2024
14e636f
Merge remote-tracking branch 'origin/homological-functor' into homoto…
joelriou Apr 18, 2024
73fd877
Merge remote-tracking branch 'origin' into homotopy-category-homologi…
joelriou Apr 30, 2024
f355a73
typo
joelriou Apr 30, 2024
bbc50bf
Merge remote-tracking branch 'origin' into homotopy-category-homologi…
joelriou May 8, 2024
118dc36
Merge remote-tracking branch 'origin' into homotopy-category-homologi…
joelriou May 9, 2024
406d7bb
shortened names
joelriou May 9, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -268,6 +268,7 @@ import Mathlib.Algebra.Homology.ExactSequence
import Mathlib.Algebra.Homology.Functor
import Mathlib.Algebra.Homology.HomologicalBicomplex
import Mathlib.Algebra.Homology.HomologicalComplex
import Mathlib.Algebra.Homology.HomologicalComplexAbelian
import Mathlib.Algebra.Homology.HomologicalComplexBiprod
import Mathlib.Algebra.Homology.HomologicalComplexLimits
import Mathlib.Algebra.Homology.Homology
Expand All @@ -277,6 +278,7 @@ import Mathlib.Algebra.Homology.HomotopyCategory
import Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
import Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
import Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
import Mathlib.Algebra.Homology.HomotopyCategory.HomologicalFunctor
import Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
import Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
import Mathlib.Algebra.Homology.HomotopyCategory.Shift
Expand Down
14 changes: 14 additions & 0 deletions Mathlib/Algebra/Homology/HomologicalComplex.lean
Original file line number Diff line number Diff line change
Expand Up @@ -332,6 +332,20 @@ theorem congr_hom {C D : HomologicalComplex V c} {f g : C ⟶ D} (w : f = g) (i
congr_fun (congr_arg Hom.f w) i
#align homological_complex.congr_hom HomologicalComplex.congr_hom

lemma mono_of_mono_f {K L : HomologicalComplex V c} (φ : K ⟶ L)
(hφ : ∀ i, Mono (φ.f i)) : Mono φ where
right_cancellation g h eq := by
ext i
rw [← cancel_mono (φ.f i)]
exact congr_hom eq i

lemma epi_of_epi_f {K L : HomologicalComplex V c} (φ : K ⟶ L)
(hφ : ∀ i, Epi (φ.f i)) : Epi φ where
left_cancellation g h eq := by
ext i
rw [← cancel_epi (φ.f i)]
exact congr_hom eq i

section

variable (V c)
Expand Down
70 changes: 70 additions & 0 deletions Mathlib/Algebra/Homology/HomologicalComplexAbelian.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,70 @@
/-
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.Additive
import Mathlib.Algebra.Homology.HomologicalComplexLimits
import Mathlib.Algebra.Homology.ShortComplex.ShortExact

/-! # THe category of homological complexes is abelian

If `C` is an abelian category, then `HomologicalComplex C c` is an abelian
category for any complex shape `c : ComplexShape ι`.

We also obtain that a short complex in `HomologicalComplex C c`
is exact (resp. short exact) iff degreewise it is so.

-/

open CategoryTheory Category Limits

namespace HomologicalComplex

variable {C ι : Type*} {c : ComplexShape ι} [Category C] [Abelian C]

noncomputable instance : NormalEpiCategory (HomologicalComplex C c) := ⟨fun p _ =>
NormalEpi.mk _ (kernel.ι p) (kernel.condition _)
(isColimitOfEval _ _ (fun _ =>
Abelian.isColimitMapCoconeOfCokernelCoforkOfπKernelConditionOfEpi _ _))⟩

noncomputable instance : NormalMonoCategory (HomologicalComplex C c) := ⟨fun p _ =>
NormalMono.mk _ (cokernel.π p) (cokernel.condition _)
(isLimitOfEval _ _ (fun _ =>
Abelian.isLimitMapConeOfKernelForkOfιCokernelConditionOfMono _ _))⟩

noncomputable instance : Abelian (HomologicalComplex C c) where

variable (S : ShortComplex (HomologicalComplex C c))

lemma exact_of_degreewise_exact (hS : ∀ (i : ι), (S.map (eval C c i)).Exact) :
S.Exact := by
simp only [ShortComplex.exact_iff_isZero_homology] at hS ⊢
rw [IsZero.iff_id_eq_zero]
ext i
apply (IsZero.of_iso (hS i) (S.mapHomologyIso (eval C c i)).symm).eq_of_src

lemma shortExact_of_degreewise_shortExact
(hS : ∀ (i : ι), (S.map (eval C c i)).ShortExact) :
S.ShortExact where
mono_f := mono_of_mono_f _ (fun i => (hS i).mono_f)
epi_g := epi_of_epi_f _ (fun i => (hS i).epi_g)
exact := exact_of_degreewise_exact S (fun i => (hS i).exact)

lemma exact_iff_degreewise_exact :
S.Exact ↔ ∀ (i : ι), (S.map (eval C c i)).Exact := by
constructor
· intro hS i
exact hS.map (eval C c i)
· exact exact_of_degreewise_exact S

lemma shortExact_iff_degreewise_shortExact :
S.ShortExact ↔ ∀ (i : ι), (S.map (eval C c i)).ShortExact := by
constructor
· intro hS i
have := hS.mono_f
have := hS.epi_g
exact hS.map (eval C c i)
· exact shortExact_of_degreewise_shortExact S

end HomologicalComplex
37 changes: 37 additions & 0 deletions Mathlib/Algebra/Homology/HomotopyCategory/HomologicalFunctor.lean
Original file line number Diff line number Diff line change
@@ -0,0 +1,37 @@
/-
Copyright (c) 2024 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.HomologicalComplexAbelian
import Mathlib.Algebra.Homology.HomotopyCategory.DegreewiseSplit
import Mathlib.Algebra.Homology.HomologySequence
import Mathlib.CategoryTheory.Triangulated.HomologicalFunctor

/-! The homological functor

In this file, it is shown that if `C` is an abelian category,
then `homologyFunctor C (ComplexShape.up ℤ) n` is a homological functor
`HomotopyCategory C (ComplexShape.up ℤ) ⥤ C`. As distinguished triangles
in the homotopy category can be characterized in terms of degreewise split
short exact sequences of cochain complexes, this follows from the homology
sequence of a short exact sequences of homological complexes.

-/

open CategoryTheory

variable {C : Type*} [Category C] [Abelian C]

namespace HomotopyCategory

instance (n : ℤ) : (homologyFunctor C (ComplexShape.up ℤ) n).IsHomological :=
Functor.IsHomological.mk' _ (fun T hT => by
rw [distinguished_iff_iso_trianglehOfDegreewiseSplit] at hT
obtain ⟨S, σ, ⟨e⟩⟩ := hT
have hS := HomologicalComplex.shortExact_of_degreewise_shortExact S
(fun n => (σ n).shortExact)
exact ⟨_, e, (ShortComplex.exact_iff_of_iso
(S.mapNatIso (homologyFunctorFactors C (ComplexShape.up ℤ) n))).2 (hS.homology_exact₂ n)⟩)

end HomotopyCategory
39 changes: 39 additions & 0 deletions Mathlib/CategoryTheory/Abelian/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ Authors: Markus Himmel, Johan Commelin, Scott Morrison
-/
import Mathlib.CategoryTheory.Limits.Constructions.Pullbacks
import Mathlib.CategoryTheory.Preadditive.Biproducts
import Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
import Mathlib.CategoryTheory.Limits.Shapes.Images
import Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
import Mathlib.CategoryTheory.Abelian.NonPreadditive
Expand Down Expand Up @@ -498,6 +499,44 @@ theorem monoLift_comp [Mono f] {T : C} (g : T ⟶ Y) (hg : g ≫ cokernel.π f =
WalkingParallelPair.zero
#align category_theory.abelian.mono_lift_comp CategoryTheory.Abelian.monoLift_comp

section

variable {D : Type*} [Category D] [HasZeroMorphisms D]

/-- If `F : D ⥤ C` is a functor to an abelian category, `i : X ⟶ Y` is a morphism
admitting a cokernel such that `F` preserves this cokernel and `F.map i` is a mono,
then `F.map X` identifies to the kernel of `F.map (cokernel.π i)`. -/
noncomputable def isLimitMapConeOfKernelForkOfιCokernelConditionOfMono
joelriou marked this conversation as resolved.
Show resolved Hide resolved
{X Y : D} (i : X ⟶ Y) [HasCokernel i] (F : D ⥤ C)
[F.PreservesZeroMorphisms] [Mono (F.map i)]
[PreservesColimit (parallelPair i 0) F] :
IsLimit (F.mapCone (KernelFork.ofι i (cokernel.condition i))) := by
let e : parallelPair (cokernel.π (F.map i)) 0 ≅ parallelPair (cokernel.π i) 0 ⋙ F :=
parallelPair.ext (Iso.refl _) (asIso (cokernelComparison i F)) (by simp) (by simp)
refine' IsLimit.postcomposeInvEquiv e _ _
let hi := Abelian.monoIsKernelOfCokernel _ (cokernelIsCokernel (F.map i))
refine' IsLimit.ofIsoLimit hi (Fork.ext (Iso.refl _) _)
change 𝟙 _ ≫ F.map i ≫ 𝟙 _ = F.map i
rw [Category.comp_id, Category.id_comp]

/-- If `F : D ⥤ C` is a functor to an abelian category, `p : X ⟶ Y` is a morphisms
admitting a kernel such that `F` preserves this kernel and `F.map p` is an epi,
then `F.map Y` identifies to the cokernel of `F.map (kernel.ι p)`. -/
noncomputable def isColimitMapCoconeOfCokernelCoforkOfπKernelConditionOfEpi
{X Y : D} (p : X ⟶ Y) [HasKernel p] (F : D ⥤ C)
[F.PreservesZeroMorphisms] [Epi (F.map p)]
[PreservesLimit (parallelPair p 0) F] :
IsColimit (F.mapCocone (CokernelCofork.ofπ p (kernel.condition p))) := by
let e : parallelPair (kernel.ι p) 0 ⋙ F ≅ parallelPair (kernel.ι (F.map p)) 0 :=
parallelPair.ext (asIso (kernelComparison p F)) (Iso.refl _) (by simp) (by simp)
refine' IsColimit.precomposeInvEquiv e _ _
let hp := Abelian.epiIsCokernelOfKernel _ (kernelIsKernel (F.map p))
refine' IsColimit.ofIsoColimit hp (Cofork.ext (Iso.refl _) _)
change F.map p ≫ 𝟙 _ = 𝟙 _ ≫ F.map p
rw [Category.comp_id, Category.id_comp]

end

end CokernelOfKernel

section
Expand Down
Loading