[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
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : Factors f h
u : Y ⟶ f.obj.left
hu : u ≫ arrow f = h
⊢ (u ≫ ((forget X).map e.hom).left) ≫ arrow g = h
[PROOFSTEP]
simp [hu]
[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
Y : C
h : Y ⟶ X
e : f ≅ g
x✝ : Factors g h
u : Y ⟶ g.obj.left
hu : u ≫ arrow g = h
⊢ (u ≫ ((forget X).map e.inv).left) ≫ arrow f = h
[PROOFSTEP]
simp [hu]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P : Subobject Y
f : X ⟶ Y
⊢ ∀ (a b : MonoOver Y), Setoid.r a b → (fun P => MonoOver.Factors P f) a = (fun P => MonoOver.Factors P f) b
[PROOFSTEP]
rintro P Q ⟨h⟩
[GOAL]
case intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) P = (fun P => MonoOver.Factors P f) Q
[PROOFSTEP]
apply propext
[GOAL]
case intro.a
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) P ↔ (fun P => MonoOver.Factors P f) Q
[PROOFSTEP]
constructor
[GOAL]
case intro.a.mp
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) P → (fun P => MonoOver.Factors P f) Q
[PROOFSTEP]
rintro ⟨i, w⟩
[GOAL]
case intro.a.mp.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ P.obj.left
w : i ≫ MonoOver.arrow P = f
⊢ MonoOver.Factors Q f
[PROOFSTEP]
exact ⟨i ≫ h.hom.left, by erw [Category.assoc, Over.w h.hom, w]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ P.obj.left
w : i ≫ MonoOver.arrow P = f
⊢ (i ≫ h.hom.left) ≫ MonoOver.arrow Q = f
[PROOFSTEP]
erw [Category.assoc, Over.w h.hom, w]
[GOAL]
case intro.a.mpr
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
⊢ (fun P => MonoOver.Factors P f) Q → (fun P => MonoOver.Factors P f) P
[PROOFSTEP]
rintro ⟨i, w⟩
[GOAL]
case intro.a.mpr.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ Q.obj.left
w : i ≫ MonoOver.arrow Q = f
⊢ MonoOver.Factors P f
[PROOFSTEP]
exact ⟨i ≫ h.inv.left, by erw [Category.assoc, Over.w h.inv, w]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P✝ : Subobject Y
f : X ⟶ Y
P Q : MonoOver Y
h : P ≅ Q
i : X ⟶ Q.obj.left
w : i ≫ MonoOver.arrow Q = f
⊢ (i ≫ h.inv.left) ≫ MonoOver.arrow P = f
[PROOFSTEP]
erw [Category.assoc, Over.w h.inv, w]
[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
⊢ 𝟙 X ≫ MonoOver.arrow (MonoOver.mk' f) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
P : Subobject X
⊢ 𝟙 (underlying.obj P) ≫ MonoOver.arrow (representative.obj P) = arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ Factors P (f ≫ g)
[PROOFSTEP]
induction' P using Quotient.ind' with P
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h✝ : Factors P✝ g
P : MonoOver Z
h : Factors (Quotient.mk'' P) g
⊢ Factors (Quotient.mk'' P) (f ≫ g)
[PROOFSTEP]
obtain ⟨g, rfl⟩ := h
[GOAL]
case h.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
h : Factors P✝ (g ≫ MonoOver.arrow P)
⊢ Factors (Quotient.mk'' P) (f ≫ g ≫ MonoOver.arrow P)
[PROOFSTEP]
exact ⟨f ≫ g, by simp⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P✝ : Subobject Z
f : X ⟶ Y
P : MonoOver Z
g : Y ⟶ P.obj.left
h : Factors P✝ (g ≫ MonoOver.arrow P)
⊢ (f ≫ g) ≫ MonoOver.arrow P = f ≫ g ≫ MonoOver.arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
⊢ 0 ≫ MonoOver.arrow (representative.obj P) = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ Factors P f → Factors Q f
[PROOFSTEP]
simp only [factors_iff]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
⊢ MonoOver.Factors (representative.obj P) f → MonoOver.Factors (representative.obj Q) f
[PROOFSTEP]
exact fun ⟨u, hu⟩ => ⟨u ≫ ofLE _ _ h, by simp [← hu]⟩
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
x✝ : MonoOver.Factors (representative.obj P) f
u : Z ⟶ (representative.obj P).obj.left
hu : u ≫ MonoOver.arrow (representative.obj P) = f
⊢ (u ≫ ofLE P Q h) ≫ MonoOver.arrow (representative.obj Q) = f
[PROOFSTEP]
simp [← hu]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : C
P : Subobject X
h : Factors P (arrow P)
⊢ factorThru P (arrow P) h = 𝟙 (underlying.obj P)
[PROOFSTEP]
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
P : Subobject X
h : Factors P (arrow P)
⊢ factorThru P (arrow P) h ≫ arrow P = 𝟙 (underlying.obj P) ≫ arrow P
[PROOFSTEP]
simp
[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
⊢ factorThru (mk f) f (_ : Factors (mk f) f) = (underlyingIso f).inv
[PROOFSTEP]
ext
[GOAL]
case h
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
⊢ factorThru (mk f) f (_ : Factors (mk f) f) ≫ arrow (mk f) = (underlyingIso f).inv ≫ arrow (mk f)
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : Factors P (f ≫ arrow P)
⊢ factorThru P (f ≫ arrow P) h = f
[PROOFSTEP]
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 Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : Factors P (f ≫ arrow P)
⊢ factorThru P (f ≫ arrow P) h ≫ arrow P = f ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ factorThru P f h = 0 ↔ f = 0
[PROOFSTEP]
fconstructor
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ factorThru P f h = 0 → f = 0
[PROOFSTEP]
intro w
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h = 0
⊢ f = 0
[PROOFSTEP]
replace w := w =≫ P.arrow
[GOAL]
case mp
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
w : factorThru P f h ≫ arrow P = 0 ≫ arrow P
⊢ f = 0
[PROOFSTEP]
simpa using w
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
f : X ⟶ Y
h : Factors P f
⊢ f = 0 → factorThru P f h = 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h = 0
[PROOFSTEP]
ext
[GOAL]
case mpr.h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h ≫ arrow P = 0 ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ f ≫ factorThru P g h = factorThru P (f ≫ g) (_ : Factors P (f ≫ g))
[PROOFSTEP]
apply (cancel_mono P.arrow).mp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X✝ Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z : C
P : Subobject Z
f : X ⟶ Y
g : Y ⟶ Z
h : Factors P g
⊢ (f ≫ factorThru P g h) ≫ arrow P = factorThru P (f ≫ g) (_ : Factors P (f ≫ g)) ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasZeroMorphisms C
X Y : C
P : Subobject Y
h : Factors P 0
⊢ factorThru P 0 h = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : Factors P f
⊢ factorThru Q f (_ : Factors Q f) = factorThru P f w ≫ ofLE P Q h
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y✝ Z✝ : C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
Y Z : C
P Q : Subobject Y
f : Z ⟶ Y
h : P ≤ Q
w : Factors P f
⊢ factorThru Q f (_ : Factors Q f) ≫ arrow Q = (factorThru P f w ≫ ofLE P Q h) ≫ arrow Q
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
wf : Factors P f
wg : Factors P g
⊢ (factorThru P f wf + factorThru P g wg) ≫ MonoOver.arrow (representative.obj P) = f + g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
wg : Factors P g
⊢ factorThru P (f + g) w = factorThru P f wf + factorThru P g wg
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
wg : Factors P g
⊢ factorThru P (f + g) w ≫ arrow P = (factorThru P f wf + factorThru P g wg) ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wg : Factors P g
⊢ (factorThru P (f + g) w - factorThru P g wg) ≫ MonoOver.arrow (representative.obj P) = f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wg : Factors P g
⊢ factorThru P (f + g) w - factorThru P g wg = factorThru P f (_ : Factors P f)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wg : Factors P g
⊢ (factorThru P (f + g) w - factorThru P g wg) ≫ arrow P = factorThru P f (_ : Factors P f) ≫ arrow P
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
⊢ (factorThru P (f + g) w - factorThru P f wf) ≫ MonoOver.arrow (representative.obj P) = g
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
⊢ factorThru P (f + g) w - factorThru P f wf = factorThru P g (_ : Factors P g)
[PROOFSTEP]
ext
[GOAL]
case h
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X✝ Y✝ Z : C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive C
X Y : C
P : Subobject Y
f g : X ⟶ Y
w : Factors P (f + g)
wf : Factors P f
⊢ (factorThru P (f + g) w - factorThru P f wf) ≫ arrow P = factorThru P g (_ : Factors P g) ≫ arrow P
[PROOFSTEP]
simp
