feat(algebra/homology): chain complexes

src/algebra/homology/chain_complex.lean

@@ -0,0 +1,104 @@
+import category_theory.graded_object
+import category_theory.differential_object
+
+universes v u
+
+open category_theory
+open category_theory.limits
+
+section
+variables (V : Type u) [𝒱 : category.{v} V]
+include 𝒱
+
+variables [has_zero_morphisms.{v} V]
+
+/--
+A chain complex in `V` is "just" a differential `ℤ`-graded object in `V`.
+-/
+-- Actually, because I chose the "shift" to correspond to the +1 direction,
+-- this is what would usually be called a cochain complex.
+-- We should definitely bikeshed this. :-)
+@[nolint has_inhabited_instance]
+def chain_complex : Type (max v u) :=
+differential_object.{v} (graded_object ℤ V)
+
+-- The chain groups of a chain complex `C` are accessed as `C.X i`,
+-- and the differentials as `C.d i : C.X i ⟶ C.X (i+1)`.
+example (C : chain_complex V) : C.X 5 ⟶ C.X 6 := C.d 5
+
+variables {V}
+/--
+A convenience lemma for morphisms of differential graded objects,
+picking out one component of the commutation relation.
+-/
+-- Could this be a simp lemma? Which way?
+lemma category_theory.differential_object.hom.comm_at {X Y : differential_object.{v} (graded_object ℤ V)}
+  (f : X ⟶ Y) (i : ℤ) : f.f i ≫ Y.d i = X.d i ≫ f.f (i+1) := congr_fun f.comm i
+end
+
+namespace chain_complex
+variables {V : Type u} [𝒱 : category.{v} V]
+include 𝒱
+
+variables [has_zero_morphisms.{v} V]
+
+@[simp]
+lemma d_squared (C : chain_complex.{v} V) (i : ℤ) :
+  C.d i ≫ C.d (i+1) = 0 :=
+congr_fun (C.d_squared) i
+
+-- FIXME why doesn't this work `by simp`?
+example (C : chain_complex V) : C.d 5 ≫ C.d 6 = 0 := C.d_squared 5
+
+variables (V)
+
+instance category_of_chain_complexes : category.{v} (chain_complex V) :=
+by { dsimp [chain_complex], apply_instance }.
+
+-- The components of a chain map `f : C ⟶ D` are accessed as `f.f i`.
+example {C D : chain_complex V} (f : C ⟶ D) : C.X 5 ⟶ D.X 5 := f.f 5
+example {C D : chain_complex V} (f : C ⟶ D) : f.f ≫ D.d = C.d ≫ f.f[[1]] := f.comm
+example {C D : chain_complex V} (f : C ⟶ D) : f.f 5 ≫ D.d 5 = C.d 5 ≫ f.f 6 := congr_fun f.comm 5
+
+/-- The forgetful functor from chain complexes to graded objects, forgetting the differential. -/
+def forget : (chain_complex V) ⥤ (graded_object ℤ V) :=
+differential_object.forget _
+
+instance forget_faithful : faithful (forget V) :=
+differential_object.forget_faithful _
+
+instance has_zero_morphisms : has_zero_morphisms.{v} (chain_complex V) :=
+by { dsimp [chain_complex], apply_instance }.
+
+variables [has_zero_object.{v} V]
+
+instance has_zero_object : has_zero_object.{v} (chain_complex V) :=
+by { dsimp [chain_complex], apply_instance, }
+
+end chain_complex
+
+namespace chain_complex
+variables
+  {V : Type (u+1)} [𝒱 : concrete_category V] [has_zero_morphisms.{u} V] [has_coproducts.{u} V]
+include 𝒱
+
+instance : concrete_category (chain_complex.{u} V) :=
+differential_object.concrete_category_of_differential_objects (graded_object ℤ V)
+
+instance : has_forget₂ (chain_complex.{u} V) (graded_object ℤ V) :=
+by { dsimp [chain_complex], apply_instance }
+
+end chain_complex
+
+-- TODO when V is enriched in W, what do we need to ensure
+-- `chain_complex V` is also enriched in W?
+
+-- TODO `chain_complex V` is a module category for `V` when `V` is monoidal
+
+-- TODO When V is enriched in AddCommGroup, and has coproducts(?),
+-- we can collapse a double complex to obtain a complex.
+-- (Do we need boundedness assumptions)
+
+-- TODO when V is monoidal, enriched in `AddCommGroup`,
+-- and has coproducts(?) then
+-- `chain_complex V` is monoidal too.

