[GOAL]
C : Type u
inst✝ : Category.{v, u} C
P : C
f : Over P
⊢ 𝟙 f.left ≫ f.hom = 𝟙 f.left ≫ f.hom
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
⊢ Transitive (PseudoEqual P)
[PROOFSTEP]
intro f g h ⟨R, p, q, ep, Eq, comm⟩ ⟨R', p', q', ep', eq', comm'⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ PseudoEqual P f h
[PROOFSTEP]
refine' ⟨pullback q p', pullback.fst ≫ p, pullback.snd ≫ q', epi_comp _ _, epi_comp _ _, _⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
f g h : Over P
R : C
p : R ⟶ f.left
q : R ⟶ g.left
ep : Epi p
Eq : Epi q
comm : p ≫ f.hom = q ≫ g.hom
R' : C
p' : R' ⟶ g.left
q' : R' ⟶ h.left
ep' : Epi p'
eq' : Epi q'
comm' : p' ≫ g.hom = q' ≫ h.hom
⊢ (pullback.fst ≫ p) ≫ f.hom = (pullback.snd ≫ q') ≫ h.hom
[PROOFSTEP]
rw [Category.assoc, comm, ← Category.assoc, pullback.condition, Category.assoc, comm', Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
a b : Over P
x✝ : a ≈ b
R : C
p : R ⟶ a.left
q : R ⟶ b.left
ep : Epi p
Eq : Epi q
comm : p ≫ a.hom = q ≫ b.hom
⊢ p ≫ a.hom ≫ f = q ≫ b.hom ≫ f
[PROOFSTEP]
rw [reassoc_of% comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ (fun g_1 => app (f ≫ g) g_1) x ≈ (fun g_1 => app g g_1) ((fun g => app f g) x)
[PROOFSTEP]
simp only [app]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
a : Pseudoelement P
x : Over P
⊢ Over.mk (x.hom ≫ f ≫ g) ≈ Over.mk ((Over.mk (x.hom ≫ f)).hom ≫ g)
[PROOFSTEP]
rw [← Category.assoc, Over.coe_hom]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
x✝ : f ≈ Over.mk 0
R : C
p : R ⟶ f.left
q : R ⟶ (Over.mk 0).left
ep : Epi p
w✝ : Epi q
comm : p ≫ f.hom = q ≫ (Over.mk 0).hom
⊢ p ≫ f.hom = 0
[PROOFSTEP]
simp [comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : Over P
hf : f.hom = 0
⊢ biprod.fst ≫ f.hom = biprod.snd ≫ (Over.mk 0).hom
[PROOFSTEP]
rw [hf, Over.coe_hom, HasZeroMorphisms.comp_zero, HasZeroMorphisms.comp_zero]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a.hom = 0
[PROOFSTEP]
rw [← pseudoZero_aux P a]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0
[PROOFSTEP]
exact Quotient.eq'
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ pseudoApply f 0 = 0
[PROOFSTEP]
rw [pseudoZero_def, pseudoApply_mk']
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Quotient.mk (setoid Q) (Over.mk ((Over.mk 0).hom ≫ f)) = 0
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ pseudoApply 0 (Quotient.mk (setoid P) a') = 0
[PROOFSTEP]
rw [pseudoZero_def, pseudoApply_mk']
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
a : Pseudoelement P
a' : Over P
⊢ Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ 0)) = Quotient.mk (setoid Q) (Over.mk 0)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ f = 0
[PROOFSTEP]
rw [← Category.id_comp f]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0
[PROOFSTEP]
exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : f = 0
a : Pseudoelement P
⊢ pseudoApply f a = 0
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
⊢ Function.Injective (pseudoApply f)
[PROOFSTEP]
intro abar abar'
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
⊢ pseudoApply f abar = pseudoApply f abar' → abar = abar'
[PROOFSTEP]
refine' Quotient.inductionOn₂ abar abar' fun a a' ha => _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ Quotient.mk (setoid P) a = Quotient.mk (setoid P) a'
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ a ≈ a'
[PROOFSTEP]
have : ⟦(a.hom ≫ f : Over Q)⟧ = ⟦↑(a'.hom ≫ f)⟧ := by convert ha
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
⊢ Quotient.mk ?m.324431 (Over.mk (a.hom ≫ f)) = Quotient.mk ?m.324431 (Over.mk (a'.hom ≫ f))
[PROOFSTEP]
convert ha
[GOAL]
case a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
⊢ a ≈ a'
[PROOFSTEP]
have ⟨R, p, q, ep, Eq, comm⟩ := Quotient.exact this
[GOAL]
case a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ a ≈ a'
[PROOFSTEP]
exact
  ⟨R, p, q, ep, Eq,
    (cancel_mono f).1 <| by
      simp only [Category.assoc]
      exact comm⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ (p ≫ a.hom) ≫ f = (q ≫ a'.hom) ≫ f
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Mono f
abar abar' : Pseudoelement P
a a' : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
this : Quotient.mk (setoid Q) (Over.mk (a.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (a'.hom ≫ f))
R : C
p : R ⟶ (Over.mk (a.hom ≫ f)).left
q : R ⟶ (Over.mk (a'.hom ≫ f)).left
ep : Epi p
Eq : Epi q
comm : p ≫ (Over.mk (a.hom ≫ f)).hom = q ≫ (Over.mk (a'.hom ≫ f)).hom
⊢ p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
[PROOFSTEP]
exact comm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = 0
⊢ a = 0
[PROOFSTEP]
rw [← apply_zero f] at ha
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Injective (pseudoApply f)
a : Pseudoelement P
ha : pseudoApply f a = pseudoApply f 0
⊢ a = 0
[PROOFSTEP]
exact h ha
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
P Q : C
f : P ⟶ Q
inst✝ : Epi f
qbar : Pseudoelement Q
q : Over Q
⊢ 𝟙 (pullback f q.hom) ≫ ((fun g => app f g) (Over.mk pullback.fst)).hom = pullback.snd ≫ q.hom
[PROOFSTEP]
rw [Category.id_comp, ← pullback.condition, app_hom, Over.coe_hom]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Function.Surjective (pseudoApply f) → Epi f
[PROOFSTEP]
intro h
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
⊢ Epi f
[PROOFSTEP]
have ⟨pbar, hpbar⟩ := h (𝟙 Q)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
⊢ Epi f
[PROOFSTEP]
have ⟨p, hp⟩ := Quotient.exists_rep pbar
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : Quotient.mk (setoid P) p = pbar
⊢ Epi f
[PROOFSTEP]
have : ⟦(p.hom ≫ f : Over Q)⟧ = ⟦↑(𝟙 Q)⟧ := by
  rw [← hp] at hpbar
  exact hpbar
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : Quotient.mk (setoid P) p = pbar
⊢ Quotient.mk ?m.452467 (Over.mk (p.hom ≫ f)) = Quotient.mk ?m.452467 (Over.mk (𝟙 Q))
[PROOFSTEP]
rw [← hp] at hpbar
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar✝ : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hpbar : pseudoApply f (Quotient.mk (setoid P) p) = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
hp : Quotient.mk (setoid P) p = pbar
⊢ Quotient.mk (?m.485675 hp) (Over.mk (p.hom ≫ f)) = Quotient.mk (?m.485675 hp) (Over.mk (𝟙 Q))
[PROOFSTEP]
exact hpbar
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : Quotient.mk (setoid P) p = pbar
this : Quotient.mk (setoid Q) (Over.mk (p.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (𝟙 Q))
⊢ Epi f
[PROOFSTEP]
have ⟨R, x, y, _, ey, comm⟩ := Quotient.exact this
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : Quotient.mk (setoid P) p = pbar
this : Quotient.mk (setoid Q) (Over.mk (p.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (𝟙 Q))
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ (Over.mk (𝟙 Q)).hom
⊢ Epi f
[PROOFSTEP]
apply @epi_of_epi_fac _ _ _ _ _ (x ≫ p.hom) f y ey
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : Quotient.mk (setoid P) p = pbar
this : Quotient.mk (setoid Q) (Over.mk (p.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (𝟙 Q))
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ (Over.mk (p.hom ≫ f)).hom = y ≫ (Over.mk (𝟙 Q)).hom
⊢ (x ≫ p.hom) ≫ f = y
[PROOFSTEP]
dsimp at comm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : Quotient.mk (setoid P) p = pbar
this : Quotient.mk (setoid Q) (Over.mk (p.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (𝟙 Q))
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q
⊢ (x ≫ p.hom) ≫ f = y
[PROOFSTEP]
rw [Category.assoc, comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
pbar : Pseudoelement P
hpbar : pseudoApply f pbar = Quot.mk (PseudoEqual Q) (Over.mk (𝟙 Q))
p : Over P
hp : Quotient.mk (setoid P) p = pbar
this : Quotient.mk (setoid Q) (Over.mk (p.hom ≫ f)) = Quotient.mk (setoid Q) (Over.mk (𝟙 Q))
R : C
x : R ⟶ (Over.mk (p.hom ≫ f)).left
y : R ⟶ (Over.mk (𝟙 Q)).left
w✝ : Epi x
ey : Epi y
comm : x ≫ p.hom ≫ f = y ≫ 𝟙 Q
⊢ y ≫ 𝟙 Q = y
[PROOFSTEP]
apply Category.comp_id
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
a : Pseudoelement P
⊢ pseudoApply g (pseudoApply f a) = 0
[PROOFSTEP]
rw [← comp_apply, h.w]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
a : Pseudoelement P
⊢ pseudoApply 0 a = 0
[PROOFSTEP]
exact zero_apply _ _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
[PROOFSTEP]
have hb' : b.hom ≫ g = 0 := (pseudoZero_iff _).1 hb
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
[PROOFSTEP]
obtain ⟨c, hc⟩ := KernelFork.IsLimit.lift' (isLimitImage f g h) _ hb'
[GOAL]
case mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ ∃ a, pseudoApply f a = Quotient.mk (setoid Q) b
[PROOFSTEP]
use(pullback.fst : pullback (Abelian.factorThruImage f) c ⟶ P)
    -- It remains to show that the image of this element under `f` is pseudo-equal to `b`.
[GOAL]
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pseudoApply f (Quot.mk (PseudoEqual P) (Over.mk pullback.fst)) = Quotient.mk (setoid Q) b
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ (fun g => app f g) (Over.mk pullback.fst) ≈ b
[PROOFSTEP]
refine'
  ⟨pullback (Abelian.factorThruImage f) c, 𝟙 _, pullback.snd, inferInstance, inferInstance, _⟩
    -- Now we can verify that the diagram commutes.
[GOAL]
case h.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ 𝟙 (pullback (Abelian.factorThruImage f) c) ≫ ((fun g => app f g) (Over.mk pullback.fst)).hom = pullback.snd ≫ b.hom
[PROOFSTEP]
calc
  𝟙 (pullback (Abelian.factorThruImage f) c) ≫ pullback.fst ≫ f = pullback.fst ≫ f := Category.id_comp _
  _ = pullback.fst ≫ Abelian.factorThruImage f ≫ kernel.ι (cokernel.π f) := by rw [Abelian.image.fac]
  _ = (pullback.snd ≫ c) ≫ kernel.ι (cokernel.π f) := by rw [← Category.assoc, pullback.condition]
  _ = pullback.snd ≫ b.hom := by
    rw [Category.assoc]
    congr
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pullback.fst ≫ f = pullback.fst ≫ Abelian.factorThruImage f ≫ kernel.ι (cokernel.π f)
[PROOFSTEP]
rw [Abelian.image.fac]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pullback.fst ≫ Abelian.factorThruImage f ≫ kernel.ι (cokernel.π f) = (pullback.snd ≫ c) ≫ kernel.ι (cokernel.π f)
[PROOFSTEP]
rw [← Category.assoc, pullback.condition]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ (pullback.snd ≫ c) ≫ kernel.ι (cokernel.π f) = pullback.snd ≫ b.hom
[PROOFSTEP]
rw [Category.assoc]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
h : Exact f g
b' : Pseudoelement Q
b : Over Q
hb : pseudoApply g (Quotient.mk (setoid Q) b) = 0
hb' : b.hom ≫ g = 0
c : (𝟭 C).obj b.left ⟶ (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)).pt
hc : c ≫ Fork.ι (KernelFork.ofι (image.ι f) (_ : image.ι f ≫ g = 0)) = b.hom
⊢ pullback.snd ≫ c ≫ kernel.ι (cokernel.π f) = pullback.snd ≫ b.hom
[PROOFSTEP]
congr
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : Q ⟶ R
a : P ⟶ Q
h : a ≫ f = 0
⊢ pseudoApply f (Quot.mk (PseudoEqual Q) (Over.mk a)) = 0
[PROOFSTEP]
simp [over_coe_def, pseudoApply_mk', Over.coe_hom, h]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
a : Pseudoelement P
⊢ pseudoApply (f ≫ g) a = 0
[PROOFSTEP]
rw [comp_apply, h₁ a]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
have : g (kernel.ι g) = 0 :=
  apply_eq_zero_of_comp_eq_zero _ _
    (kernel.condition _)
      -- By pseudo-exactness, we get a preimage.
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
obtain ⟨a', ha⟩ := h₂ _ this
[GOAL]
case intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
ha : pseudoApply f a' = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
obtain ⟨a, ha'⟩ := Quotient.exists_rep a'
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
ha : pseudoApply f a' = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
a : Over P
ha' : Quotient.mk (setoid P) a = a'
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
rw [← ha'] at ha
[GOAL]
case intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
obtain ⟨Z, r, q, _, eq, comm⟩ := Quotient.exact ha
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
obtain ⟨z, _, hz₂⟩ :=
  @pullback.lift' _ _ _ _ _ _ (kernel.ι (cokernel.π f)) (kernel.ι g) _ (r ≫ a.hom ≫ Abelian.factorThruImage f) q
    (by
      simp only [Category.assoc, Abelian.image.fac]
      exact comm)
      -- Let's give a name to the second pullback morphism.
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ (r ≫ a.hom ≫ Abelian.factorThruImage f) ≫ kernel.ι (cokernel.π f) = q ≫ kernel.ι g
[PROOFSTEP]
simp only [Category.assoc, Abelian.image.fac]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
⊢ r ≫ a.hom ≫ f = q ≫ kernel.ι g
[PROOFSTEP]
exact comm
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
let j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
haveI pe : Epi j := epi_of_epi_fac hz₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
haveI : IsIso j :=
  isIso_of_mono_of_epi
    _
      -- But then `kernel.ι g` can be expressed using all of the maps of the pullback square, and we
            -- are done.
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this✝ : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
this : IsIso j
⊢ kernel.ι g ≫ cokernel.π f = 0
[PROOFSTEP]
rw [(Iso.eq_inv_comp (asIso j)).2 pullback.condition.symm]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
x✝ :
  (∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0) ∧
    ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
h₁ : ∀ (a : Pseudoelement P), pseudoApply g (pseudoApply f a) = 0
h₂ : ∀ (b : Pseudoelement Q), pseudoApply g b = 0 → ∃ a, pseudoApply f a = b
this✝ : pseudoApply g (Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))) = 0
a' : Pseudoelement P
a : Over P
ha : pseudoApply f (Quotient.mk (setoid P) a) = Quot.mk (PseudoEqual Q) (Over.mk (kernel.ι g))
ha' : Quotient.mk (setoid P) a = a'
Z : C
r : Z ⟶ ((fun g => app f g) a).left
q : Z ⟶ (Over.mk (kernel.ι g)).left
w✝ : Epi r
eq : Epi q
comm : r ≫ ((fun g => app f g) a).hom = q ≫ (Over.mk (kernel.ι g)).hom
z : Z ⟶ pullback (kernel.ι (cokernel.π f)) (kernel.ι g)
left✝ : z ≫ pullback.fst = r ≫ a.hom ≫ Abelian.factorThruImage f
hz₂ : z ≫ pullback.snd = q
j : pullback (kernel.ι (cokernel.π f)) (kernel.ι g) ⟶ kernel g := pullback.snd
pe : Epi j
this : IsIso j
⊢ ((asIso j).inv ≫ pullback.fst ≫ kernel.ι (cokernel.π f)) ≫ cokernel.π f = 0
[PROOFSTEP]
simp only [Category.assoc, kernel.condition, HasZeroMorphisms.comp_zero]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
⊢ Quotient.mk (setoid Q) (Over.mk (a'' ≫ f)) = Quotient.mk (setoid Q) (Over.mk 0)
[PROOFSTEP]
dsimp at comm
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝ : Epi q
comm : p ≫ a.hom ≫ f = q ≫ a'.hom ≫ f
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
⊢ Quotient.mk (setoid Q) (Over.mk (a'' ≫ f)) = Quotient.mk (setoid Q) (Over.mk 0)
[PROOFSTEP]
simp [sub_eq_zero.2 comm]
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
⊢ pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g (Quotient.mk (setoid P) a)
[PROOFSTEP]
obtain ⟨X, p', q', ep', _, comm'⟩ := Quotient.exact hh
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
X : C
p' : X ⟶ ((fun g_1 => app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom
⊢ pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g (Quotient.mk (setoid P) a)
[PROOFSTEP]
have : a'.hom ≫ g = 0 := by
  apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
  simpa using comm'
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
X : C
p' : X ⟶ ((fun g_1 => app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom
⊢ a'.hom ≫ g = 0
[PROOFSTEP]
apply (epi_iff_cancel_zero _).1 ep' _ (a'.hom ≫ g)
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
X : C
p' : X ⟶ ((fun g_1 => app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom
⊢ p' ≫ a'.hom ≫ g = 0
[PROOFSTEP]
simpa using comm'
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
X : C
p' : X ⟶ ((fun g_1 => app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom
this : a'.hom ≫ g = 0
⊢ pseudoApply g (Quot.mk (PseudoEqual P) (Over.mk a'')) = pseudoApply g (Quotient.mk (setoid P) a)
[PROOFSTEP]
apply Quotient.sound
[GOAL]
case intro.intro.intro.intro.intro.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
X : C
p' : X ⟶ ((fun g_1 => app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom
this : a'.hom ≫ g = 0
⊢ (fun g_1 => app g g_1) (Over.mk a'') ≈ (fun g_1 => app g g_1) a
[PROOFSTEP]
change app g (a'' : Over P) ≈ app g a
[GOAL]
case intro.intro.intro.intro.intro.a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
X : C
p' : X ⟶ ((fun g_1 => app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom
this : a'.hom ≫ g = 0
⊢ app g (Over.mk a'') ≈ app g a
[PROOFSTEP]
exact ⟨R, 𝟙 R, p, inferInstance, ep, by simp [sub_eq_add_neg, this]⟩
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
x y : Pseudoelement P
a a' : Over P
h : pseudoApply f (Quotient.mk (setoid P) a) = pseudoApply f (Quotient.mk (setoid P) a')
R : C
p : R ⟶ ((fun g => app f g) a).left
q : R ⟶ ((fun g => app f g) a').left
ep : Epi p
w✝¹ : Epi q
comm : p ≫ ((fun g => app f g) a).hom = q ≫ ((fun g => app f g) a').hom
a'' : R ⟶ P := p ≫ a.hom - q ≫ a'.hom
Z : C
g : P ⟶ Z
hh : pseudoApply g (Quotient.mk (setoid P) a') = 0
X : C
p' : X ⟶ ((fun g_1 => app g g_1) a').left
q' : X ⟶ (Over.mk 0).left
ep' : Epi p'
w✝ : Epi q'
comm' : p' ≫ ((fun g_1 => app g g_1) a').hom = q' ≫ (Over.mk 0).hom
this : a'.hom ≫ g = 0
⊢ 𝟙 R ≫ (app g (Over.mk a'')).hom = p ≫ (app g a).hom
[PROOFSTEP]
simp [sub_eq_add_neg, this]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
[PROOFSTEP]
obtain ⟨Z, a, b, ea, eb, comm⟩ := Quotient.exact h
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
[PROOFSTEP]
obtain ⟨l, hl₁, hl₂⟩ :=
  @pullback.lift' _ _ _ _ _ _ f g _ (a ≫ x.hom) (b ≫ y.hom)
    (by
      simp only [Category.assoc]
      exact comm)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ (a ≫ x.hom) ≫ f = (b ≫ y.hom) ≫ g
[PROOFSTEP]
simp only [Category.assoc]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
⊢ a ≫ x.hom ≫ f = b ≫ y.hom ≫ g
[PROOFSTEP]
exact comm
[GOAL]
case intro.intro.intro.intro.intro.mk.intro
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst = a ≫ x.hom
hl₂ : l ≫ pullback.snd = b ≫ y.hom
⊢ ∃ s, pseudoApply pullback.fst s = Quotient.mk (setoid P) x ∧ pseudoApply pullback.snd s = Quotient.mk (setoid Q) y
[PROOFSTEP]
exact
  ⟨l,
    ⟨Quotient.sound ⟨Z, 𝟙 Z, a, inferInstance, ea, by rwa [Category.id_comp]⟩,
      Quotient.sound ⟨Z, 𝟙 Z, b, inferInstance, eb, by rwa [Category.id_comp]⟩⟩⟩
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst = a ≫ x.hom
hl₂ : l ≫ pullback.snd = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 => app pullback.fst g_1) (Over.mk l)).hom = a ≫ x.hom
[PROOFSTEP]
rwa [Category.id_comp]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasPullbacks C
P Q R : C
f : P ⟶ R
g : Q ⟶ R
p : Pseudoelement P
q : Pseudoelement Q
x : Over P
y : Over Q
h : pseudoApply f (Quotient.mk (setoid P) x) = pseudoApply g (Quotient.mk (setoid Q) y)
Z : C
a : Z ⟶ ((fun g => app f g) x).left
b : Z ⟶ ((fun g_1 => app g g_1) y).left
ea : Epi a
eb : Epi b
comm : a ≫ ((fun g => app f g) x).hom = b ≫ ((fun g_1 => app g g_1) y).hom
l : Z ⟶ pullback f g
hl₁ : l ≫ pullback.fst = a ≫ x.hom
hl₂ : l ≫ pullback.snd = b ≫ y.hom
⊢ 𝟙 Z ≫ ((fun g_1 => app pullback.snd g_1) (Over.mk l)).hom = b ≫ y.hom
[PROOFSTEP]
rwa [Category.id_comp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
h : PseudoEqual G x y
⊢ LinearMap.range x.hom = LinearMap.range y.hom
[PROOFSTEP]
obtain ⟨P, p, q, hp, hq, H⟩ := h
[GOAL]
case intro.intro.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
⊢ LinearMap.range x.hom = LinearMap.range y.hom
[PROOFSTEP]
refine' Submodule.ext fun a => ⟨fun ha => _, fun ha => _⟩
[GOAL]
case intro.intro.intro.intro.intro.refine'_1
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
ha : a ∈ LinearMap.range x.hom
⊢ a ∈ LinearMap.range y.hom
[PROOFSTEP]
obtain ⟨a', ha'⟩ := ha
[GOAL]
case intro.intro.intro.intro.intro.refine'_1.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : ↑x.hom a' = a
⊢ a ∈ LinearMap.range y.hom
[PROOFSTEP]
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective p).1 hp a'
[GOAL]
case intro.intro.intro.intro.intro.refine'_1.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : ↑x.hom a' = a
a'' : ↑P
ha'' : ↑p a'' = a'
⊢ a ∈ LinearMap.range y.hom
[PROOFSTEP]
refine' ⟨q a'', _⟩
[GOAL]
case intro.intro.intro.intro.intro.refine'_1.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj x.left)
ha' : ↑x.hom a' = a
a'' : ↑P
ha'' : ↑p a'' = a'
⊢ ↑y.hom (↑q a'') = a
[PROOFSTEP]
rw [← LinearMap.comp_apply, ← ModuleCat.comp_def, ← H, ModuleCat.comp_def, LinearMap.comp_apply, ha'', ha']
[GOAL]
case intro.intro.intro.intro.intro.refine'_2
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
ha : a ∈ LinearMap.range y.hom
⊢ a ∈ LinearMap.range x.hom
[PROOFSTEP]
obtain ⟨a', ha'⟩ := ha
[GOAL]
case intro.intro.intro.intro.intro.refine'_2.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : ↑y.hom a' = a
⊢ a ∈ LinearMap.range x.hom
[PROOFSTEP]
obtain ⟨a'', ha''⟩ := (ModuleCat.epi_iff_surjective q).1 hq a'
[GOAL]
case intro.intro.intro.intro.intro.refine'_2.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : ↑y.hom a' = a
a'' : ↑P
ha'' : ↑q a'' = a'
⊢ a ∈ LinearMap.range x.hom
[PROOFSTEP]
refine' ⟨p a'', _⟩
[GOAL]
case intro.intro.intro.intro.intro.refine'_2.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
inst✝¹ : HasPullbacks C
R : Type u_1
inst✝ : CommRing R
G : ModuleCat R
x y : Over G
P : ModuleCat R
p : P ⟶ x.left
q : P ⟶ y.left
hp : Epi p
hq : Epi q
H : p ≫ x.hom = q ≫ y.hom
a : ↑((Functor.fromPUnit G).obj x.right)
a' : ↑((𝟭 (ModuleCat R)).obj y.left)
ha' : ↑y.hom a' = a
a'' : ↑P
ha'' : ↑q a'' = a'
⊢ ↑x.hom (↑p a'') = a
[PROOFSTEP]
rw [← LinearMap.comp_apply, ← ModuleCat.comp_def, H, ModuleCat.comp_def, LinearMap.comp_apply, ha'', ha']


[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
⊢ f = g
[PROOFSTEP]
apply @Faithful.map_injective C _ (Type w) _ (forget C) _ X Y
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
⊢ (forget C).map f = (forget C).map g
[PROOFSTEP]
dsimp [forget]
[GOAL]
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
⊢ ConcreteCategory.forget.map f = ConcreteCategory.forget.map g
[PROOFSTEP]
funext x
[GOAL]
case a.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ConcreteCategory C
X Y : C
f g : X ⟶ Y
w : ∀ (x : (forget C).obj X), ↑f x = ↑g x
x : ConcreteCategory.forget.obj X
⊢ ConcreteCategory.forget.map f x = ConcreteCategory.forget.map g x
[PROOFSTEP]
exact w x
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ConcreteCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ Function.Bijective ((forget C).map f)
[PROOFSTEP]
rw [← isIso_iff_bijective]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ConcreteCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ IsIso ((forget C).map f)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesMonomorphisms (forget C)
⊢ Functor.PreservesMonomorphisms (forget₂ C D ⋙ forget D)
[PROOFSTEP]
simp only [HasForget₂.forget_comp]
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesMonomorphisms (forget C)
⊢ Functor.PreservesMonomorphisms (forget C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesEpimorphisms (forget C)
⊢ Functor.PreservesEpimorphisms (forget₂ C D ⋙ forget D)
[PROOFSTEP]
simp only [HasForget₂.forget_comp]
[GOAL]
C : Type u
D : Type u'
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
inst✝³ : Category.{v', u'} D
inst✝² : ConcreteCategory D
inst✝¹ : HasForget₂ C D
inst✝ : Functor.PreservesEpimorphisms (forget C)
⊢ Functor.PreservesEpimorphisms (forget C)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
D : Type u'
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
inst✝¹ : Category.{v', u'} D
inst✝ : ConcreteCategory D
obj : C → D
h_obj : ∀ (X : C), (forget D).obj (obj X) = (forget C).obj X
map : {X Y : C} → (X ⟶ Y) → (obj X ⟶ obj Y)
h_map : ∀ {X Y : C} {f : X ⟶ Y}, HEq ((forget D).map (map f)) ((forget C).map f)
⊢ Faithful.div (forget C) (forget D) (fun X => obj X) h_obj (fun X Y f => map f) h_map ⋙ forget D = forget C
[PROOFSTEP]
apply Faithful.div_comp