work on graded modules

algebra/graded.hlean

@@ -2,7 +2,7 @@
 
 -- Author: Floris van Doorn
 
-import .left_module .direct_sum .submodule
+import .left_module .direct_sum .submodule ..heq
 
 open algebra eq left_module pointed function equiv is_equiv is_trunc prod group sigma
 
@@ -11,7 +11,7 @@ namespace left_module
 definition graded [reducible] (str : Type) (I : Type) : Type := I → str
 definition graded_module [reducible] (R : Ring) : Type → Type := graded (LeftModule R)
 
-variables {R : Ring} {I : Type} {M M₁ M₂ M₃ : graded_module R I}
+variables {R : Ring} {I : Set} {M M₁ M₂ M₃ : graded_module R I}
 
 /-
   morphisms between graded modules.
@@ -31,6 +31,7 @@ variables {R : Ring} {I : Type} {M M₁ M₂ M₃ : graded_module R I}
     but as a function taking a path as argument. Specifically, for every path
     deg f i = j
     we get a function M₁ i → M₂ j.
+  (3) Note: we do assume that I is a set. This is not strictly necessary, but it simplifies things
 -/
 
 definition graded_hom_of_deg (d : I ≃ I) (M₁ M₂ : graded_module R I) : Type :=
@@ -49,21 +50,21 @@ mk' ::  (d : I ≃ I)
 notation M₁ ` →gm ` M₂ := graded_hom M₁ M₂
 
 abbreviation deg [unfold 5] := @graded_hom.d
-postfix ` ↘`:(max+10) := graded_hom.fn' -- there is probably a better character for this? Maybe ↷?
+postfix ` ↘`:max := graded_hom.fn' -- there is probably a better character for this? Maybe ↷?
 
 definition graded_hom_fn [reducible] [unfold 5] [coercion] (f : M₁ →gm M₂) (i : I) : M₁ i →lm M₂ (deg f i) :=
 f ↘ idp
 
-definition graded_hom_fn_in [reducible] [unfold 5] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
+definition graded_hom_fn_out [reducible] [unfold 5] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
 f ↘ (to_right_inv (deg f) i)
 