src/algebra/homology/homology.lean

@@ -0,0 +1,93 @@
+import algebra.homology.chain_complex
+import category_theory.limits.shapes.images
+import category_theory.limits.shapes.kernels
+
+universes v u
+
+namespace chain_complex
+
+open category_theory
+open category_theory.limits
+
+variables {V : Type u} [𝒱 : category.{v} V] [has_zero_morphisms.{v} V]
+include 𝒱
+
+section
+variable [has_kernels.{v} V]
+/-- The map induceed by a chain map between the kernels of the differentials. -/
+def induced_map_on_cycles {C C' : chain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+  kernel (C.d i) ⟶ kernel (C'.d i) :=
+kernel.lift _ (kernel.ι _ ≫ f.f i)
+begin
+  rw [category.assoc, f.comm_at, ←category.assoc, kernel.condition, has_zero_morphisms.zero_comp],
+end
+end
+
+/-!
+At this point we assume that we have all images, and all equalizers.
+We need to assume all equalizers, not just kernels, so that
+`factor_thru_image` is an epimorphism.
+-/
+variables [has_images.{v} V] [has_equalizers.{v} V]
+
+/-- The connecting morphism from the image of `d i` to the kernel of `d (i+1)`. -/
+def image_to_kernel_map (C : chain_complex.{v} V) (i : ℤ) :
+  image (C.d i) ⟶ kernel (C.d (i+1)) :=
+kernel.lift _ (image.ι (C.d i))
+begin
+  apply @epi.left_cancellation _ _ _ _ (factor_thru_image (C.d i)) _ _ _ _ _,
+  simp,
+  refl,
+end
+
+-- PROJECT:
+-- At this level of generality, it's just not true that a chain map
+-- induces maps on boundaries
+--
+-- Let's add these later, with appropriate (but hopefully fairly minimal)
+-- assumptions: perhaps that the category is regular?
+-- I think in that case we can compute `image` as the regular coimage,
+-- i.e. the coequalizer of the kernel pair,
+-- and that image has the appropriate mapping property.
+
+-- def induced_map_on_boundaries {C C' : chain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+--   image (C.d i) ⟶ image (C'.d i) :=
+-- sorry
+
+-- I'm not certain what the minimal assumptions required to prove the following
+-- lemma are:
+
+-- lemma induced_maps_commute {C C' : chain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+-- image_to_kernel_map C i ≫ induced_map_on_cycles f (i+1) =
+--   induced_map_on_boundaries f i ≫ image_to_kernel_map C' i :=
+-- sorry
+
+variables [has_cokernels.{v} V]
+
+/-- The `i`-th homology group of the chain complex `C`. -/
+def homology_group (C : chain_complex.{v} V) (i : ℤ) : V :=
+cokernel (image_to_kernel_map C i)
+
+-- PROJECT:
+
+-- As noted above, as we don't get induced maps on boundaries with this generality,
+-- we can't assemble the homology groups into a functor. Hopefully, however,
+-- the commented out code below will work
+-- (with whatever added assumptions are needed above.)
+
+-- def induced_map_on_homology {C C' : chain_complex.{v} V} (f : C ⟶ C') (i : ℤ) :
+--   C.homology_group i ⟶ C'.homology_group i :=
+-- cokernel.desc _ (induced_map_on_cycles f (i+1) ≫ cokernel.π _)
+-- begin
+--   rw [←category.assoc, induced_maps_commute, category.assoc, cokernel.condition],
+--   erw [has_zero_morphisms.comp_zero],
+-- end
+
+-- /-- The homology functor from chain complexes to `ℤ` graded objects in `V`. -/
+-- def homology : chain_complex.{v} V ⥤ graded_object ℤ V :=
+-- { obj := λ C i, homology_group C i,
+--   map := λ C C' f i, induced_map_on_homology f i,
+--   map_id' := sorry,
+--   map_comp' := sorry, }
+
+end chain_complex

src/category_theory/differential_object.lean

@@ -0,0 +1,124 @@
+import category_theory.limits.shapes.zero
+import category_theory.shift
+
+open category_theory.limits
+
+universes v u
+
+namespace category_theory
+
+variables (C : Type u) [𝒞 : category.{v} C]
+include 𝒞
+
+variables [has_zero_morphisms.{v} C] [has_shift.{v} C]
+
+/--
+A differential object in a category with zero morphisms and a shift is
+an object `X` equipped with
+a morphism `d : X ⟶ X[1]`, so `d^2 = 0`.
+-/
+@[nolint has_inhabited_instance]
+structure differential_object :=
+(X : C)
+(d : X ⟶ X[1])
+(d_squared' : d ≫ d[[1]] = 0 . obviously)
+
+restate_axiom differential_object.d_squared'
+attribute [simp] differential_object.d_squared
+
+variables {C}
+
+namespace differential_object
+
+/--
+A morphism of differential objects is a morphism commuting with the differentials.
+-/
+@[ext, nolint has_inhabited_instance]
+structure hom (X Y : differential_object.{v} C) :=
+(f : X.X ⟶ Y.X)
+(comm' : f ≫ Y.d = X.d ≫ f[[1]] . obviously)
+
+restate_axiom hom.comm'
+
+namespace hom
+
+/-- The identity morphism of a differential object. -/
+@[simps]
+def id (X : differential_object.{v} C) : hom X X :=
+{ f := 𝟙 X.X }
+
+/-- The composition of morphisms of differential objects. -/
+@[simps]
+def comp {X Y Z : differential_object.{v} C} (f : hom X Y) (g : hom Y Z) : hom X Z :=
+{ f := f.f ≫ g.f,
+  comm' := by rw [category.assoc, g.comm, ←category.assoc, f.comm, category.assoc, functor.map_comp], }
+
+end hom
+
+instance category_of_differential_objects : category.{v} (differential_object.{v} C) :=
+{ hom := hom,
+  id := hom.id,
+  comp := λ X Y Z f g, hom.comp f g, }
+
+@[simp]
+lemma id_f (X : differential_object.{v} C) : ((𝟙 X) : hom X X).f = 𝟙 (X.X) := rfl
+
+@[simp]
+lemma comp_f {X Y Z : differential_object.{v} C} (f : X ⟶ Y) (g : Y ⟶ Z) :
+  (f ≫ g).f = f.f ≫ g.f :=
+rfl
+
+variables (C)
+
+/-- The forgetful functor taking a differential object to its underlying object. -/
+def forget : (differential_object.{v} C) ⥤ C :=
+{ obj := λ X, X.X,
+  map := λ X Y f, f.f, }
+
+instance forget_faithful : faithful (forget C) :=
+{ }
+
+instance has_zero_morphisms : has_zero_morphisms.{v} (differential_object.{v} C) :=
+{ has_zero := λ X Y,
+  ⟨{ f := 0, }⟩}
+
+end differential_object
+
+end category_theory
+
+namespace category_theory
+
+namespace differential_object
+
+variables (C : Type u) [𝒞 : category.{v} C]
+include 𝒞
+
+variables [has_zero_object.{v} C] [has_zero_morphisms.{v} C] [has_shift.{v} C]
+
+local attribute [instance] has_zero_object.has_zero
+
+instance has_zero_object : has_zero_object.{v} (differential_object.{v} C) :=
+{ zero :=
+  { X := (0 : C),
+    d := 0, },
+  unique_to := λ X, ⟨⟨{ f := 0 }⟩, λ f, (by ext)⟩,
+  unique_from := λ X, ⟨⟨{ f := 0 }⟩, λ f, (by ext)⟩, }
+
+end differential_object
+
+namespace differential_object
+
+variables (C : Type (u+1))
+  [𝒞 : concrete_category C] [has_zero_morphisms.{u} C] [has_shift.{u} C]
+include 𝒞
+
+instance concrete_category_of_differential_objects :
+  concrete_category (differential_object.{u} C) :=
+{ forget := forget C ⋙ category_theory.forget C }
+
+instance : has_forget₂ (differential_object.{u} C) C :=
+{ forget₂ := forget C }
+
+end differential_object
+
+end category_theory

src/category_theory/epi_mono.lean

@@ -60,8 +60,8 @@ such that `f ≫ retraction f = 𝟙 X`.
 
 Every split monomorphism is a monomorphism.
 -/
--- TODO:
--- Every split monomorphism is also a regular monomorphism,
+-- TODO:	
+-- Every split monomorphism is also a regular monomorphism,	
 -- and this should be proved when they are introduced.
 class split_mono {X Y : C} (f : X ⟶ Y) :=
 (retraction : Y ⟶ X)