[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hI : F.I = F'.I
hm : F.m = eqToHom hI ≫ F'.m
⊢ F = F'
[PROOFSTEP]
cases' F with _ Fm _ _ Ffac
[GOAL]
case mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F' : MonoFactorisation f
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝ : Mono Fm
e✝ : X ⟶ I✝
Ffac : e✝ ≫ Fm = f
hI : (mk I✝ Fm e✝).I = F'.I
hm : (mk I✝ Fm e✝).m = eqToHom hI ≫ F'.m
⊢ mk I✝ Fm e✝ = F'
[PROOFSTEP]
cases' F' with _ Fm' _ _ Ffac'
[GOAL]
case mk.mk
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝¹ : C
Fm : I✝¹ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝¹
Ffac : e✝¹ ≫ Fm = f
I✝ : C
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hI : (mk I✝¹ Fm e✝¹).I = (mk I✝ Fm' e✝).I
hm : (mk I✝¹ Fm e✝¹).m = eqToHom hI ≫ (mk I✝ Fm' e✝).m
⊢ mk I✝¹ Fm e✝¹ = mk I✝ Fm' e✝
[PROOFSTEP]
cases' hI
[GOAL]
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : (mk I✝ Fm e✝¹).m = eqToHom (_ : (mk I✝ Fm e✝¹).I = (mk I✝ Fm e✝¹).I) ≫ (mk I✝ Fm' e✝).m
⊢ mk I✝ Fm e✝¹ = mk I✝ Fm' e✝
[PROOFSTEP]
simp at hm 
[GOAL]
case mk.mk.refl
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ mk I✝ Fm e✝¹ = mk I✝ Fm' e✝
[PROOFSTEP]
congr
[GOAL]
case mk.mk.refl.e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ e✝¹ = e✝
[PROOFSTEP]
apply (cancel_mono Fm).1
[GOAL]
case mk.mk.refl.e_e
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
I✝ : C
Fm : I✝ ⟶ Y
m_mono✝¹ : Mono Fm
e✝¹ : X ⟶ I✝
Ffac : e✝¹ ≫ Fm = f
Fm' : I✝ ⟶ Y
m_mono✝ : Mono Fm'
e✝ : X ⟶ I✝
Ffac' : e✝ ≫ Fm' = f
hm : Fm = Fm'
⊢ e✝¹ ≫ Fm = e✝ ≫ Fm
[PROOFSTEP]
rw [Ffac, hm, Ffac']
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
f g : Arrow C
F : MonoFactorisation f.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ (inv sq.left ≫ F.e) ≫ F.m ≫ sq.right = g.hom
[PROOFSTEP]
simp only [fac_assoc, Arrow.w, IsIso.inv_comp_eq, Category.assoc]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : MonoFactorisation f
hF : IsImage F
F' : MonoFactorisation f
⊢ (F.e ≫ lift hF F') ≫ F'.m = F'.e ≫ F'.m
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (lift hF F' ≫ lift hF' F) ≫ F.m = 𝟙 F.I ≫ F.m
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (lift hF' F ≫ lift hF F') ≫ F'.m = 𝟙 F'.I ≫ F'.m
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (isoExt hF hF').hom ≫ F'.m = F.m
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ (isoExt hF hF').inv ≫ F.m = F'.m
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F.e ≫ (isoExt hF hF').hom = F'.e
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F'.e ≫ (isoExt hF hF').inv = F.e
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
F✝ F'✝ : MonoFactorisation f✝
hF✝ : IsImage F✝
hF' : IsImage F'✝
f g : Arrow C
F : MonoFactorisation f.hom
hF : IsImage F
sq : f ⟶ g
inst✝ : IsIso sq
F' : MonoFactorisation g.hom
⊢ (fun F' => lift hF (MonoFactorisation.ofArrowIso F' (inv sq))) F' ≫ F'.m = (MonoFactorisation.ofArrowIso F sq).m
[PROOFSTEP]
simpa only [MonoFactorisation.ofArrowIso_m, Arrow.inv_right, ← Category.assoc, IsIso.comp_inv_eq] using
  hF.lift_fac (F'.ofArrowIso (inv sq))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
F' : MonoFactorisation f
⊢ Mono (lift F')
[PROOFSTEP]
refine @mono_of_mono _ _ _ _ _ _ F'.m ?_
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
F' : MonoFactorisation f
⊢ Mono (lift F' ≫ F'.m)
[PROOFSTEP]
simpa using MonoFactorisation.m_mono _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
F' : MonoFactorisation f
l : image f ⟶ F'.I
w : l ≫ F'.m = image.ι f
⊢ l ≫ F'.m = image.lift F' ≫ F'.m
[PROOFSTEP]
simp [w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).inv ≫ image.ι f = f
[PROOFSTEP]
simp [imageMonoIsoSource]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ f = image.ι f
[PROOFSTEP]
simp only [← imageMonoIsoSource_inv_ι f]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (imageMonoIsoSource f).hom ≫ (imageMonoIsoSource f).inv ≫ image.ι f = image.ι f
[PROOFSTEP]
rw [← Category.assoc, Iso.hom_inv_id, Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
⊢ g = h
[PROOFSTEP]
let q := equalizer.ι g h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
⊢ g = h
[PROOFSTEP]
let e' := equalizer.lift _ w
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
⊢ g = h
[PROOFSTEP]
let F' : MonoFactorisation f :=
  { I := equalizer g h
    m := q ≫ image.ι f
    m_mono := by apply mono_comp
    e := e' }
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
⊢ Mono (q ≫ ι f)
[PROOFSTEP]
apply mono_comp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
⊢ g = h
[PROOFSTEP]
let v := image.lift F'
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
⊢ g = h
[PROOFSTEP]
have t₀ : v ≫ q ≫ image.ι f = image.ι f := image.lift_fac F'
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ g = h
[PROOFSTEP]
have t : v ≫ q = 𝟙 (image f) :=
  (cancel_mono_id (image.ι f)).1
    (by
      convert t₀ using 1
      rw [Category.assoc])
      -- The proof from wikipedia next proves `q ≫ v = 𝟙 _`,
        -- and concludes that `equalizer g h ≅ image f`,
        -- but this isn't necessary.
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ (v ≫ q) ≫ ι f = ι f
[PROOFSTEP]
convert t₀ using 1
[GOAL]
case h.e'_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
⊢ (v ≫ q) ≫ ι f = v ≫ q ≫ ι f
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = h
[PROOFSTEP]
calc
  g = 𝟙 (image f) ≫ g := by rw [Category.id_comp]
  _ = v ≫ q ≫ g := by rw [← t, Category.assoc]
  _ = v ≫ q ≫ h := by rw [equalizer.condition g h]
  _ = 𝟙 (image f) ≫ h := by rw [← Category.assoc, t]
  _ = h := by rw [Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ g = 𝟙 (image f) ≫ g
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ g = v ≫ q ≫ g
[PROOFSTEP]
rw [← t, Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ g = v ≫ q ≫ h
[PROOFSTEP]
rw [equalizer.condition g h]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ v ≫ q ≫ h = 𝟙 (image f) ≫ h
[PROOFSTEP]
rw [← Category.assoc, t]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝¹ : HasImage f
W : C
g h : image f ⟶ W
inst✝ : HasLimit (parallelPair g h)
w : factorThruImage f ≫ g = factorThruImage f ≫ h
q : equalizer g h ⟶ image f := equalizer.ι g h
e' : X ⟶ equalizer g h := equalizer.lift (factorThruImage f) w
F' : MonoFactorisation f := MonoFactorisation.mk (equalizer g h) (q ≫ ι f) e'
v : image f ⟶ F'.I := lift F'
t₀ : v ≫ q ≫ ι f = ι f
t : v ≫ q = 𝟙 (image f)
⊢ 𝟙 (image f) ≫ h = h
[PROOFSTEP]
rw [Category.id_comp]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi f
⊢ Epi (image.ι f)
[PROOFSTEP]
rw [← image.fac f] at E 
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)
[PROOFSTEP]
skip
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
E : Epi (factorThruImage f ≫ image.ι f)
⊢ Epi (image.ι f)
[PROOFSTEP]
exact epi_of_epi (factorThruImage f) (image.ι f)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi f
[PROOFSTEP]
rw [← image.fac f]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
X Y : C
f : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : Epi (image.ι f)
inst✝ : Epi (factorThruImage f)
⊢ Epi (factorThruImage f ≫ image.ι f)
[PROOFSTEP]
apply epi_comp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ ι f' = f'
[PROOFSTEP]
simp only [image.fac]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ (image.eqToHom h ≫ image.eqToHom (_ : f' = f)) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f
[PROOFSTEP]
let F : MonoFactorisation f' := ⟨image f, image.ι f, factorThruImage f, (by aesop_cat)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f ≫ image.ι f = f'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F : MonoFactorisation f' := MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)
⊢ (image.eqToHom h ≫ image.eqToHom (_ : f' = f)) ≫ image.ι f = 𝟙 (image f) ≫ image.ι f
[PROOFSTEP]
dsimp [image.eqToHom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F : MonoFactorisation f' := MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)
⊢ (image.lift (MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')) ≫
        image.lift (MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f))) ≫
      image.ι f =
    𝟙 (image f) ≫ image.ι f
[PROOFSTEP]
rw [Category.id_comp, Category.assoc, image.lift_fac F]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F : MonoFactorisation f' := MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)
⊢ image.lift (MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')) ≫ image.ι f' = image.ι f
[PROOFSTEP]
let F' : MonoFactorisation f := ⟨image f', image.ι f', factorThruImage f', (by aesop_cat)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F : MonoFactorisation f' := MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)
⊢ factorThruImage f' ≫ image.ι f' = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F : MonoFactorisation f' := MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)
F' : MonoFactorisation f := MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')
⊢ image.lift (MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')) ≫ image.ι f' = image.ι f
[PROOFSTEP]
rw [image.lift_fac F']
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ (image.eqToHom (_ : f' = f) ≫ image.eqToHom h) ≫ image.ι f' = 𝟙 (image f') ≫ image.ι f'
[PROOFSTEP]
let F' : MonoFactorisation f := ⟨image f', image.ι f', factorThruImage f', (by aesop_cat)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
⊢ factorThruImage f' ≫ image.ι f' = f
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F' : MonoFactorisation f := MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')
⊢ (image.eqToHom (_ : f' = f) ≫ image.eqToHom h) ≫ image.ι f' = 𝟙 (image f') ≫ image.ι f'
[PROOFSTEP]
dsimp [image.eqToHom]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F' : MonoFactorisation f := MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')
⊢ (image.lift (MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)) ≫
        image.lift (MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f'))) ≫
      image.ι f' =
    𝟙 (image f') ≫ image.ι f'
[PROOFSTEP]
rw [Category.id_comp, Category.assoc, image.lift_fac F']
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F' : MonoFactorisation f := MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')
⊢ image.lift (MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)) ≫ image.ι f = image.ι f'
[PROOFSTEP]
let F : MonoFactorisation f' := ⟨image f, image.ι f, factorThruImage f, (by aesop_cat)⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F' : MonoFactorisation f := MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')
⊢ factorThruImage f ≫ image.ι f = f'
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝¹ : HasImage f
inst✝ : HasImage f'
h : f = f'
F' : MonoFactorisation f := MonoFactorisation.mk (image f') (image.ι f') (factorThruImage f')
F : MonoFactorisation f' := MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)
⊢ image.lift (MonoFactorisation.mk (image f) (image.ι f) (factorThruImage f)) ≫ image.ι f = image.ι f'
[PROOFSTEP]
rw [image.lift_fac F]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ ι f = (eqToIso h).hom ≫ ι f'
[PROOFSTEP]
apply image.ext
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f = factorThruImage f ≫ (eqToIso h).hom ≫ ι f'
[PROOFSTEP]
dsimp [asIso, image.eqToIso, image.eqToHom]
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f f' : X ⟶ Y
inst✝² : HasImage f
inst✝¹ : HasImage f'
inst✝ : HasEqualizers C
h : f = f'
⊢ factorThruImage f ≫ ι f =
    factorThruImage f ≫ lift (MonoFactorisation.mk (image f') (ι f') (factorThruImage f')) ≫ ι f'
[PROOFSTEP]
rw [image.lift_fac]
  -- Porting note: simp did not fire with this it seems
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ preComp f g ≫ ι g = ι (f ≫ g)
[PROOFSTEP]
dsimp [image.preComp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ lift (MonoFactorisation.mk (image g) (ι g) (f ≫ factorThruImage g)) ≫ ι g = ι (f ≫ g)
[PROOFSTEP]
rw [image.lift_fac]
  -- Porting note: also here, see image.eq_fac
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ factorThruImage (f ≫ g) ≫ preComp f g = f ≫ factorThruImage g
[PROOFSTEP]
simp [image.preComp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (preComp f g)
[PROOFSTEP]
refine @mono_of_mono _ _ _ _ _ _ (image.ι g) ?_
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (preComp f g ≫ ι g)
[PROOFSTEP]
simp only [image.preComp_ι]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ Mono (ι (f ≫ g))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ preComp f (g ≫ h) ≫ preComp g h = eqToHom (_ : f ≫ g ≫ h = (f ≫ g) ≫ h) ≫ preComp (f ≫ g) h
[PROOFSTEP]
apply (cancel_mono (image.ι h)).1
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (preComp f (g ≫ h) ≫ preComp g h) ≫ ι h = (eqToHom (_ : f ≫ g ≫ h = (f ≫ g) ≫ h) ≫ preComp (f ≫ g) h) ≫ ι h
[PROOFSTEP]
dsimp [image.preComp, image.eqToHom]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (lift (MonoFactorisation.mk (image (g ≫ h)) (ι (g ≫ h)) (f ≫ factorThruImage (g ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) (g ≫ factorThruImage h))) ≫
      ι h =
    (lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h))) ≫
      ι h
[PROOFSTEP]
repeat (rw [Category.assoc, image.lift_fac])
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ (lift (MonoFactorisation.mk (image (g ≫ h)) (ι (g ≫ h)) (f ≫ factorThruImage (g ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) (g ≫ factorThruImage h))) ≫
      ι h =
    (lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h))) ≫
      ι h
[PROOFSTEP]
rw [Category.assoc, image.lift_fac]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ lift (MonoFactorisation.mk (image (g ≫ h)) (ι (g ≫ h)) (f ≫ factorThruImage (g ≫ h))) ≫ ι (g ≫ h) =
    (lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
        lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h))) ≫
      ι h
[PROOFSTEP]
rw [Category.assoc, image.lift_fac]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
[PROOFSTEP]
rw [Category.assoc, image.lift_fac]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
W : C
h : Z ⟶ W
inst✝³ : HasImage (g ≫ h)
inst✝² : HasImage (f ≫ g ≫ h)
inst✝¹ : HasImage h
inst✝ : HasImage ((f ≫ g) ≫ h)
⊢ ι (f ≫ g ≫ h) =
    lift (MonoFactorisation.mk (image ((f ≫ g) ≫ h)) (ι ((f ≫ g) ≫ h)) (factorThruImage ((f ≫ g) ≫ h))) ≫
      lift (MonoFactorisation.mk (image h) (ι h) ((f ≫ g) ≫ factorThruImage h)) ≫ ι h
[PROOFSTEP]
rw [image.lift_fac, image.lift_fac]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝³ : HasEqualizers C
inst✝² : HasImage g
inst✝¹ : HasImage (f ≫ g)
inst✝ : Epi f
⊢ Epi (preComp f g)
[PROOFSTEP]
apply @epi_of_epi_fac _ _ _ _ _ _ _ _ ?_ (image.factorThruImage_preComp _ _)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝³ : HasEqualizers C
inst✝² : HasImage g
inst✝¹ : HasImage (f ≫ g)
inst✝ : Epi f
⊢ Epi (f ≫ factorThruImage g)
[PROOFSTEP]
exact epi_comp _ _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ (fun F' => image.lift (MonoFactorisation.ofIsoComp f F')) F' ≫ F'.m =
    (MonoFactorisation.isoComp (Image.monoFactorisation g) f).m
[PROOFSTEP]
dsimp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = image.ι g
[PROOFSTEP]
have : (MonoFactorisation.ofIsoComp f F').m = F'.m := rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : IsIso f
inst✝ : HasImage g
F' : MonoFactorisation (f ≫ g)
this : (MonoFactorisation.ofIsoComp f F').m = F'.m
⊢ image.lift (MonoFactorisation.ofIsoComp f F') ≫ F'.m = image.ι g
[PROOFSTEP]
rw [← this, image.lift_fac (MonoFactorisation.ofIsoComp f F')]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ preComp f g ≫ lift (MonoFactorisation.mk (image (f ≫ g)) (ι (f ≫ g)) (inv f ≫ factorThruImage (f ≫ g))) =
    𝟙 (image (f ≫ g))
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ factorThruImage (f ≫ g) ≫
      preComp f g ≫ lift (MonoFactorisation.mk (image (f ≫ g)) (ι (f ≫ g)) (inv f ≫ factorThruImage (f ≫ g))) =
    factorThruImage (f ≫ g) ≫ 𝟙 (image (f ≫ g))
[PROOFSTEP]
simp [image.preComp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ lift (MonoFactorisation.mk (image (f ≫ g)) (ι (f ≫ g)) (inv f ≫ factorThruImage (f ≫ g))) ≫ preComp f g = 𝟙 (image g)
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f✝ : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
f : X ⟶ Y
inst✝¹ : IsIso f
inst✝ : HasImage g
⊢ factorThruImage g ≫
      lift (MonoFactorisation.mk (image (f ≫ g)) (ι (f ≫ g)) (inv f ≫ factorThruImage (f ≫ g))) ≫ preComp f g =
    factorThruImage g ≫ 𝟙 (image g)
[PROOFSTEP]
simp [image.preComp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ (fun F' => image.lift (MonoFactorisation.ofCompIso F')) F' ≫ F'.m =
    (MonoFactorisation.compMono (Image.monoFactorisation f) g).m
[PROOFSTEP]
rw [← Category.comp_id (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m), ← IsIso.inv_hom_id g, ← Category.assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ ((image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g) ≫ g =
    (MonoFactorisation.compMono (Image.monoFactorisation f) g).m
[PROOFSTEP]
refine congrArg (· ≫ g) ?_
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
[PROOFSTEP]
have :
  (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
    image.lift (MonoFactorisation.ofCompIso F') ≫ ((MonoFactorisation.ofCompIso F').m) :=
  by simp only [MonoFactorisation.ofCompIso_I, Category.assoc, MonoFactorisation.ofCompIso_m]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
⊢ (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
    image.lift (MonoFactorisation.ofCompIso F') ≫ (MonoFactorisation.ofCompIso F').m
[PROOFSTEP]
simp only [MonoFactorisation.ofCompIso_I, Category.assoc, MonoFactorisation.ofCompIso_m]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
F' : MonoFactorisation (f ≫ g)
this :
  (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g =
    image.lift (MonoFactorisation.ofCompIso F') ≫ (MonoFactorisation.ofCompIso F').m
⊢ (image.lift (MonoFactorisation.ofCompIso F') ≫ F'.m) ≫ inv g = (Image.monoFactorisation f).m
[PROOFSTEP]
rw [this, image.lift_fac (MonoFactorisation.ofCompIso F'), image.as_ι]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ (compIso f g).hom ≫ ι (f ≫ g) = ι f ≫ g
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage f ≫ (compIso f g).hom ≫ ι (f ≫ g) = factorThruImage f ≫ ι f ≫ g
[PROOFSTEP]
simp [image.compIso]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ (compIso f g).inv ≫ ι f = ι (f ≫ g) ≫ inv g
[PROOFSTEP]
ext
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝² : HasEqualizers C
inst✝¹ : HasImage f
inst✝ : IsIso g
⊢ factorThruImage (f ≫ g) ≫ (compIso f g).inv ≫ ι f = factorThruImage (f ≫ g) ≫ ι (f ≫ g) ≫ inv g
[PROOFSTEP]
simp [image.compIso]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasImage f
⊢ HasImage f
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : HasImage f.hom
⊢ 𝟙 (image f.hom) ≫ image.ι f.hom = image.ι f.hom ≫ (𝟙 f).right
[PROOFSTEP]
aesop
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
m : ImageMap sq
⊢ (factorThruImage f.hom ≫ m.map) ≫ image.ι g.hom = (sq.left ≫ factorThruImage g.hom) ≫ image.ι g.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
F : MonoFactorisation f.hom
F' : MonoFactorisation g.hom
hF' : IsImage F'
map : F.I ⟶ F'.I
map_ι : map ≫ F'.m = F.m ≫ sq.right
⊢ (image.lift F ≫ map ≫ IsImage.lift hF' (Image.monoFactorisation g.hom)) ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
[PROOFSTEP]
simp [map_ι]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : IsIso sq
⊢ image.lift (MonoFactorisation.ofArrowIso (Image.monoFactorisation g.hom) (inv sq)) ≫ image.ι g.hom =
    image.ι f.hom ≫ sq.right
[PROOFSTEP]
erw [← cancel_mono (inv sq).right, Category.assoc, ← MonoFactorisation.ofArrowIso_m, image.lift_fac, Category.assoc, ←
  Comma.comp_right, IsIso.hom_inv_id, Comma.id_right, Category.comp_id]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
f g h : Arrow C
inst✝⁴ : HasImage f.hom
inst✝³ : HasImage g.hom
inst✝² : HasImage h.hom
sq1 : f ⟶ g
sq2 : g ⟶ h
inst✝¹ : HasImageMap sq1
inst✝ : HasImageMap sq2
⊢ ((imageMap sq1).map ≫ (imageMap sq2).map) ≫ image.ι h.hom = image.ι f.hom ≫ (sq1 ≫ sq2).right
[PROOFSTEP]
rw [Category.assoc, ImageMap.map_ι, ImageMap.map_ι_assoc, Comma.comp_right]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
f✝ g✝ : Arrow C
inst✝³ : HasImage f✝.hom
inst✝² : HasImage g✝.hom
sq✝ : f✝ ⟶ g✝
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ map = map'
[PROOFSTEP]
have : map ≫ image.ι g.hom = map' ≫ image.ι g.hom := by rw [map_ι, map_ι']
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
f✝ g✝ : Arrow C
inst✝³ : HasImage f✝.hom
inst✝² : HasImage g✝.hom
sq✝ : f✝ ⟶ g✝
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ map ≫ image.ι g.hom = map' ≫ image.ι g.hom
[PROOFSTEP]
rw [map_ι, map_ι']
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
f✝ g✝ : Arrow C
inst✝³ : HasImage f✝.hom
inst✝² : HasImage g✝.hom
sq✝ : f✝ ⟶ g✝
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
this : map ≫ image.ι g.hom = map' ≫ image.ι g.hom
⊢ map = map'
[PROOFSTEP]
apply (cancel_mono (image.ι g.hom)).1 this
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
f✝ g✝ : Arrow C
inst✝³ : HasImage f✝.hom
inst✝² : HasImage g✝.hom
sq✝ : f✝ ⟶ g✝
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
F G : ImageMap sq
⊢ F.map = G.map
[PROOFSTEP]
apply ImageMap.map_uniq_aux _ F.map_ι _ G.map_ι
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
f✝ g✝ : Arrow C
inst✝³ : HasImage f✝.hom
inst✝² : HasImage g✝.hom
sq✝ : f✝ ⟶ g✝
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ (map = map') = True
[PROOFSTEP]
simp only [Functor.id_obj, eq_iff_iff, iff_true]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
f✝ g✝ : Arrow C
inst✝³ : HasImage f✝.hom
inst✝² : HasImage g✝.hom
sq✝ : f✝ ⟶ g✝
f g : Arrow C
inst✝¹ : HasImage f.hom
inst✝ : HasImage g.hom
sq : f ⟶ g
map : image f.hom ⟶ image g.hom
map_ι : autoParam (map ≫ image.ι g.hom = image.ι f.hom ≫ sq.right) _auto✝
map' : image f.hom ⟶ image g.hom
map_ι' : map' ≫ image.ι g.hom = image.ι f.hom ≫ sq.right
⊢ map = map'
[PROOFSTEP]
apply ImageMap.map_uniq_aux _ map_ι _ map_ι'
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ factorThruImage f.hom ≫ map sq = sq.left ≫ factorThruImage g.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
f g : Arrow C
inst✝² : HasImage f.hom
inst✝¹ : HasImage g.hom
sq : f ⟶ g
inst✝ : HasImageMap sq
⊢ map sq ≫ ι g.hom = ι f.hom ≫ sq.right
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
f g : Arrow C
inst✝⁵ : HasImage f.hom
inst✝⁴ : HasImage g.hom
sq : f ⟶ g
inst✝³ : HasImageMap sq
h : Arrow C
inst✝² : HasImage h.hom
sq' : g ⟶ h
inst✝¹ : HasImageMap sq'
inst✝ : HasImageMap (sq ≫ sq')
⊢ (HasImageMap.imageMap (sq ≫ sq')).map = (imageMapComp sq sq').map
[PROOFSTEP]
congr
[GOAL]
case e_self
C : Type u
inst✝⁶ : Category.{v, u} C
f g : Arrow C
inst✝⁵ : HasImage f.hom
inst✝⁴ : HasImage g.hom
sq : f ⟶ g
inst✝³ : HasImageMap sq
h : Arrow C
inst✝² : HasImage h.hom
sq' : g ⟶ h
inst✝¹ : HasImageMap sq'
inst✝ : HasImageMap (sq ≫ sq')
⊢ HasImageMap.imageMap (sq ≫ sq') = imageMapComp sq sq'
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
f g : Arrow C
inst✝³ : HasImage f.hom
inst✝² : HasImage g.hom
sq : f ⟶ g
inst✝¹ : HasImageMap sq
inst✝ : HasImageMap (𝟙 f)
⊢ (HasImageMap.imageMap (𝟙 f)).map = (imageMapId f).map
[PROOFSTEP]
congr
[GOAL]
case e_self
C : Type u
inst✝⁴ : Category.{v, u} C
f g : Arrow C
inst✝³ : HasImage f.hom
inst✝² : HasImage g.hom
sq : f ⟶ g
inst✝¹ : HasImageMap sq
inst✝ : HasImageMap (𝟙 f)
⊢ HasImageMap.imageMap (𝟙 f) = imageMapId f
[PROOFSTEP]
simp only [eq_iff_true_of_subsingleton]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : StrongEpi f
⊢ f ≫ 𝟙 Y = f
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
G : MonoFactorisation f
⊢ G.e ≫ G.m = F.e ≫ F.m
[PROOFSTEP]
rw [F.toMonoFactorisation.fac, G.fac]
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi F'.e
[PROOFSTEP]
rw [← IsImage.e_isoExt_hom F.toMonoIsImage hF']
[GOAL]
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F : StrongEpiMonoFactorisation f
F' : MonoFactorisation f
hF' : IsImage F'
⊢ StrongEpi (F.e ≫ (IsImage.isoExt (StrongEpiMonoFactorisation.toMonoIsImage F) hF').hom)
[PROOFSTEP]
apply strongEpi_comp
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasImages C
inst✝ : HasStrongEpiImages C
f g : Arrow C
st : f ⟶ g
⊢ (st.left ≫ factorThruImage g.hom) ≫ image.ι g.hom = factorThruImage f.hom ≫ image.ι f.hom ≫ st.right
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ factorThruImage f ≫
      image.lift
          (MonoFactorisation.mk (pullback h y) (pullback.snd ≫ image.ι f)
            (pullback.lift x (factorThruImage f) (_ : x ≫ h = factorThruImage f ≫ y))) ≫
        pullback.fst =
    x
[PROOFSTEP]
simp only [image.fac_lift_assoc, pullback.lift_fst]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ (image.lift
          (MonoFactorisation.mk (pullback h y) (pullback.snd ≫ image.ι f)
            (pullback.lift x (factorThruImage f) (_ : x ≫ h = factorThruImage f ≫ y))) ≫
        pullback.fst) ≫
      h =
    y
[PROOFSTEP]
apply image.ext
[GOAL]
case w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasImages C
inst✝¹ : HasPullbacks C
inst✝ : HasEqualizers C
X✝ Y✝ : C
f : X✝ ⟶ Y✝
A B : C
h : A ⟶ B
h_mono : Mono h
x : X✝ ⟶ A
y : image f ⟶ B
sq : CommSq x (factorThruImage f) h y
⊢ factorThruImage f ≫
      (image.lift
            (MonoFactorisation.mk (pullback h y) (pullback.snd ≫ image.ι f)
              (pullback.lift x (factorThruImage f) (_ : x ≫ h = factorThruImage f ≫ y))) ≫
          pullback.fst) ≫
        h =
    factorThruImage f ≫ y
[PROOFSTEP]
simp only [sq.w, Category.assoc, image.fac_lift_assoc, pullback.lift_fst_assoc]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ (isoStrongEpiMono e m comm).hom ≫ ι f = m
[PROOFSTEP]
dsimp [isoStrongEpiMono]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasStrongEpiMonoFactorisations C
X Y : C
f : X ⟶ Y
I' : C
e : X ⟶ I'
m : I' ⟶ Y
comm : e ≫ m = f
inst✝¹ : StrongEpi e
inst✝ : Mono m
⊢ IsImage.lift (StrongEpiMonoFactorisation.toMonoIsImage (StrongEpiMonoFactorisation.mk (MonoFactorisation.mk I' m e)))
        (Image.monoFactorisation f) ≫
      ι f =
    m
[PROOFSTEP]
apply IsImage.lift_fac
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
let em : StrongEpiMonoFactorisation (F.inv.map f) := (HasStrongEpiMonoFactorisations.has_fac (F.inv.map f)).some
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : Mono (F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y) := mono_comp _ _
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this : Mono (F.map em.m ≫ NatTrans.app (asEquivalence F).counitIso.hom Y)
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
haveI : StrongEpi (F.asEquivalence.counitIso.inv.app X ≫ F.map em.e) := strongEpi_comp _ _
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this✝ : Mono (F.map em.m ≫ NatTrans.app (asEquivalence F).counitIso.hom Y)
this : StrongEpi (NatTrans.app (asEquivalence F).counitIso.inv X ≫ F.map em.e)
⊢ Nonempty (StrongEpiMonoFactorisation f)
[PROOFSTEP]
exact
  Nonempty.intro
    { I := F.obj em.I
      e := F.asEquivalence.counitIso.inv.app X ≫ F.map em.e
      m := F.map em.m ≫ F.asEquivalence.counitIso.hom.app Y
      fac := by
        simpa only [Category.assoc, ← F.map_comp_assoc, em.fac, IsEquivalence.fun_inv_map, Iso.inv_hom_id_app,
          Iso.inv_hom_id_app_assoc] using Category.comp_id _ }
[GOAL]
C : Type u_1
D : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Category.{u_4, u_2} D
F : C ⥤ D
inst✝ : IsEquivalence F
h : HasStrongEpiMonoFactorisations C
X Y : D
f : X ⟶ Y
em : StrongEpiMonoFactorisation ((inv F).map f) :=
  Nonempty.some (_ : Nonempty (StrongEpiMonoFactorisation ((inv F).map f)))
this✝ : Mono (F.map em.m ≫ NatTrans.app (asEquivalence F).counitIso.hom Y)
this : StrongEpi (NatTrans.app (asEquivalence F).counitIso.inv X ≫ F.map em.e)
⊢ (NatTrans.app (asEquivalence F).counitIso.inv X ≫ F.map em.e) ≫
      F.map em.m ≫ NatTrans.app (asEquivalence F).counitIso.hom Y =
    f
[PROOFSTEP]
simpa only [Category.assoc, ← F.map_comp_assoc, em.fac, IsEquivalence.fun_inv_map, Iso.inv_hom_id_app,
  Iso.inv_hom_id_app_assoc] using Category.comp_id _
