[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ d f ≫ f = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
X Y : C
f : X ⟶ Y
⊢ π (kernel f) ≫ kernel.ι f ≫ cokernel.π (d f) = 0
[PROOFSTEP]
rw [← Category.assoc, cokernel.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
⊢ PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
[PROOFSTEP]
haveI := (projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj' P).mp hP
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
this : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
⊢ PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
[PROOFSTEP]
haveI := @Functor.preservesEpimorphisms_of_preserves_of_reflects _ _ _ _ _ _ _ _ this _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : Projective P
this✝ : Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
this : Functor.PreservesEpimorphisms (preadditiveCoyonedaObj (op P))
⊢ PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
[PROOFSTEP]
apply Functor.preservesFiniteColimitsOfPreservesEpisAndKernels
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
⊢ Projective P
[PROOFSTEP]
rw [projective_iff_preservesEpimorphisms_preadditiveCoyoneda_obj']
  -- porting note: this next line wasn't necessary in Lean 3
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
⊢ Functor.PreservesEpimorphisms (preadditiveCoyoneda.obj (op P))
[PROOFSTEP]
dsimp only [preadditiveCoyoneda]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
hP : PreservesFiniteColimits (preadditiveCoyonedaObj (op P))
⊢ Functor.PreservesEpimorphisms (preadditiveCoyonedaObj (op P) ⋙ forget₂ (ModuleCat (End (op P))) AddCommGroupCat)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ 0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0 =
    HomologicalComplex.d (ofComplex Z) 1 0 ≫ Projective.π Z
[PROOFSTEP]
simp only [ofComplex_X, ChainComplex.single₀_obj_X_0, ChainComplex.single₀_obj_X_succ, ComplexShape.down_Rel, not_true,
  ChainComplex.single₀_obj_X_d, comp_zero, ofComplex_d, eqToHom_refl, Category.id_comp, dite_eq_ite, ite_true]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ 0 =
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z)))
          (_ :
            {
                      fst :=
                        syzygies
                          { fst := over Z,
                                snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := over Z,
                                    snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                          snd :=
                            (_ :
                              d
                                    { fst := over Z,
                                          snd :=
                                            { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                                0) } }.snd.fst ≫
                { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
          0).d₀ ≫
      Projective.π Z
[PROOFSTEP]
exact (exact_d_f (Projective.π Z)).w.symm
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Exact (HomologicalComplex.d (ofComplex Z) (0 + 2) (0 + 1)) (HomologicalComplex.d (ofComplex Z) (0 + 1) 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Exact
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (0 + 1)).d₀
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        0).d₀
[PROOFSTEP]
apply exact_d_f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n m : ℕ
⊢ Exact (HomologicalComplex.d (ofComplex Z) (m + 1 + 2) (m + 1 + 1))
    (HomologicalComplex.d (ofComplex Z) (m + 1 + 1) (m + 1))
[PROOFSTEP]
simp only [ofComplex_X, ComplexShape.down_Rel, ofComplex_d, eqToHom_refl, Category.id_comp, dite_eq_ite, not_true,
  ite_true]
  -- Porting note: this is probably required now due to
        -- https://github.com/leanprover/lean4/pull/2146
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n m : ℕ
⊢ Exact
    (if m + 1 + 2 = m + 1 + 1 + 1 then
      (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
          (d (d (Projective.π Z)))
          (_ :
            {
                      fst :=
                        syzygies
                          { fst := over Z,
                                snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                      snd :=
                        {
                          fst :=
                            d
                              { fst := over Z,
                                    snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                          snd :=
                            (_ :
                              d
                                    { fst := over Z,
                                          snd :=
                                            { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                                0) } }.snd.fst ≫
                { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
              0)
          (fun t =>
            { fst := syzygies t.snd.snd.snd.snd.fst,
              snd :=
                { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
          (m + 1 + 1)).d₀
    else 0)
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (m + 1)).d₀
[PROOFSTEP]
erw [if_pos (c := m + 1 + 1 + 1 = m + 2 + 1) rfl]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n m : ℕ
⊢ Exact
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (m + 1 + 1)).d₀
    (ChainComplex.mkAux (over Z) (syzygies (Projective.π Z)) (syzygies (d (Projective.π Z))) (d (Projective.π Z))
        (d (d (Projective.π Z)))
        (_ :
          {
                    fst :=
                      syzygies
                        { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                    snd :=
                      {
                        fst :=
                          d
                            { fst := over Z,
                                  snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd,
                        snd :=
                          (_ :
                            d
                                  { fst := over Z,
                                        snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd ≫
                                { fst := over Z,
                                      snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.2.snd =
                              0) } }.snd.fst ≫
              { fst := over Z, snd := { fst := syzygies (Projective.π Z), snd := d (Projective.π Z) } }.snd.snd =
            0)
        (fun t =>
          { fst := syzygies t.snd.snd.snd.snd.fst,
            snd :=
              { fst := d t.snd.snd.snd.snd.fst, snd := (_ : d t.snd.snd.snd.snd.fst ≫ t.snd.snd.snd.snd.fst = 0) } })
        (m + 1)).d₀
[PROOFSTEP]
apply exact_d_f
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
x✝ :
  (f : HomologicalComplex.X (ofComplex Z) n ⟶ HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) n) ×'
    (f' : HomologicalComplex.X (ofComplex Z) (n + 1) ⟶ HomologicalComplex.X ((ChainComplex.single₀ C).obj Z) (n + 1)) ×'
      f' ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 1) n =
        HomologicalComplex.d (ofComplex Z) (n + 1) n ≫ f
⊢ 0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 2) (n + 1) =
    HomologicalComplex.d (ofComplex Z) (n + 2) (n + 1) ≫ x✝.snd.fst
[PROOFSTEP]
apply HasZeroObject.to_zero_ext
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ ∀ (n : ℕ), Projective (HomologicalComplex.X (ofComplex Z) n)
[PROOFSTEP]
rintro (_ | _ | _ | n)
[GOAL]
case zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective (HomologicalComplex.X (ofComplex Z) Nat.zero)
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
case succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective (HomologicalComplex.X (ofComplex Z) (Nat.succ Nat.zero))
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
case succ.succ.zero
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Projective (HomologicalComplex.X (ofComplex Z) (Nat.succ (Nat.succ Nat.zero)))
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
case succ.succ.succ
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
n : ℕ
⊢ Projective (HomologicalComplex.X (ofComplex Z) (Nat.succ (Nat.succ (Nat.succ n))))
[PROOFSTEP]
apply Projective.projective_over
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ Exact (HomologicalComplex.d (ofComplex Z) 1 0)
    (HomologicalComplex.Hom.f
      (ChainComplex.mkHom (ofComplex Z) ((ChainComplex.single₀ C).obj Z) (Projective.π Z) 0
        (_ :
          0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) 1 0 =
            HomologicalComplex.d (ofComplex Z) 1 0 ≫ Projective.π Z)
        fun n x =>
        { fst := 0,
          snd :=
            (_ :
              0 ≫ HomologicalComplex.d ((ChainComplex.single₀ C).obj Z) (n + 2) (n + 1) =
                HomologicalComplex.d (ofComplex Z) (n + 2) (n + 1) ≫ x.snd.fst) })
      0)
[PROOFSTEP]
simpa using exact_d_f (Projective.π Z)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : EnoughProjectives C
Z : C
⊢ HasProjectiveResolution Z
[PROOFSTEP]
infer_instance
