[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
L M N K : ModuleCat R
f : L ⟶ M
g : M ⟶ N
w✝ : f ≫ g = 0
h k : _root_.homology f g w✝ ⟶ K
w :
  ∀ (x : { x // x ∈ LinearMap.ker g }),
    ↑h (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x)) =
      ↑k (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x))
⊢ h = k
[PROOFSTEP]
refine'
  cokernel_funext fun n =>
    _
      -- porting note: as `equiv_rw` was not ported, it was replaced by `Equiv.surjective`
        -- Gosh it would be nice if `equiv_rw` could directly use an isomorphism, or an enriched `≃`.
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
L M N K : ModuleCat R
f : L ⟶ M
g : M ⟶ N
w✝ : f ≫ g = 0
h k : _root_.homology f g w✝ ⟶ K
w :
  ∀ (x : { x // x ∈ LinearMap.ker g }),
    ↑h (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x)) =
      ↑k (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x))
n : (CategoryTheory.forget (ModuleCat R)).obj (Subobject.underlying.obj (kernelSubobject g))
⊢ ↑h (↑(cokernel.π (imageToKernel f g w✝)) n) = ↑k (↑(cokernel.π (imageToKernel f g w✝)) n)
[PROOFSTEP]
obtain ⟨n, rfl⟩ := (kernelSubobjectIso g ≪≫ ModuleCat.kernelIsoKer g).toLinearEquiv.toEquiv.symm.surjective n
[GOAL]
case intro
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
L M N K : ModuleCat R
f : L ⟶ M
g : M ⟶ N
w✝ : f ≫ g = 0
h k : _root_.homology f g w✝ ⟶ K
w :
  ∀ (x : { x // x ∈ LinearMap.ker g }),
    ↑h (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x)) =
      ↑k (↑(cokernel.π (imageToKernel f g w✝)) (↑toKernelSubobject x))
n : ↑(of R { x // x ∈ LinearMap.ker g })
⊢ ↑h
      (↑(cokernel.π (imageToKernel f g w✝))
        (↑(LinearEquiv.toEquiv (Iso.toLinearEquiv (kernelSubobjectIso g ≪≫ kernelIsoKer g))).symm n)) =
    ↑k
      (↑(cokernel.π (imageToKernel f g w✝))
        (↑(LinearEquiv.toEquiv (Iso.toLinearEquiv (kernelSubobjectIso g ≪≫ kernelIsoKer g))).symm n))
[PROOFSTEP]
exact w n
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C✝ D C : HomologicalComplex (ModuleCat R) c
i : ι
x y : ↑(Subobject.underlying.obj (cycles C i))
w : ↑(Subobject.arrow (cycles C i)) x = ↑(Subobject.arrow (cycles C i)) y
⊢ x = y
[PROOFSTEP]
apply_fun (C.cycles i).arrow using (ModuleCat.mono_iff_injective _).mp (cycles C i).arrow_mono
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C✝ D C : HomologicalComplex (ModuleCat R) c
i : ι
x y : ↑(Subobject.underlying.obj (cycles C i))
w : ↑(Subobject.arrow (cycles C i)) x = ↑(Subobject.arrow (cycles C i)) y
⊢ ↑(Subobject.arrow (cycles C i)) x = ↑(Subobject.arrow (cycles C i)) y
[PROOFSTEP]
exact w
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f : C ⟶ D
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Hom.f f i) ↑x ∈ LinearMap.ker (dFrom D i)
[PROOFSTEP]
rw [LinearMap.mem_ker, Hom.comm_from_apply, x.2, map_zero]
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f : C ⟶ D
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(cyclesMap f i) (toCycles x) =
    toCycles { val := ↑(Hom.f f i) ↑x, property := (_ : ↑(Hom.f f i) ↑x ∈ LinearMap.ker (dFrom D i)) }
[PROOFSTEP]
ext
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f : C ⟶ D
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Subobject.arrow (cycles D i)) (↑(cyclesMap f i) (toCycles x)) =
    ↑(Subobject.arrow (cycles D i))
      (toCycles { val := ↑(Hom.f f i) ↑x, property := (_ : ↑(Hom.f f i) ↑x ∈ LinearMap.ker (dFrom D i)) })
[PROOFSTEP]
rw [cyclesMap_arrow_apply, toKernelSubobject_arrow, toKernelSubobject_arrow]
[GOAL]
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ (homologyFunctor (ModuleCat R) c i).map f = (homologyFunctor (ModuleCat R) c i).map g
[PROOFSTEP]
apply homology_ext
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
⊢ ∀ (x : { x // x ∈ LinearMap.ker (dFrom C i) }),
    ↑((homologyFunctor (ModuleCat R) c i).map f)
        (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x)) =
      ↑((homologyFunctor (ModuleCat R) c i).map g)
        (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x))
[PROOFSTEP]
intro x
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑((homologyFunctor (ModuleCat R) c i).map f)
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x)) =
    ↑((homologyFunctor (ModuleCat R) c i).map g)
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x))
[PROOFSTEP]
simp only [homologyFunctor_map]
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo f i) (Hom.sqFrom f i)
          (_ : (Hom.sqTo f i).right = (Hom.sqTo f i).right))
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x)) =
    ↑(homology.map (_ : dTo C i ≫ dFrom C i = 0) (_ : dTo D i ≫ dFrom D i = 0) (Hom.sqTo g i) (Hom.sqFrom g i)
          (_ : (Hom.sqTo g i).right = (Hom.sqTo g i).right))
      (↑(cokernel.π (imageToKernel (dTo C i) (dFrom C i) (_ : dTo C i ≫ dFrom C i = 0))) (↑toKernelSubobject x))
