[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
⊢ ∀ (a b : f ⟶ g), a = b
[PROOFSTEP]
intro h₁ h₂
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ h₁ = h₂
[PROOFSTEP]
apply Over.OverMorphism.ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
f g : MonoOver X
h₁ h₂ : f ⟶ g
⊢ h₁.left = h₂.left
[PROOFSTEP]
erw [← cancel_mono g.arrow, Over.w h₁, Over.w h₂]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
f g : MonoOver X
h : f.obj.left ≅ g.obj.left
w : autoParam (h.hom ≫ arrow g = arrow f) _auto✝
⊢ h.inv ≫ arrow f = arrow g
[PROOFSTEP]
rw [h.inv_comp_eq, w]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
g : MonoOver Y
⊢ Mono ((Over.pullback f).obj ((forget Y).obj g)).hom
[PROOFSTEP]
haveI : Mono ((forget Y).obj g).hom := (inferInstance : Mono g.arrow)
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasPullbacks C
f : X ⟶ Y
g : MonoOver Y
this : Mono ((forget Y).obj g).hom
⊢ Mono ((Over.pullback f).obj ((forget Y).obj g)).hom
[PROOFSTEP]
apply pullback.snd_of_mono
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g : MonoOver X
⊢ Mono ((Over.map f).obj ((forget X).obj g)).hom
[PROOFSTEP]
apply mono_comp g.arrow f
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ g ⟶ h
[PROOFSTEP]
refine' homMk e.left _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ e.left ≫ arrow h = arrow g
[PROOFSTEP]
rw [← cancel_mono f, assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
f : X ⟶ Y
inst✝ : Mono f
g h : MonoOver X
e : (map f).obj g ⟶ (map f).obj h
⊢ e.left ≫ arrow h ≫ f = arrow g ≫ f
[PROOFSTEP]
apply w e
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.hom ≫ e.inv) = map (𝟙 A)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
A B : C
e : A ≅ B
⊢ map (e.inv ≫ e.hom) = map (𝟙 B)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver X
⊢ Mono ((Over.post e.functor).obj ((forget X).obj f)).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver X
⊢ Mono (e.functor.map (arrow f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver (e.functor.obj X)
⊢ Mono ((Over.post e.inverse).obj ((forget (e.functor.obj X)).obj f)).hom
[PROOFSTEP]
dsimp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
e : C ≌ D
f : MonoOver (e.functor.obj X)
⊢ Mono (e.inverse.map (arrow f))
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ (fun f => imageMonoOver f.hom) f ⟶ (fun f => imageMonoOver f.hom) g
[PROOFSTEP]
apply (forget X).preimage _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ (forget X).obj ((fun f => imageMonoOver f.hom) f) ⟶ (forget X).obj ((fun f => imageMonoOver f.hom) g)
[PROOFSTEP]
apply Over.homMk _ _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ ((forget X).obj ((fun f => imageMonoOver f.hom) f)).left ⟶ ((forget X).obj ((fun f => imageMonoOver f.hom) g)).left
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ ?m.186308 ≫ ((forget X).obj ((fun f => imageMonoOver f.hom) g)).hom =
    ((forget X).obj ((fun f => imageMonoOver f.hom) f)).hom
[PROOFSTEP]
refine'
  image.lift
    { I := Limits.image _
      m := image.ι g.hom
      e := k.left ≫ factorThruImage g.hom }
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f g : Over X
k : f ⟶ g
⊢ image.lift (MonoFactorisation.mk (Limits.image g.hom) (image.ι g.hom) (k.left ≫ factorThruImage g.hom)) ≫
      ((forget X).obj ((fun f => imageMonoOver f.hom) g)).hom =
    ((forget X).obj ((fun f => imageMonoOver f.hom) f)).hom
[PROOFSTEP]
apply image.lift_fac
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ f ⟶ (forget X).obj g
[PROOFSTEP]
apply Over.homMk (factorThruImage f.hom ≫ k.left) _
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ (factorThruImage f.hom ≫ k.left) ≫ g.obj.hom = f.hom
[PROOFSTEP]
change (factorThruImage f.hom ≫ k.left) ≫ _ = f.hom
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ (factorThruImage f.hom ≫ k.left) ≫ g.obj.hom = f.hom
[PROOFSTEP]
rw [assoc, Over.w k]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : image.obj f ⟶ g
⊢ factorThruImage f.hom ≫ (image.obj f).obj.hom = f.hom
[PROOFSTEP]
apply image.fac
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ image.obj f ⟶ g
[PROOFSTEP]
refine' Over.homMk _ _
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ (image.obj f).obj.left ⟶ g.obj.left
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ ?refine'_1 ≫ g.obj.hom = (image.obj f).obj.hom
[PROOFSTEP]
refine'
  image.lift
    { I := g.obj.left
      m := g.arrow
      e := k.left
      fac := Over.w k }
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left) ≫ g.obj.hom = (image.obj f).obj.hom
[PROOFSTEP]
apply image.lift_fac
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ (fun k => Over.homMk (factorThruImage f.hom ≫ k.left))
      ((fun k => Over.homMk (image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left))) k) =
    k
[PROOFSTEP]
ext1
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ ((fun k => Over.homMk (factorThruImage f.hom ≫ k.left))
        ((fun k => Over.homMk (image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left))) k)).left =
    k.left
[PROOFSTEP]
change factorThruImage _ ≫ image.lift _ = _
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ factorThruImage f.hom ≫ image.lift (MonoFactorisation.mk g.obj.left (arrow g) k.left) = k.left
[PROOFSTEP]
rw [← cancel_mono g.arrow, assoc, image.lift_fac, image.fac f.hom]
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasImages C
f : Over X
g : MonoOver X
k : f ⟶ (forget X).obj g
⊢ f.hom = k.left ≫ arrow g
[PROOFSTEP]
exact (Over.w k).symm
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
⊢ (X_1 : MonoOver X) → (exists f).obj X_1 ≅ (map f).obj X_1
[PROOFSTEP]
intro Z
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (exists f).obj Z ≅ (map f).obj Z
[PROOFSTEP]
suffices : (forget _).obj ((exists f).obj Z) ≅ (forget _).obj ((map f).obj Z)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
this : (forget Y).obj ((exists f).obj Z) ≅ (forget Y).obj ((map f).obj Z)
⊢ (exists f).obj Z ≅ (map f).obj Z
case this
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (forget Y).obj ((exists f).obj Z) ≅ (forget Y).obj ((map f).obj Z)
[PROOFSTEP]
apply (forget _).preimageIso this
[GOAL]
case this
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (forget Y).obj ((exists f).obj Z) ≅ (forget Y).obj ((map f).obj Z)
[PROOFSTEP]
apply Over.isoMk _ _
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ ((forget Y).obj ((exists f).obj Z)).left ≅ ((forget Y).obj ((map f).obj Z)).left
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ ?m.226355.hom ≫ ((forget Y).obj ((map f).obj Z)).hom = ((forget Y).obj ((exists f).obj Z)).hom
[PROOFSTEP]
apply imageMonoIsoSource (Z.arrow ≫ f)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
X Y Z✝ : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasImages C
f : X ⟶ Y
inst✝ : Mono f
Z : MonoOver X
⊢ (imageMonoIsoSource (arrow Z ≫ f)).hom ≫ ((forget Y).obj ((map f).obj Z)).hom =
    ((forget Y).obj ((exists f).obj Z)).hom
[PROOFSTEP]
apply imageMonoIsoSource_hom_self