-infix ` ← `:101 := graded_hom_fn_in -- todo: change notation
+infix ` ← `:101 := graded_hom_fn_out -- todo: change notation
 
 definition graded_hom.mk [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
   (fn : Πi, M₁ i →lm M₂ (d i)) : M₁ →gm M₂ :=
 graded_hom.mk' d (λi j p, homomorphism_of_eq (ap M₂ p) ∘lm fn i)
 
-definition graded_hom.mk_in [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
+definition graded_hom.mk_out [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
   (fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) : M₁ →gm M₂ :=
 graded_hom.mk' d (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
 
@@ -81,7 +82,7 @@ definition graded_hom_eq_zero {f : M₁ →gm M₂} {i j k : I} {q : deg f i = j
 have f ↘ p m = transport M₂ (q⁻¹ ⬝ p) (f ↘ q m), begin induction p, induction q, reflexivity end,
 this ⬝ ap (transport M₂ (q⁻¹ ⬝ p)) r ⬝ tr_eq_of_pathover (apd (λi, 0) (q⁻¹ ⬝ p))
 
-variables {f' : M₂ →gm M₃} {f g : M₁ →gm M₂}
+variables {f' : M₂ →gm M₃} {f g h : M₁ →gm M₂}
 
 definition graded_hom_compose [constructor] (f' : M₂ →gm M₃) (f : M₁ →gm M₂) : M₁ →gm M₃ :=
 graded_hom.mk (deg f ⬝e deg f') (λi, f' (deg f i) ∘lm f i)
@@ -121,7 +122,7 @@ definition isomorphism_of_graded_iso [constructor] (φ : M₁ ≃gm M₂) (i : I
   M₁ i ≃lm M₂ (deg φ i) :=
 isomorphism.mk (φ i) _
 
-definition isomorphism_of_graded_iso_in [constructor] (φ : M₁ ≃gm M₂) (i : I) :
+definition isomorphism_of_graded_iso_out [constructor] (φ : M₁ ≃gm M₂) (i : I) :
   M₁ ((deg φ)⁻¹ i) ≃lm M₂ i :=
 isomorphism_of_graded_iso' φ !to_right_inv
 
@@ -133,10 +134,10 @@ begin
   exact to_is_equiv (equiv_of_isomorphism (φ i)),
 end
 
-protected definition graded_iso.mk_in [constructor] (d : I ≃ I) (φ : Πi, M₁ (d⁻¹ i) ≃lm M₂ i) :
+protected definition graded_iso.mk_out [constructor] (d : I ≃ I) (φ : Πi, M₁ (d⁻¹ i) ≃lm M₂ i) :
   M₁ ≃gm M₂ :=
 begin
-  apply graded_iso.mk' (graded_hom.mk_in d φ),
+  apply graded_iso.mk' (graded_hom.mk_out d φ),
   intro i j p, esimp,
   exact @is_equiv_compose _ _ _ _ _ !is_equiv_cast _,
 end
@@ -146,7 +147,7 @@ definition graded_iso_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M
 graded_iso.mk erfl (λi, isomorphism_of_eq (p i))
 
 -- definition to_gminv [constructor] (φ : M₁ ≃gm M₂) : M₂ →gm M₁ :=
--- graded_hom.mk_in (deg φ)⁻¹ᵉ
+-- graded_hom.mk_out (deg φ)⁻¹ᵉ
 --   abstract begin
 --     intro i, apply isomorphism.to_hom, symmetry,
 --     apply isomorphism_of_graded_iso φ
@@ -160,63 +161,91 @@ variable {M}
 definition graded_iso.rfl [refl] [constructor] : M ≃gm M := graded_iso.refl M
 
 definition graded_iso.symm [symm] [constructor] (φ : M₁ ≃gm M₂) : M₂ ≃gm M₁ :=
-graded_iso.mk_in (deg φ)⁻¹ᵉ (λi, (isomorphism_of_graded_iso φ i)⁻¹ˡᵐ)
+graded_iso.mk_out (deg φ)⁻¹ᵉ (λi, (isomorphism_of_graded_iso φ i)⁻¹ˡᵐ)
 
 definition graded_iso.trans [trans] [constructor] (φ : M₁ ≃gm M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
 graded_iso.mk (deg φ ⬝e deg ψ)
   (λi, isomorphism_of_graded_iso φ i ⬝lm isomorphism_of_graded_iso ψ (deg φ i))
 
 definition graded_iso.eq_trans [trans] [constructor]
-   {M₁ M₂ : graded_module R I} {M₃ : graded_module R I} (φ : M₁ ~ M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
+   {M₁ M₂ M₃ : graded_module R I} (φ : M₁ ~ M₂) (ψ : M₂ ≃gm M₃) : M₁ ≃gm M₃ :=
 proof graded_iso.trans (graded_iso_of_eq φ) ψ qed
 
 definition graded_iso.trans_eq [trans] [constructor]
-  {M₁ : graded_module R I} {M₂ M₃ : graded_module R I} (φ : M₁ ≃gm M₂) (ψ : M₂ ~ M₃) : M₁ ≃gm M₃ :=
+  {M₁ M₂ M₃ : graded_module R I} (φ : M₁ ≃gm M₂) (ψ : M₂ ~ M₃) : M₁ ≃gm M₃ :=
 graded_iso.trans φ (graded_iso_of_eq ψ)
 
-postfix `⁻¹ᵍᵐ`:(max + 1) := graded_iso.symm
+postfix `⁻¹ᵉᵍᵐ`:(max + 1) := graded_iso.symm
-infixl ` ⬝gm `:75 := graded_iso.trans
+infixl ` ⬝egm `:75 := graded_iso.trans
-infixl ` ⬝gmp `:75 := graded_iso.trans_eq
+infixl ` ⬝egmp `:75 := graded_iso.trans_eq
-infixl ` ⬝pgm `:75 := graded_iso.eq_trans
+infixl ` ⬝epgm `:75 := graded_iso.eq_trans
 
-definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂)
+definition graded_hom_of_eq [constructor] {M₁ M₂ : graded_module R I} (p : M₁ ~ M₂) : M₁ →gm M₂ :=
-  : M₁ →gm M₂ :=
+proof graded_iso_of_eq p qed
-graded_iso_of_eq p
 
-structure graded_homotopy (f g : M₁ →gm M₂) : Type :=
+definition graded_homotopy (f g : M₁ →gm M₂) : Type :=
-mk' :: (hd : deg f ~ deg g)
+Π⦃i j k⦄ (p : deg f i = j) (q : deg g i = k) (m : M₁ i), f ↘ p m ==[λi, M₂ i] g ↘ q m
-       (hfn : Π⦃i j : I⦄ (pf : deg f i = j) (pg : deg g i = j) (r : hd i ⬝ pg = pf), f ↘ pf ~ g ↘ pg)
+-- mk' :: (hd : deg f ~ deg g)
+--        (hfn : Π⦃i j : I⦄ (pf : deg f i = j) (pg : deg g i = j), f ↘ pf ~ g ↘ pg)
 
 infix ` ~gm `:50 := graded_homotopy
 
-definition graded_homotopy.mk (hd : deg f ~ deg g) (hfn : Πi m, f i m =[hd i] g i m) : f ~gm g :=
+-- definition graded_homotopy.mk2 (hd : deg f ~ deg g) (hfn : Πi m, f i m =[hd i] g i m) : f ~gm g :=
-graded_homotopy.mk' hd
+-- graded_homotopy.mk' hd
-  begin
+--   begin
-    intro i j pf pg r m, induction r, induction pg, esimp,
+--     intro i j pf pg m, induction (is_set.elim (hd i ⬝ pg) pf), induction pg, esimp,
-    exact graded_hom_eq_transport f (hd i) m ⬝ tr_eq_of_pathover (hfn i m),
+--     exact graded_hom_eq_transport f (hd i) m ⬝ tr_eq_of_pathover (hfn i m),
-  end
+--   end
 
-definition graded_homotopy_of_deg (d : I ≃ I) (f g : graded_hom_of_deg d M₁ M₂) : Type :=
+definition graded_homotopy.mk (h : Πi m, f i m ==[λi, M₂ i] g i m) : f ~gm g :=
-Π⦃i j : I⦄ (p : d i = j), f p ~ g p
-
-notation f ` ~[`:50 d:0 `] `:0 g:50 := graded_homotopy_of_deg d f g
-
-variables {d : I ≃ I} {f₁ f₂ : graded_hom_of_deg d M₁ M₂}
--- definition graded_homotopy_elim' [unfold 8] := @graded_homotopy_of_deg.elim'
--- definition graded_homotopy_elim [reducible] [unfold 8] [coercion] (h : f₁ ~[d] f₂) (i : I) :
---   f₁ (refl i) ~ f₂ (refl i) :=
--- graded_homotopy_elim' _ _
-
--- definition graded_homotopy_elim_in [reducible] [unfold 8] (f : M₁ →gm M₂) (i : I) : M₁ ((deg f)⁻¹ i) →lm M₂ i :=
--- f ↘ (to_right_inv (deg f) i)
-
-definition graded_homotopy_of_deg.mk [constructor] (h : Πi, f₁ (idpath (d i)) ~ f₂ (idpath (d i))) :
-  f₁ ~[d] f₂ :=
 begin
-  intro i j p, induction p, exact h i
+  intros i j k p q m, induction q, induction p, exact h i m
 end
 
--- definition graded_homotopy.mk_in [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
+-- definition graded_hom_compose_out {d₁ d₂ : I ≃ I} (f₂ : Πi, M₂ i →lm M₃ (d₂ i))
+--   (f₁ : Πi, M₁ (d₁⁻¹ i) →lm M₂ i) : graded_hom.mk d₂ f₂ ∘gm graded_hom.mk_out d₁ f₁ ~gm
+--   graded_hom.mk_out_in d₁⁻¹ᵉ d₂ _ :=
+-- _
+
+definition graded_hom_out_in_compose_out {d₁ d₂ d₃ : I ≃ I} (f₂ : Πi, M₂ (d₂ i) →lm M₃ (d₃ i))
+  (f₁ : Πi, M₁ (d₁⁻¹ i) →lm M₂ i) : graded_hom.mk_out_in d₂ d₃ f₂ ∘gm graded_hom.mk_out d₁ f₁ ~gm
+  graded_hom.mk_out_in (d₂ ⬝e d₁⁻¹ᵉ) d₃ (λi, f₂ i ∘lm (f₁ (d₂ i))) :=
+begin
+  apply graded_homotopy.mk, intro i m, exact sorry
+end
+
+definition graded_hom_out_in_rfl {d₁ d₂ : I ≃ I} (f : Πi, M₁ i →lm M₂ (d₂ i))
+  (p : Πi, d₁ i = i) :
+  graded_hom.mk_out_in d₁ d₂ (λi, sorry) ~gm graded_hom.mk d₂ f :=
+begin
+  apply graded_homotopy.mk, intro i m, exact sorry
+end
+
+definition graded_homotopy.trans (h₁ : f ~gm g) (h₂ : g ~gm h) : f ~gm h :=
+begin
+  exact sorry
+end
+
+-- postfix `⁻¹ᵍᵐ`:(max + 1) := graded_iso.symm
+infixl ` ⬝gm `:75 := graded_homotopy.trans
+-- infixl ` ⬝gmp `:75 := graded_iso.trans_eq
+-- infixl ` ⬝pgm `:75 := graded_iso.eq_trans
+
+
+-- definition graded_homotopy_of_deg (d : I ≃ I) (f g : graded_hom_of_deg d M₁ M₂) : Type :=
+-- Π⦃i j : I⦄ (p : d i = j), f p ~ g p
+
+-- notation f ` ~[`:50 d:0 `] `:0 g:50 := graded_homotopy_of_deg d f g
+
+-- variables {d : I ≃ I} {f₁ f₂ : graded_hom_of_deg d M₁ M₂}
+
+-- definition graded_homotopy_of_deg.mk [constructor] (h : Πi, f₁ (idpath (d i)) ~ f₂ (idpath (d i))) :
+--   f₁ ~[d] f₂ :=
+-- begin
+--   intro i j p, induction p, exact h i
+-- end
+
+-- definition graded_homotopy.mk_out [constructor] {M₁ M₂ : graded_module R I} (d : I ≃ I)
 --   (fn : Πi, M₁ (d⁻¹ i) →lm M₂ i) : M₁ →gm M₂ :=
 -- graded_hom.mk' d (λi j p, fn j ∘lm homomorphism_of_eq (ap M₁ (eq_inv_of_eq p)))
 -- definition is_gconstant (f : M₁ →gm M₂) : Type :=
@@ -294,10 +323,10 @@ definition graded_hom_lift [constructor] {S : Πi, submodule_rel (M₂ i)} (φ :
 graded_hom.mk (deg φ) (λi, hom_lift (φ i) (h i))
 
 definition graded_image (f : M₁ →gm M₂) : graded_module R I :=
-λi, image_module (f ↘ (to_right_inv (deg f) i))
+λi, image_module (f ← i)
 
 definition graded_image_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image f :=
-graded_hom.mk_in (deg f) (λi, image_lift (f ↘ (to_right_inv (deg f) i)))
+graded_hom.mk_out (deg f) (λi, image_lift (f ← i))
 
 definition graded_image_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
   (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
@@ -311,6 +340,77 @@ begin
   exact graded_hom_eq_zero m p
 end
 
+definition graded_image' (f : M₁ →gm M₂) : graded_module R I :=
+λi, image_module (f i)
+
+definition graded_image'_lift [constructor] (f : M₁ →gm M₂) : M₁ →gm graded_image' f :=
+graded_hom.mk erfl (λi, image_lift (f i))
+
+definition graded_image'_elim [constructor] {f : M₁ →gm M₂} (g : M₁ →gm M₃)
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+  graded_image' f →gm M₃ :=
+begin
+  apply graded_hom.mk (deg g),
+  intro i,
+  apply image_elim (g i),
+  intro m p, exact h p
+end
+
+theorem graded_image'_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+  graded_image'_elim g h ∘gm graded_image'_lift f ~gm g :=
+begin
+  apply graded_homotopy.mk,
+  intro i m, reflexivity
+end
+
+theorem graded_image_elim_compute {f : M₁ →gm M₂} {g : M₁ →gm M₃}
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+  graded_image_elim g h ∘gm graded_image_lift f ~gm g :=
+begin
+  refine _ ⬝gm graded_image'_elim_compute h,
+  esimp, exact sorry
+  -- refine graded_hom_out_in_compose_out _ _ ⬝gm _, exact sorry
+  -- -- apply graded_homotopy.mk,
+  -- -- intro i m,
+end
+variables {α β : I ≃ I}
+definition gen_image (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : graded_module R I :=
+λi, image_module (f ↘ (p i))
+
+definition gen_image_lift [constructor] (f : M₁ →gm M₂) (p : Πi, deg f (α i) = β i) : M₁ →gm gen_image f p :=
+graded_hom.mk_out α⁻¹ᵉ (λi, image_lift (f ↘ (p i)))
+
+definition gen_image_elim [constructor] {f : M₁ →gm M₂} (p : Πi, deg f (α i) = β i) (g : M₁ →gm M₃)
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+  gen_image f p →gm M₃ :=
+begin
+  apply graded_hom.mk_out_in α⁻¹ᵉ (deg g),
+  intro i,
+  apply image_elim (g ↘ (ap (deg g) (to_right_inv α i))),
+  intro m p,
+  refine graded_hom_eq_zero m (h _),
+  exact graded_hom_eq_zero m p
+end
+
+theorem gen_image_elim_compute {f : M₁ →gm M₂} {p : deg f ∘ α ~ β} {g : M₁ →gm M₃}
+  (h : Π⦃i m⦄, f i m = 0 → g i m = 0) :
+  gen_image_elim p g h ∘gm gen_image_lift f p ~gm g :=
+begin
+  -- induction β with β βe, esimp at *, induction p using homotopy.rec_on_idp,
+  assert q : β ⬝e (deg f)⁻¹ᵉ = α,
+  { apply equiv_eq, intro i, apply inv_eq_of_eq, exact (p i)⁻¹ },
+  induction q,
+  -- unfold [gen_image_elim, gen_image_lift],
+
+  -- induction (is_prop.elim (λi, to_right_inv (deg f) (β i)) p),
+  -- apply graded_homotopy.mk,
+  -- intro i m, reflexivity
+end
+
+definition graded_kernel (f : M₁ →gm M₂) : graded_module R I :=
+λi, kernel_module (f i)
+
 definition graded_quotient (S : Πi, submodule_rel (M i)) : graded_module R I :=
 λi, quotient_module (S i)
 
@@ -321,6 +421,10 @@ graded_hom.mk erfl (λi, quotient_map (S i))
 definition graded_homology (g : M₂ →gm M₃) (f : M₁ →gm M₂) : graded_module R I :=
 λi, homology (g i) (f ↘ (to_right_inv (deg f) i))
 
+definition graded_homology_intro [constructor] (g : M₂ →gm M₃) (f : M₁ →gm M₂) :
+  graded_kernel g →gm graded_homology g f :=
+graded_quotient_map _
+
 definition graded_homology_elim {g : M₂ →gm M₃} {f : M₁ →gm M₂} (h : M₂ →gm M)
   (H : compose_constant h f) : graded_homology g f →gm M :=
 graded_hom.mk (deg h) (λi, homology_elim (h i) (H _ _))
@@ -331,6 +435,11 @@ graded_hom.mk (deg h) (λi, homology_elim (h i) (H _ _))
 definition is_exact_gmod (f : M₁ →gm M₂) (f' : M₂ →gm M₃) : Type :=
 Π⦃i j k⦄ (p : deg f i = j) (q : deg f' j = k), is_exact_mod (f ↘ p) (f' ↘ q)
 
+definition is_exact_gmod.mk {f : M₁ →gm M₂} {f' : M₂ →gm M₃}
+  (h₁ : Π⦃i⦄ (m : M₁ i), f' (deg f i) (f i m) = 0)
+  (h₂ : Π⦃i⦄ (m : M₂ (deg f i)), f' (deg f i) m = 0 → image (f i) m) : is_exact_gmod f f' :=
+begin intro i j k p q; induction p; induction q; split, apply h₁, apply h₂ end
+
 definition gmod_im_in_ker (h : is_exact_gmod f f') : compose_constant f' f :=
 λi j k p q, is_exact.im_in_ker (h p q)
 
@@ -345,16 +454,19 @@ end left_module
 namespace left_module
   namespace derived_couple
   section
-  parameters {R : Ring} {I : Type} {D E : graded_module R I} {i : D →gm D} {j : D →gm E} {k : E →gm D}
+  parameters {R : Ring} {I : Set} {D E : graded_module R I}
-            (exact_ij : is_exact_gmod i j)
+    {i : D →gm D} {j : D →gm E} {k : E →gm D}
-            (exact_jk : is_exact_gmod j k)
+    (exact_ij : is_exact_gmod i j) (exact_jk : is_exact_gmod j k) (exact_ki : is_exact_gmod k i)
-            (exact_ki : is_exact_gmod k i)
 
   definition d : E →gm E := j ∘gm k
   definition D' : graded_module R I := graded_image i
   definition E' : graded_module R I := graded_homology d d
-  definition i' : D' →gm D' := graded_image_lift i ∘gm graded_submodule_incl _
+
-  include exact_jk exact_ki
+  include exact_jk exact_ki exact_ij
+
+  definition i' : D' →gm D' :=
+  graded_image_lift i ∘gm graded_submodule_incl _
+  -- degree i + 0
 
   theorem j_lemma1 ⦃x : I⦄ (m : D x) : d ((deg j) x) (j x m) = 0 :=
   begin
@@ -380,7 +492,8 @@ namespace left_module
       intros,
       refine this _ _ _ p,
       exact to_right_inv (deg k) _ ⬝ to_left_inv (deg j) x,
-      rewrite [ap_con, -adj],
+      apply is_set.elim
+      -- rewrite [ap_con, -adj],
     end,
     intros,
     rewrite [graded_hom_compose_fn],
@@ -388,7 +501,8 @@ namespace left_module
   end
 
   definition j' : D' →gm E' :=
-  graded_image_elim (!graded_quotient_map ∘gm graded_hom_lift j j_lemma1) j_lemma2
+  graded_image_elim (graded_homology_intro d d ∘gm graded_hom_lift j j_lemma1) j_lemma2
+  -- degree -(deg i) + deg j
 
   definition k' : E' →gm D' :=
   graded_homology_elim (graded_image_lift i ∘gm k)
@@ -398,9 +512,46 @@ namespace left_module
       refine ap (graded_hom_fn (graded_image_lift i) (deg k (deg d x))) _ ⬝ !to_respect_zero,
       exact compose_constant.elim (gmod_im_in_ker exact_jk) (deg k x) (k x m)
     end end
+  -- degree deg i + deg k
+
+  theorem is_exact_i'j' : is_exact_gmod i' j' :=
+  begin
+    apply is_exact_gmod.mk,
+    { intro x, refine total_image.rec _, intro m,
+      exact calc
+        j' (deg i' x) (i' x ⟨(i ← x) m, image.mk m idp⟩)
+            = j' (deg i' x) (graded_image_lift i x ((i ← x) m)) : idp
+        ... = graded_homology_intro d d (deg j ((deg i)⁻¹ᵉ (deg i x)))
+                (graded_hom_lift j j_lemma1 ((deg i)⁻¹ᵉ (deg i x))
+                (i ↘ (!to_right_inv ⬝ !to_left_inv⁻¹) m)) : _
+        ... = graded_homology_intro d d (deg j ((deg i)⁻¹ᵉ (deg i x)))
+                (graded_hom_lift j j_lemma1 ((deg i)⁻¹ᵉ (deg i x))
+                (i ↘ (!to_right_inv ⬝ !to_left_inv⁻¹) m)) : _
+        ... = 0 : _
+      },
+    { exact sorry }
+  end
+
+  theorem is_exact_j'k' : is_exact_gmod j' k' :=
+  begin
+    apply is_exact_gmod.mk,
+    { },
+    { exact sorry }
+  end
+
+  theorem is_exact_k'i' : is_exact_gmod k' i' :=
+  begin
+    apply is_exact_gmod.mk,
+    { intro x m, },
+    { exact sorry }
+  end
 
   end
 
+-- homomorphism_fn (graded_hom_fn j' (to_fun (deg i') i))
+--       (homomorphism_fn (graded_hom_fn i' i) m) = 0
+
+
   end derived_couple
 
 

algebra/left_module.hlean

@@ -288,11 +288,12 @@ end
   definition to_respect_zero (φ : M₁ →lm M₂) : φ 0 = 0 :=
   respect_zero φ
 
-  definition homomorphism_compose [constructor] (f' : M₂ →lm M₃) (f : M₁ →lm M₂) : M₁ →lm M₃ :=
+  definition homomorphism_compose [reducible] [constructor] (f' : M₂ →lm M₃) (f : M₁ →lm M₂) :
+    M₁ →lm M₃ :=
   homomorphism.mk (f' ∘ f) !is_module_hom_comp
 
   variable (M)
-  definition homomorphism_id [constructor] [refl] : M →lm M :=
+  definition homomorphism_id [reducible] [constructor] [refl] : M →lm M :=
   homomorphism.mk (@id M) !is_module_hom_id
   variable {M}
 

algebra/submodule.hlean

@@ -9,7 +9,7 @@ attribute normal_subgroup_rel.to_subgroup_rel [constructor]
 
 namespace left_module
 /- submodules -/
-variables {R : Ring} {M M₁ M₂ : LeftModule R} {m m₁ m₂ : M}
+variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M}
 
 structure submodule_rel (M : LeftModule R) : Type :=
   (S : M → Prop)
@@ -91,6 +91,16 @@ lm_homomorphism_of_group_homomorphism (hom_lift (group_homomorphism_of_lm_homomo
     intro r g, exact subtype_eq (to_respect_smul φ r g)
   end
 
+definition hom_lift_compose {K : submodule_rel M₃}
+  (φ : M₂ →lm M₃) (h : Π (m : M₂), K (φ m)) (ψ : M₁ →lm M₂) :
+  hom_lift φ h ∘lm ψ ~ hom_lift (φ ∘lm ψ) proof (λm, h (ψ m)) qed :=
+by reflexivity
+
+definition hom_lift_homotopy {K : submodule_rel M₂} {φ : M₁ →lm M₂}
+  {h : Π (m : M₁), K (φ m)} {φ' : M₁ →lm M₂}
+  {h' : Π (m : M₁), K (φ' m)} (p : φ ~ φ') : hom_lift φ h ~ hom_lift φ' h' :=
+λg, subtype_eq (p g)
+
 definition incl_smul (S : submodule_rel M) (r : R) (m : M) (h : S m) :
   r • ⟨m, h⟩ = ⟨_, contains_smul S r h⟩ :> submodule S :=
 by reflexivity
@@ -104,12 +114,7 @@ submodule_rel.mk (λm, S₁ (submodule_incl S₂ m))
     intro m r p, induction m with m hm, exact contains_smul S₁ r p
   end
 
-end left_module
-
-namespace left_module
-
 /- quotient modules -/
-variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R} {m m₁ m₂ : M} {S : submodule_rel M}
 
 definition quotient_module' (S : submodule_rel M) : AddAbGroup :=
 quotient_ab_group (subgroup_rel_of_submodule_rel S)
@@ -188,17 +193,26 @@ definition image_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := s
 --   (image_module φ : AddAbGroup) = image (group_homomorphism_of_lm_homomorphism φ) :=
 -- by reflexivity
 
-variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂}
+definition image_lift [constructor] (φ : M₁ →lm M₂) : M₁ →lm image_module φ :=
-definition image_elim [constructor] (ψ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → ψ g = 0) :
+hom_lift φ (λm, image.mk m idp)
+
+variables {ψ : M₂ →lm M₃} {φ : M₁ →lm M₂} {θ : M₁ →lm M₃}
+definition image_elim [constructor] (θ : M₁ →lm M₃) (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
   image_module φ →lm M₃ :=
 begin
-  refine homomorphism.mk (image_elim (group_homomorphism_of_lm_homomorphism ψ) h) _,
+  refine homomorphism.mk (image_elim (group_homomorphism_of_lm_homomorphism θ) h) _,
   split,
   { apply homomorphism.addstruct },
   { intro r, refine @total_image.rec _ _ _ _ (λx, !is_trunc_eq) _, intro g,
     apply to_respect_smul }
 end
 
+definition image_elim_compute (h : Π⦃g⦄, φ g = 0 → θ g = 0) :
+  image_elim θ h ∘lm image_lift φ ~ θ :=
+begin
+  reflexivity
+end
+
 definition has_scalar_kernel (φ : M₁ →lm M₂) ⦃m : M₁⦄ (r : R)
   (p : φ m = 0) : φ (r • m) = 0 :=
 begin
@@ -212,9 +226,6 @@ submodule_rel_of_subgroup_rel
 
 definition kernel_module [constructor] (φ : M₁ →lm M₂) : LeftModule R := submodule (kernel_rel φ)
 
-definition image_lift [constructor] (φ : M₁ →lm M₂) : M₁ →lm image_module φ :=
-hom_lift φ (λm, image.mk m idp)
-
 definition homology (ψ : M₂ →lm M₃) (φ : M₁ →lm M₂) : LeftModule R :=
 @quotient_module R (submodule (kernel_rel ψ)) (submodule_rel_of_submodule _ (image_rel φ))
 

known_bugs.txt

@@ -3,6 +3,7 @@
 instead of
 `have g : G, from _,`
 
+- coercions are still displayed by the pretty printer
 
 - When using the calc mode for homotopies, you have to give the proofs using a tactic (e.g. `by exact foo` instead of `foo`)
 
@@ -26,3 +27,5 @@ equiv.MK f
          abstract (* long proof *) end
          abstract (* long proof *) end
 ```
+
+- unfold [foo] also does various (sometimes unwanted) reductions (as if you called esimp)