C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
⊢ Epi f
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
⊢ Function.Surjective (pseudoApply f) → Epi f
intro h
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : Function.Surjective (pseudoApply f)
⊢ Epi f
have ⟨pbar, hpbar⟩ := h (𝟙 Q)
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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
have ⟨p, hp⟩ := Quotient.exists_rep pbar
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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
have : ⟦(p.hom ≫ f : Over Q)⟧ = ⟦↑(𝟙 Q)⟧ := by
  rw [← hp] at hpbar
  exact hpbar
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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
have ⟨R, x, y, _, ey, comm⟩ := Quotient.exact this
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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
apply @epi_of_epi_fac _ _ _ _ _ (x ≫ p.hom) f y ey
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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
dsimp at comm
C : Type u
inst✝¹ : Category 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
C : Type u
inst✝¹ : Category 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
rw [Category.assoc, comm]
no goals
C : Type u
inst✝¹ : Category 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
apply Category.comp_id
C : Type u
inst✝¹ : Category 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.445621 hp) (Over.mk (p.hom ≫ f)) = Quotient.mk (?m.445621 hp) (Over.mk (𝟙 Q))
C : Type u
inst✝¹ : Category 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.415411 (Over.mk (p.hom ≫ f)) = Quotient.mk ?m.415411 (Over.mk (𝟙 Q))
rw [← hp] at hpbar
no goals
C : Type u
inst✝¹ : Category 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.445621 hp) (Over.mk (p.hom ≫ f)) = Quotient.mk (?m.445621 hp) (Over.mk (𝟙 Q))
exact hpbar