[PROOFSTEP]
erw [homology.π_map_apply, homology.π_map_apply]
  -- To check that two elements are equal mod boundaries, it suffices to exhibit a boundary:
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
      (↑(kernelSubobjectMap (Hom.sqFrom f i)) (↑toKernelSubobject x)) =
    ↑(homology.π (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
      (↑(kernelSubobjectMap (Hom.sqFrom g i)) (↑toKernelSubobject x))
[PROOFSTEP]
refine'
  cokernel_π_imageSubobject_ext _ _ ((toPrev i h.hom) x.1)
    _
      -- Moreover, to check that two cycles are equal, it suffices to check their underlying elements:
[GOAL]
case w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(kernelSubobjectMap (Hom.sqFrom f i)) (↑toKernelSubobject x) =
    ↑(kernelSubobjectMap (Hom.sqFrom g i)) (↑toKernelSubobject x) +
      ↑(imageToKernel (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
        (↑(factorThruImageSubobject (dTo D i)) (↑(↑(toPrev i) h.hom) ↑x))
[PROOFSTEP]
ext
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Subobject.arrow (cycles D i)) (↑(kernelSubobjectMap (Hom.sqFrom f i)) (↑toKernelSubobject x)) =
    ↑(Subobject.arrow (cycles D i))
      (↑(kernelSubobjectMap (Hom.sqFrom g i)) (↑toKernelSubobject x) +
        ↑(imageToKernel (dTo D i) (dFrom D i) (_ : dTo D i ≫ dFrom D i = 0))
          (↑(factorThruImageSubobject (dTo D i)) (↑(↑(toPrev i) h.hom) ↑x)))
[PROOFSTEP]
erw [map_add, CategoryTheory.Limits.kernelSubobjectMap_arrow_apply,
  CategoryTheory.Limits.kernelSubobjectMap_arrow_apply, ModuleCat.toKernelSubobject_arrow, imageToKernel_arrow_apply,
  imageSubobject_arrow_comp_apply]
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ ↑(Hom.sqFrom f i).left ↑x = ↑(Hom.sqFrom g i).left ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
rw [Hom.sqFrom_left, Hom.sqFrom_left, h.comm i, LinearMap.add_apply, LinearMap.add_apply, prevD_eq_toPrev_dTo,
  dNext_eq_dFrom_fromNext, comp_apply, comp_apply, x.2, map_zero]
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ 0 + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x) + ↑(Hom.f g i) ↑x = ↑(Hom.f g i) ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
dsimp
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ 0 + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x) + ↑(Hom.f g i) ↑x = ↑(Hom.f g i) ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
abel
[GOAL]
case w.w
R : Type v
inst✝ : Ring R
ι : Type u_1
c : ComplexShape ι
C D : HomologicalComplex (ModuleCat R) c
f g : C ⟶ D
h : Homotopy f g
i : ι
x : { x // x ∈ LinearMap.ker (dFrom C i) }
⊢ 0 + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x) + ↑(Hom.f g i) ↑x = ↑(Hom.f g i) ↑x + ↑(dTo D i) (↑(↑(toPrev i) h.hom) ↑x)
[PROOFSTEP]
abel
