[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
E✝ X✝ : C
f : 0 ⟶ X✝
e : E✝ ⟶ X✝
x✝ : Epi e
⊢ 0 ≫ e = f
[PROOFSTEP]
ext
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P Q : C
i : P ≅ Q
hP : Projective P
E✝ X✝ : C
f : Q ⟶ X✝
e : E✝ ⟶ X✝
e_epi : Epi e
f' : P ⟶ E✝
hf' : f' ≫ e = i.hom ≫ f
⊢ (i.inv ≫ f') ≫ e = f
[PROOFSTEP]
simp [hf']
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
P Q : C
inst✝² : HasBinaryCoproduct P Q
inst✝¹ : Projective P
inst✝ : Projective Q
E✝ X✝ : C
f : P ⨿ Q ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ coprod.desc (factorThru (coprod.inl ≫ f) e) (factorThru (coprod.inr ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
β : Type v
g : β → C
inst✝¹ : HasCoproduct g
inst✝ : ∀ (b : β), Projective (g b)
E✝ X✝ : C
f : ∐ g ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ (Sigma.desc fun b => factorThru (Sigma.ι g b ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
P Q : C
inst✝³ : HasZeroMorphisms C
inst✝² : HasBinaryBiproduct P Q
inst✝¹ : Projective P
inst✝ : Projective Q
E✝ X✝ : C
f : P ⊞ Q ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ biprod.desc (factorThru (biprod.inl ≫ f) e) (factorThru (biprod.inr ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
β : Type v
g : β → C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasBiproduct g
inst✝ : ∀ (b : β), Projective (g b)
E✝ X✝ : C
f : ⨁ g ⟶ X✝
e : E✝ ⟶ X✝
epi : Epi e
⊢ (biproduct.desc fun b => factorThru (biproduct.ι g b ≫ f) e) ≫ e = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
rcases hP.factors (adj.unit.app P ≫ G.map f) (G.map g) with ⟨f', hf'⟩
[GOAL]
case intro
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = NatTrans.app adj.unit P ≫ G.map f
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
use F.map f' ≫ adj.counit.app _
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = NatTrans.app adj.unit P ≫ G.map f
⊢ (F.map f' ≫ NatTrans.app adj.counit E✝) ≫ g = f
[PROOFSTEP]
rw [Category.assoc, ← Adjunction.counit_naturality, ← Category.assoc, ← F.map_comp, hf']
[GOAL]
case h
C : Type u
inst✝² : Category.{v, u} C
D : Type u'
inst✝¹ : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : Functor.PreservesEpimorphisms G
P : C
hP : Projective P
E✝ X✝ : D
f : F.obj P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
f' : P ⟶ G.obj E✝
hf' : f' ≫ G.map g = NatTrans.app adj.unit P ≫ G.map f
⊢ F.map (NatTrans.app adj.unit P ≫ G.map f) ≫ NatTrans.app adj.counit X✝ = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
haveI := Adjunction.leftAdjointPreservesColimits.{0, 0} adj
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
rcases(@hP).1 (F.map f) (F.map g) with ⟨f', hf'⟩
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ ∃ f', f' ≫ g = f
[PROOFSTEP]
use adj.unit.app _ ≫ G.map f' ≫ (inv <| adj.unit.app _)
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ (NatTrans.app adj.unit P ≫ G.map f' ≫ inv (NatTrans.app adj.unit E✝)) ≫ g = f
[PROOFSTEP]
refine' Faithful.map_injective (F := F) _
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
D : Type u'
inst✝² : Category.{v', u'} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝¹ : Full F
inst✝ : Faithful F
P : C
hP : Projective (F.obj P)
E✝ X✝ : C
f : P ⟶ X✝
g : E✝ ⟶ X✝
x✝ : Epi g
this : PreservesColimitsOfSize.{0, 0, v, v', u, u'} F
f' : F.obj P ⟶ F.obj E✝
hf' : f' ≫ F.map g = F.map f
⊢ F.map ((NatTrans.app adj.unit P ≫ G.map f' ≫ inv (NatTrans.app adj.unit E✝)) ≫ g) = F.map f
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives C ↔ EnoughProjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C
[PROOFSTEP]
all_goals intro H; constructor; intro X; constructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives C → EnoughProjectives D
[PROOFSTEP]
intro H
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
⊢ EnoughProjectives D
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
⊢ ∀ (X : D), Nonempty (ProjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mp.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
X : D
⊢ Nonempty (ProjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
⊢ EnoughProjectives D → EnoughProjectives C
[PROOFSTEP]
intro H
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ EnoughProjectives C
[PROOFSTEP]
constructor
[GOAL]
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
⊢ ∀ (X : C), Nonempty (ProjectivePresentation X)
[PROOFSTEP]
intro X
[GOAL]
case mpr.presentation
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ Nonempty (ProjectivePresentation X)
[PROOFSTEP]
constructor
[GOAL]
case mp.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives C
X : D
⊢ ProjectivePresentation X
[PROOFSTEP]
exact F.symm.projectivePresentationOfMapProjectivePresentation _ (Nonempty.some (H.presentation (F.inverse.obj X)))
[GOAL]
case mpr.presentation.val
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ F : C ≌ D
H : EnoughProjectives D
X : C
⊢ ProjectivePresentation X
[PROOFSTEP]
exact F.projectivePresentationOfMapProjectivePresentation X (Nonempty.some (H.presentation (F.functor.obj X)))
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
⊢ lift h f g hfg w ≫ f = h
[PROOFSTEP]
simp only [Exact.lift]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
⊢ factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
        (factorThruImageSubobject f) ≫
      f =
    h
[PROOFSTEP]
conv_lhs =>
  congr
  rfl
  rw [← imageSubobject_arrow_comp f]
    -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
      (factorThruImageSubobject f) ≫
    f
[PROOFSTEP]
  congr
  rfl
  rw [← imageSubobject_arrow_comp f]
    -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
      (factorThruImageSubobject f) ≫
    f
[PROOFSTEP]
  congr
  rfl
  rw [← imageSubobject_arrow_comp f]
    -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
      (factorThruImageSubobject f) ≫
    f
[PROOFSTEP]
congr
[GOAL]
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
    (factorThruImageSubobject f)
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| f
[PROOFSTEP]
rfl
[GOAL]
case a
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
| f
[PROOFSTEP]
rw [← imageSubobject_arrow_comp f]
  -- See the porting note on `Exact.epi`.
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
⊢ factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
        (factorThruImageSubobject f) ≫
      factorThruImageSubobject f ≫ Subobject.arrow (imageSubobject f) =
    h
[PROOFSTEP]
haveI := hfg.epi
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
inst✝¹ : HasImages C
P Q R S : C
inst✝ : Projective P
h : P ⟶ R
f : Q ⟶ R
g : R ⟶ S
hfg : Exact f g
w : h ≫ g = 0
this : Epi (imageToKernel f g (_ : f ≫ g = 0))
⊢ factorThru (factorThru (factorThruKernelSubobject g h w) (imageToKernel f g (_ : f ≫ g = 0)))
        (factorThruImageSubobject f) ≫
      factorThruImageSubobject f ≫ Subobject.arrow (imageSubobject f) =
    h
[PROOFSTEP]
rw [← Category.assoc, factorThru_comp, ← imageToKernel_arrow f g, ← Category.assoc,
  CategoryTheory.Projective.factorThru_comp, factorThruKernelSubobject_comp_arrow]
