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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat(Algebra/Homology): relax assumptions for Functor.mapHomologicalComplex #12174

Closed
wants to merge 1 commit into from
Closed

[Merged by Bors] - feat(Algebra/Homology): relax assumptions for Functor.mapHomologicalComplex #12174

Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
87 changes: 48 additions & 39 deletions Mathlib/Algebra/Homology/Additive.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ open CategoryTheory CategoryTheory.Category CategoryTheory.Limits HomologicalCom

variable {ι : Type*}
variable {V : Type u} [Category.{v} V] [Preadditive V]
variable {W : Type*} [Category W] [Preadditive W]
variable {W₁ W₂ : Type*} [Category W₁] [Category W₂] [HasZeroMorphisms W₁] [HasZeroMorphisms W₂]
variable {c : ComplexShape ι} {C D E : HomologicalComplex V c}
variable (f g : C ⟶ D) (h k : D ⟶ E) (i : ι)

Expand Down Expand Up @@ -136,14 +138,12 @@ end HomologicalComplex

namespace CategoryTheory

variable {W : Type*} [Category W] [Preadditive W]

/-- An additive functor induces a functor between homological complexes.
This is sometimes called the "prolongation".
-/
@[simps]
def Functor.mapHomologicalComplex (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) :
HomologicalComplex V c ⥤ HomologicalComplex W c where
def Functor.mapHomologicalComplex (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) :
HomologicalComplex W₁ c ⥤ HomologicalComplex W₂ c where
obj C :=
{ X := fun i => F.obj (C.X i)
d := fun i j => F.map (C.d i j)
Expand All @@ -158,59 +158,66 @@ def Functor.mapHomologicalComplex (F : V ⥤ W) [F.Additive] (c : ComplexShape
rw [← F.map_comp, ← F.map_comp, f.comm] }
#align category_theory.functor.map_homological_complex CategoryTheory.Functor.mapHomologicalComplex

variable (V)
instance (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] (c : ComplexShape ι) :
(F.mapHomologicalComplex c).PreservesZeroMorphisms where

instance Functor.map_homogical_complex_additive (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) :
(F.mapHomologicalComplex c).Additive where
#align category_theory.functor.map_homogical_complex_additive CategoryTheory.Functor.map_homogical_complex_additive

variable (W₁)

/-- The functor on homological complexes induced by the identity functor is
isomorphic to the identity functor. -/
@[simps!]
def Functor.mapHomologicalComplexIdIso (c : ComplexShape ι) :
(𝟭 V).mapHomologicalComplex c ≅ 𝟭 _ :=
(𝟭 W₁).mapHomologicalComplex c ≅ 𝟭 _ :=
NatIso.ofComponents fun K => Hom.isoOfComponents fun i => Iso.refl _
#align category_theory.functor.map_homological_complex_id_iso CategoryTheory.Functor.mapHomologicalComplexIdIso

variable {V}

instance Functor.map_homogical_complex_additive (F : V ⥤ W) [F.Additive] (c : ComplexShape ι) :
(F.mapHomologicalComplex c).Additive where
#align category_theory.functor.map_homogical_complex_additive CategoryTheory.Functor.map_homogical_complex_additive

instance Functor.mapHomologicalComplex_reflects_iso (F : V ⥤ W) [F.Additive]
instance Functor.mapHomologicalComplex_reflects_iso (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms]
[ReflectsIsomorphisms F] (c : ComplexShape ι) :
ReflectsIsomorphisms (F.mapHomologicalComplex c) :=
⟨fun f => by
intro
haveI : ∀ n : ι, IsIso (F.map (f.f n)) := fun n =>
IsIso.of_iso
((HomologicalComplex.eval W c n).mapIso (asIso ((F.mapHomologicalComplex c).map f)))
((HomologicalComplex.eval W₂ c n).mapIso (asIso ((F.mapHomologicalComplex c).map f)))
haveI := fun n => isIso_of_reflects_iso (f.f n) F
exact HomologicalComplex.Hom.isIso_of_components f⟩
#align category_theory.functor.map_homological_complex_reflects_iso CategoryTheory.Functor.mapHomologicalComplex_reflects_iso

variable {W₁}

/-- A natural transformation between functors induces a natural transformation
between those functors applied to homological complexes.
-/
@[simps]
def NatTrans.mapHomologicalComplex {F G : V ⥤ W} [F.Additive] [G.Additive] (α : F ⟶ G)
def NatTrans.mapHomologicalComplex {F G : W₁ ⥤ W₂}
[F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] (α : F ⟶ G)
(c : ComplexShape ι) : F.mapHomologicalComplex c ⟶ G.mapHomologicalComplex c where
app C := { f := fun i => α.app _ }
#align category_theory.nat_trans.map_homological_complex CategoryTheory.NatTrans.mapHomologicalComplex

@[simp]
theorem NatTrans.mapHomologicalComplex_id (c : ComplexShape ι) (F : V ⥤ W) [F.Additive] :
theorem NatTrans.mapHomologicalComplex_id
(c : ComplexShape ι) (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] :
NatTrans.mapHomologicalComplex (𝟙 F) c = 𝟙 (F.mapHomologicalComplex c) := by aesop_cat
#align category_theory.nat_trans.map_homological_complex_id CategoryTheory.NatTrans.mapHomologicalComplex_id

@[simp]
theorem NatTrans.mapHomologicalComplex_comp (c : ComplexShape ι) {F G H : V ⥤ W} [F.Additive]
[G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) :
theorem NatTrans.mapHomologicalComplex_comp (c : ComplexShape ι) {F G H : W₁ ⥤ W₂}
[F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms] [H.PreservesZeroMorphisms]
(α : F ⟶ G) (β : G ⟶ H) :
NatTrans.mapHomologicalComplex (α ≫ β) c =
NatTrans.mapHomologicalComplex α c ≫ NatTrans.mapHomologicalComplex β c :=
by aesop_cat
#align category_theory.nat_trans.map_homological_complex_comp CategoryTheory.NatTrans.mapHomologicalComplex_comp

@[reassoc (attr := simp 1100)]
theorem NatTrans.mapHomologicalComplex_naturality {c : ComplexShape ι} {F G : V ⥤ W} [F.Additive]
[G.Additive] (α : F ⟶ G) {C D : HomologicalComplex V c} (f : C ⟶ D) :
theorem NatTrans.mapHomologicalComplex_naturality {c : ComplexShape ι} {F G : W₁ ⥤ W₂}
[F.PreservesZeroMorphisms] [G.PreservesZeroMorphisms]
(α : F ⟶ G) {C D : HomologicalComplex W₁ c} (f : C ⟶ D) :
(F.mapHomologicalComplex c).map f ≫ (NatTrans.mapHomologicalComplex α c).app D =
(NatTrans.mapHomologicalComplex α c).app C ≫ (G.mapHomologicalComplex c).map f :=
by aesop_cat
Expand All @@ -220,8 +227,9 @@ theorem NatTrans.mapHomologicalComplex_naturality {c : ComplexShape ι} {F G : V
between those functors applied to homological complexes.
-/
@[simps!]
def NatIso.mapHomologicalComplex {F G : V ⥤ W} [F.Additive] [G.Additive] (α : F ≅ G)
(c : ComplexShape ι) : F.mapHomologicalComplex c ≅ G.mapHomologicalComplex c where
def NatIso.mapHomologicalComplex {F G : W₁ ⥤ W₂} [F.PreservesZeroMorphisms]
[G.PreservesZeroMorphisms] (α : F ≅ G) (c : ComplexShape ι) :
F.mapHomologicalComplex c ≅ G.mapHomologicalComplex c where
hom := NatTrans.mapHomologicalComplex α.hom c
inv := NatTrans.mapHomologicalComplex α.inv c
hom_inv_id := by simp only [← NatTrans.mapHomologicalComplex_comp, α.hom_inv_id,
Expand All @@ -234,24 +242,25 @@ def NatIso.mapHomologicalComplex {F G : V ⥤ W} [F.Additive] [G.Additive] (α :
of homological complex.
-/
@[simps]
def Equivalence.mapHomologicalComplex (e : V ≌ W) [e.functor.Additive] (c : ComplexShape ι) :
HomologicalComplex V c ≌ HomologicalComplex W c where
def Equivalence.mapHomologicalComplex (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms]
(c : ComplexShape ι) :
HomologicalComplex W₁ c ≌ HomologicalComplex W₂ c where
functor := e.functor.mapHomologicalComplex c
inverse := e.inverse.mapHomologicalComplex c
unitIso :=
(Functor.mapHomologicalComplexIdIso V c).symm ≪≫ NatIso.mapHomologicalComplex e.unitIso c
counitIso := NatIso.mapHomologicalComplex e.counitIso c ≪≫ Functor.mapHomologicalComplexIdIso W c
(Functor.mapHomologicalComplexIdIso W₁ c).symm ≪≫ NatIso.mapHomologicalComplex e.unitIso c
counitIso := NatIso.mapHomologicalComplex e.counitIso c ≪≫
Functor.mapHomologicalComplexIdIso W₂ c
#align category_theory.equivalence.map_homological_complex CategoryTheory.Equivalence.mapHomologicalComplex

end CategoryTheory

namespace ChainComplex

variable {W : Type*} [Category W] [Preadditive W]
variable {α : Type*} [AddRightCancelSemigroup α] [One α] [DecidableEq α]

theorem map_chain_complex_of (F : V ⥤ W) [F.Additive] (X : α → V) (d : ∀ n, X (n + 1) ⟶ X n)
(sq : ∀ n, d (n + 1) ≫ d n = 0) :
theorem map_chain_complex_of (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms] (X : α → W₁)
(d : ∀ n, X (n + 1) ⟶ X n) (sq : ∀ n, d (n + 1) ≫ d n = 0) :
(F.mapHomologicalComplex _).obj (ChainComplex.of X d sq) =
ChainComplex.of (fun n => F.obj (X n)) (fun n => F.map (d n)) fun n => by
rw [← F.map_comp, sq n, Functor.map_zero] := by
Expand All @@ -263,16 +272,18 @@ theorem map_chain_complex_of (F : V ⥤ W) [F.Additive] (X : α → V) (d : ∀

end ChainComplex

variable [HasZeroObject V] {W : Type*} [Category W] [Preadditive W] [HasZeroObject W]
variable [HasZeroObject W₁] [HasZeroObject W₂]

namespace HomologicalComplex

variable (F : W₁ ⥤ W₂) [F.PreservesZeroMorphisms]
(c : ComplexShape ι) [DecidableEq ι]

/-- Turning an object into a complex supported at `j` then applying a functor is
the same as applying the functor then forming the complex.
-/
noncomputable def singleMapHomologicalComplex (F : V ⥤ W) [F.Additive] (c : ComplexShape ι)
[DecidableEq ι] (j : ι) :
single V c j ⋙ F.mapHomologicalComplex _ ≅ F ⋙ single W c j :=
noncomputable def singleMapHomologicalComplex (j : ι) :
single W₁ c j ⋙ F.mapHomologicalComplex _ ≅ F ⋙ single W₂ c j :=
NatIso.ofComponents
(fun X =>
{ hom := { f := fun i => if h : i = j then eqToHom (by simp [h]) else 0 }
Expand All @@ -299,30 +310,28 @@ noncomputable def singleMapHomologicalComplex (F : V ⥤ W) [F.Additive] (c : Co
· apply (isZero_single_obj_X c j _ _ h).eq_of_tgt
#align homological_complex.single_map_homological_complex HomologicalComplex.singleMapHomologicalComplex

variable (F : V ⥤ W) [Functor.Additive F] (c) [DecidableEq ι]

@[simp]
theorem singleMapHomologicalComplex_hom_app_self (j : ι) (X : V) :
theorem singleMapHomologicalComplex_hom_app_self (j : ι) (X : W₁) :
((singleMapHomologicalComplex F c j).hom.app X).f j =
F.map (singleObjXSelf c j X).hom ≫ (singleObjXSelf c j (F.obj X)).inv := by
simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
#align homological_complex.single_map_homological_complex_hom_app_self HomologicalComplex.singleMapHomologicalComplex_hom_app_self

@[simp]
theorem singleMapHomologicalComplex_hom_app_ne {i j : ι} (h : i ≠ j) (X : V) :
theorem singleMapHomologicalComplex_hom_app_ne {i j : ι} (h : i ≠ j) (X : W₁) :
((singleMapHomologicalComplex F c j).hom.app X).f i = 0 := by
simp [singleMapHomologicalComplex, h]
#align homological_complex.single_map_homological_complex_hom_app_ne HomologicalComplex.singleMapHomologicalComplex_hom_app_ne

@[simp]
theorem singleMapHomologicalComplex_inv_app_self (j : ι) (X : V) :
theorem singleMapHomologicalComplex_inv_app_self (j : ι) (X : W₁) :
((singleMapHomologicalComplex F c j).inv.app X).f j =
(singleObjXSelf c j (F.obj X)).hom ≫ F.map (singleObjXSelf c j X).inv := by
simp [singleMapHomologicalComplex, singleObjXSelf, singleObjXIsoOfEq, eqToHom_map]
#align homological_complex.single_map_homological_complex_inv_app_self HomologicalComplex.singleMapHomologicalComplex_inv_app_self

@[simp]
theorem singleMapHomologicalComplex_inv_app_ne {i j : ι} (h : i ≠ j) (X : V) :
theorem singleMapHomologicalComplex_inv_app_ne {i j : ι} (h : i ≠ j) (X : W₁) :
((singleMapHomologicalComplex F c j).inv.app X).f i = 0 := by
simp [singleMapHomologicalComplex, h]
#align homological_complex.single_map_homological_complex_inv_app_ne HomologicalComplex.singleMapHomologicalComplex_inv_app_ne
Expand Down
Loading