[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
⊢ IsSeparating (Set.op 𝒢) ↔ IsCoseparating 𝒢
[PROOFSTEP]
refine' ⟨fun h𝒢 X Y f g hfg => _, fun h𝒢 X Y f g hfg => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsSeparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
[PROOFSTEP]
refine' Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj _)
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsSeparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : G ⟶ op Y
⊢ (h ≫ f.op).unop = (h ≫ g.op).unop
[PROOFSTEP]
simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj _)
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : X.unop ⟶ G
⊢ (f.unop ≫ h).op = (g.unop ≫ h).op
[PROOFSTEP]
simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
⊢ IsCoseparating (Set.op 𝒢) ↔ IsSeparating 𝒢
[PROOFSTEP]
refine' ⟨fun h𝒢 X Y f g hfg => _, fun h𝒢 X Y f g hfg => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCoseparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
[PROOFSTEP]
refine' Quiver.Hom.op_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.unop_inj _)
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCoseparating (Set.op 𝒢)
X Y : C
f g : X ⟶ Y
hfg : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : op X ⟶ G
⊢ (f.op ≫ h).unop = (g.op ≫ h).unop
[PROOFSTEP]
simpa only [unop_comp, Quiver.Hom.unop_op] using hfg _ (Set.mem_op.1 hG) _
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
[PROOFSTEP]
refine' Quiver.Hom.unop_inj (h𝒢 _ _ fun G hG h => Quiver.Hom.op_inj _)
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : Cᵒᵖ
f g : X ⟶ Y
hfg : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : G ∈ 𝒢
h : G ⟶ Y.unop
⊢ (h ≫ f.unop).op = (h ≫ g.unop).op
[PROOFSTEP]
simpa only [op_comp, Quiver.Hom.op_unop] using hfg _ (Set.op_mem_op.2 hG) _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set Cᵒᵖ
⊢ IsCoseparating (Set.unop 𝒢) ↔ IsSeparating 𝒢
[PROOFSTEP]
rw [← isSeparating_op_iff, Set.unop_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set Cᵒᵖ
⊢ IsSeparating (Set.unop 𝒢) ↔ IsCoseparating 𝒢
[PROOFSTEP]
rw [← isCoseparating_op_iff, Set.unop_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
⊢ IsDetecting (Set.op 𝒢) ↔ IsCodetecting 𝒢
[PROOFSTEP]
refine' ⟨fun h𝒢 X Y f hf => _, fun h𝒢 X Y f hf => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
[PROOFSTEP]
refine' (isIso_op_iff _).1 (h𝒢 _ fun G hG h => _)
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : G ⟶ op X
⊢ ∃! h', h' ≫ f.op = h
[PROOFSTEP]
obtain ⟨t, ht, ht'⟩ := hf (unop G) (Set.mem_op.1 hG) h.unop
[GOAL]
case refine'_1.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : G ⟶ op X
t : Y ⟶ G.unop
ht : f ≫ t = h.unop
ht' : ∀ (y : Y ⟶ G.unop), (fun h' => f ≫ h' = h.unop) y → y = t
⊢ ∃! h', h' ≫ f.op = h
[PROOFSTEP]
exact ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
[PROOFSTEP]
refine' (isIso_unop_iff _).1 (h𝒢 _ fun G hG h => _)
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : Y.unop ⟶ G
⊢ ∃! h', f.unop ≫ h' = h
[PROOFSTEP]
obtain ⟨t, ht, ht'⟩ := hf (op G) (Set.op_mem_op.2 hG) h.op
[GOAL]
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : Y.unop ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
⊢ ∃! h', f.unop ≫ h' = h
[PROOFSTEP]
refine' ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ _)⟩
[GOAL]
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : Y.unop ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
y : X.unop ⟶ G
hy : (fun h' => f.unop ≫ h' = h) y
⊢ (fun h' => h' ≫ f = h.op) y.op
[PROOFSTEP]
exact Quiver.Hom.unop_inj (by simpa only using hy)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : C
hG : G ∈ 𝒢
h : Y.unop ⟶ G
t : op G ⟶ X
ht : t ≫ f = h.op
ht' : ∀ (y : op G ⟶ X), (fun h' => h' ≫ f = h.op) y → y = t
y : X.unop ⟶ G
hy : (fun h' => f.unop ≫ h' = h) y
⊢ (y.op ≫ f).unop = h.op.unop
[PROOFSTEP]
simpa only using hy
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
⊢ IsCodetecting (Set.op 𝒢) ↔ IsDetecting 𝒢
[PROOFSTEP]
refine' ⟨fun h𝒢 X Y f hf => _, fun h𝒢 X Y f hf => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
[PROOFSTEP]
refine' (isIso_op_iff _).1 (h𝒢 _ fun G hG h => _)
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : op Y ⟶ G
⊢ ∃! h', f.op ≫ h' = h
[PROOFSTEP]
obtain ⟨t, ht, ht'⟩ := hf (unop G) (Set.mem_op.1 hG) h.unop
[GOAL]
case refine'_1.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsCodetecting (Set.op 𝒢)
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
G : Cᵒᵖ
hG : G ∈ Set.op 𝒢
h : op Y ⟶ G
t : G.unop ⟶ X
ht : t ≫ f = h.unop
ht' : ∀ (y : G.unop ⟶ X), (fun h' => h' ≫ f = h.unop) y → y = t
⊢ ∃! h', f.op ≫ h' = h
[PROOFSTEP]
exact ⟨t.op, Quiver.Hom.unop_inj ht, fun y hy => Quiver.Hom.unop_inj (ht' _ (Quiver.Hom.op_inj hy))⟩
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
[PROOFSTEP]
refine' (isIso_unop_iff _).1 (h𝒢 _ fun G hG h => _)
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
⊢ ∃! h', h' ≫ f.unop = h
[PROOFSTEP]
obtain ⟨t, ht, ht'⟩ := hf (op G) (Set.op_mem_op.2 hG) h.op
[GOAL]
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' => f ≫ h' = h.op) y → y = t
⊢ ∃! h', h' ≫ f.unop = h
[PROOFSTEP]
refine' ⟨t.unop, Quiver.Hom.op_inj ht, fun y hy => Quiver.Hom.op_inj (ht' _ _)⟩
[GOAL]
case refine'_2.intro.intro
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' => f ≫ h' = h.op) y → y = t
y : G ⟶ Y.unop
hy : (fun h' => h' ≫ f.unop = h) y
⊢ (fun h' => f ≫ h' = h.op) y.op
[PROOFSTEP]
exact Quiver.Hom.unop_inj (by simpa only using hy)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X Y : Cᵒᵖ
f : X ⟶ Y
hf : ∀ (G : Cᵒᵖ), G ∈ Set.op 𝒢 → ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
G : C
hG : G ∈ 𝒢
h : G ⟶ X.unop
t : Y ⟶ op G
ht : f ≫ t = h.op
ht' : ∀ (y : Y ⟶ op G), (fun h' => f ≫ h' = h.op) y → y = t
y : G ⟶ Y.unop
hy : (fun h' => h' ≫ f.unop = h) y
⊢ (f ≫ y.op).unop = h.op.unop
[PROOFSTEP]
simpa only using hy
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set Cᵒᵖ
⊢ IsDetecting (Set.unop 𝒢) ↔ IsCodetecting 𝒢
[PROOFSTEP]
rw [← isCodetecting_op_iff, Set.unop_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set Cᵒᵖ
⊢ IsCodetecting (Set.unop 𝒢) ↔ IsDetecting 𝒢
[PROOFSTEP]
rw [← isDetecting_op_iff, Set.unop_op]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : HasCoequalizers C
𝒢 : Set C
⊢ IsCodetecting 𝒢 → IsCoseparating 𝒢
[PROOFSTEP]
simpa only [← isSeparating_op_iff, ← isDetecting_op_iff] using IsDetecting.isSeparating
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
⊢ IsDetecting 𝒢
[PROOFSTEP]
intro X Y f hf
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
[PROOFSTEP]
refine' (isIso_iff_mono_and_epi _).2 ⟨⟨fun g h hgh => h𝒢 _ _ fun G hG i => _⟩, ⟨fun g h hgh => _⟩⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : G ∈ 𝒢
i : G ⟶ Z✝
⊢ i ≫ g = i ≫ h
[PROOFSTEP]
obtain ⟨t, -, ht⟩ := hf G hG (i ≫ g ≫ f)
[GOAL]
case refine'_1.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Z✝ ⟶ X
hgh : g ≫ f = h ≫ f
G : C
hG : G ∈ 𝒢
i : G ⟶ Z✝
t : G ⟶ X
ht : ∀ (y : G ⟶ X), (fun h' => h' ≫ f = i ≫ g ≫ f) y → y = t
⊢ i ≫ g = i ≫ h
[PROOFSTEP]
rw [ht (i ≫ g) (Category.assoc _ _ _), ht (i ≫ h) (hgh.symm ▸ Category.assoc _ _ _)]
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
⊢ g = h
[PROOFSTEP]
refine' h𝒢 _ _ fun G hG i => _
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : G ∈ 𝒢
i : G ⟶ Y
⊢ i ≫ g = i ≫ h
[PROOFSTEP]
obtain ⟨t, rfl, -⟩ := hf G hG i
[GOAL]
case refine'_2.intro.intro
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : C
f : X ⟶ Y
hf : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
Z✝ : C
g h : Y ⟶ Z✝
hgh : f ≫ g = f ≫ h
G : C
hG : G ∈ 𝒢
t : G ⟶ X
⊢ (t ≫ f) ≫ g = (t ≫ f) ≫ h
[PROOFSTEP]
rw [Category.assoc, hgh, Category.assoc]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Balanced C
𝒢 : Set C
⊢ IsCoseparating 𝒢 → IsCodetecting 𝒢
[PROOFSTEP]
simpa only [← isDetecting_op_iff, ← isSeparating_op_iff] using IsSeparating.isDetecting
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
⊢ IsSeparating 𝒢 ↔ ∀ (A : C), Epi (Sigma.desc Sigma.snd)
[PROOFSTEP]
refine' ⟨fun h A => ⟨fun u v huv => h _ _ fun G hG f => _⟩, fun h X Y f g hh => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : IsSeparating 𝒢
A Z✝ : C
u v : A ⟶ Z✝
huv : Sigma.desc Sigma.snd ≫ u = Sigma.desc Sigma.snd ≫ v
G : C
hG : G ∈ 𝒢
f : G ⟶ A
⊢ f ≫ u = f ≫ v
[PROOFSTEP]
simpa using Sigma.ι (fun f : Σ G : 𝒢, (G : C) ⟶ A => (f.1 : C)) ⟨⟨G, hG⟩, f⟩ ≫= huv
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : ∀ (A : C), Epi (Sigma.desc Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
[PROOFSTEP]
haveI := h X
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : ∀ (A : C), Epi (Sigma.desc Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc Sigma.snd)
⊢ f = g
[PROOFSTEP]
refine' (cancel_epi (Sigma.desc (@Sigma.snd 𝒢 fun G => (G : C) ⟶ X))).1 (colimit.hom_ext fun j => _)
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasCoproduct fun f => ↑f.fst
h : ∀ (A : C), Epi (Sigma.desc Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ (G : C), G ∈ 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc Sigma.snd)
j : Discrete ((G : ↑𝒢) × (↑G ⟶ X))
⊢ colimit.ι (Discrete.functor fun b => ↑b.fst) j ≫ Sigma.desc Sigma.snd ≫ f =
    colimit.ι (Discrete.functor fun b => ↑b.fst) j ≫ Sigma.desc Sigma.snd ≫ g
[PROOFSTEP]
simpa using hh j.as.1.1 j.as.1.2 j.as.2
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasProduct fun f => ↑f.fst
⊢ IsCoseparating 𝒢 ↔ ∀ (A : C), Mono (Pi.lift Sigma.snd)
[PROOFSTEP]
refine' ⟨fun h A => ⟨fun u v huv => h _ _ fun G hG f => _⟩, fun h X Y f g hh => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasProduct fun f => ↑f.fst
h : IsCoseparating 𝒢
A Z✝ : C
u v : Z✝ ⟶ A
huv : u ≫ Pi.lift Sigma.snd = v ≫ Pi.lift Sigma.snd
G : C
hG : G ∈ 𝒢
f : A ⟶ G
⊢ u ≫ f = v ≫ f
[PROOFSTEP]
simpa using huv =≫ Pi.π (fun f : Σ G : 𝒢, A ⟶ (G : C) => (f.1 : C)) ⟨⟨G, hG⟩, f⟩
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasProduct fun f => ↑f.fst
h : ∀ (A : C), Mono (Pi.lift Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
[PROOFSTEP]
haveI := h Y
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasProduct fun f => ↑f.fst
h : ∀ (A : C), Mono (Pi.lift Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift Sigma.snd)
⊢ f = g
[PROOFSTEP]
refine' (cancel_mono (Pi.lift (@Sigma.snd 𝒢 fun G => Y ⟶ (G : C)))).1 (limit.hom_ext fun j => _)
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
𝒢 : Set C
inst✝ : ∀ (A : C), HasProduct fun f => ↑f.fst
h : ∀ (A : C), Mono (Pi.lift Sigma.snd)
X Y : C
f g : X ⟶ Y
hh : ∀ (G : C), G ∈ 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift Sigma.snd)
j : Discrete ((G : ↑𝒢) × (Y ⟶ ↑G))
⊢ (f ≫ Pi.lift Sigma.snd) ≫ limit.π (Discrete.functor fun b => ↑b.fst) j =
    (g ≫ Pi.lift Sigma.snd) ≫ limit.π (Discrete.functor fun b => ↑b.fst) j
[PROOFSTEP]
simpa using hh j.as.1.1 j.as.1.2 j.as.2
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
⊢ HasInitial C
[PROOFSTEP]
haveI : HasProductsOfShape 𝒢 C := hasProductsOfShape_of_small C 𝒢
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this : HasProductsOfShape (↑𝒢) C
⊢ HasInitial C
[PROOFSTEP]
haveI := fun A => hasProductsOfShape_of_small.{v₁} C (Σ G : 𝒢, A ⟶ (G : C))
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝ : HasProductsOfShape (↑𝒢) C
this : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
⊢ HasInitial C
[PROOFSTEP]
letI := completeLatticeOfCompleteSemilatticeInf (Subobject (piObj (Subtype.val : 𝒢 → C)))
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
⊢ HasInitial C
[PROOFSTEP]
suffices ∀ A : C, Unique (((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C) ⟶ A) by
  exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
this : (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
⊢ HasInitial C
[PROOFSTEP]
exact hasInitial_of_unique ((⊥ : Subobject (piObj (Subtype.val : 𝒢 → C))) : C)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
⊢ (A : C) → Unique (Subobject.underlying.obj ⊥ ⟶ A)
[PROOFSTEP]
refine' fun A => ⟨⟨_⟩, fun f => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
⊢ Subobject.underlying.obj ⊥ ⟶ A
[PROOFSTEP]
let s := Pi.lift fun f : Σ G : 𝒢, A ⟶ (G : C) => id (Pi.π (Subtype.val : 𝒢 → C)) f.1
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
⊢ Subobject.underlying.obj ⊥ ⟶ A
[PROOFSTEP]
let t := Pi.lift (@Sigma.snd 𝒢 fun G => A ⟶ (G : C))
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
t : A ⟶ ∏ fun b => ↑b.fst := Pi.lift Sigma.snd
⊢ Subobject.underlying.obj ⊥ ⟶ A
[PROOFSTEP]
haveI : Mono t := (isCoseparating_iff_mono 𝒢).1 h𝒢 A
[GOAL]
case refine'_1
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
s : ∏ Subtype.val ⟶ ∏ fun f => ↑f.fst := Pi.lift fun f => id (Pi.π Subtype.val) f.fst
t : A ⟶ ∏ fun b => ↑b.fst := Pi.lift Sigma.snd
this : Mono t
⊢ Subobject.underlying.obj ⊥ ⟶ A
[PROOFSTEP]
exact Subobject.ofLEMk _ (pullback.fst : pullback s t ⟶ _) bot_le ≫ pullback.snd
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = default
[PROOFSTEP]
suffices ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g by apply this
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
this : ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
⊢ f = default
[PROOFSTEP]
apply this
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
⊢ ∀ (g : Subobject.underlying.obj ⊥ ⟶ A), f = g
[PROOFSTEP]
intro g
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ f = g
[PROOFSTEP]
suffices IsSplitEpi (equalizer.ι f g) by exact eq_of_epi_equalizer
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝² : HasProductsOfShape (↑𝒢) C
this✝¹ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this✝ : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
this : IsSplitEpi (equalizer.ι f g)
⊢ f = g
[PROOFSTEP]
exact eq_of_epi_equalizer
[GOAL]
case refine'_2
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ IsSplitEpi (equalizer.ι f g)
[PROOFSTEP]
exact
  IsSplitEpi.mk'
    ⟨Subobject.ofLEMk _ (equalizer.ι f g ≫ Subobject.arrow _) bot_le,
      by
      ext
      simp⟩
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
⊢ Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥)
        (_ : ⊥ ≤ Subobject.mk (equalizer.ι f g ≫ Subobject.arrow ⊥)) ≫
      equalizer.ι f g =
    𝟙 (Subobject.underlying.obj ⊥)
[PROOFSTEP]
ext
[GOAL]
case h.h
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered C
inst✝¹ : HasLimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsCoseparating 𝒢
this✝¹ : HasProductsOfShape (↑𝒢) C
this✝ : ∀ (A : C), HasProductsOfShape ((G : ↑𝒢) × (A ⟶ ↑G)) C
this : CompleteLattice (Subobject (∏ Subtype.val)) :=
  completeLatticeOfCompleteSemilatticeInf (Subobject (∏ Subtype.val))
A : C
f : Subobject.underlying.obj ⊥ ⟶ A
g : Subobject.underlying.obj ⊥ ⟶ A
b✝ : { x // x ∈ 𝒢 }
⊢ ((Subobject.ofLEMk ⊥ (equalizer.ι f g ≫ Subobject.arrow ⊥)
            (_ : ⊥ ≤ Subobject.mk (equalizer.ι f g ≫ Subobject.arrow ⊥)) ≫
          equalizer.ι f g) ≫
        Subobject.arrow ⊥) ≫
      Pi.π Subtype.val b✝ =
    (𝟙 (Subobject.underlying.obj ⊥) ≫ Subobject.arrow ⊥) ≫ Pi.π Subtype.val b✝
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
⊢ HasTerminal C
[PROOFSTEP]
haveI : Small.{v₁} 𝒢.op := small_of_injective (Set.opEquiv_self 𝒢).injective
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
this : Small.{v₁, u₁} ↑(Set.op 𝒢)
⊢ HasTerminal C
[PROOFSTEP]
haveI : HasInitial Cᵒᵖ := hasInitial_of_isCoseparating ((isCoseparating_op_iff _).2 h𝒢)
[GOAL]
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
inst✝² : WellPowered Cᵒᵖ
inst✝¹ : HasColimits C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsSeparating 𝒢
this✝ : Small.{v₁, u₁} ↑(Set.op 𝒢)
this : HasInitial Cᵒᵖ
⊢ HasTerminal C
[PROOFSTEP]
exact hasTerminal_of_hasInitial_op
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
⊢ P = Q
[PROOFSTEP]
suffices IsIso (ofLE _ _ h₁) by exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
this : IsIso (ofLE P Q h₁)
⊢ P = Q
[PROOFSTEP]
exact le_antisymm h₁ (le_of_comm (inv (ofLE _ _ h₁)) (by simp))
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
this : IsIso (ofLE P Q h₁)
⊢ inv (ofLE P Q h₁) ≫ arrow P = arrow Q
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
⊢ IsIso (ofLE P Q h₁)
[PROOFSTEP]
refine' h𝒢 _ fun G hG f => _
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
⊢ ∃! h', h' ≫ ofLE P Q h₁ = f
[PROOFSTEP]
have : P.Factors (f ≫ Q.arrow) := h₂ _ hG ((factors_iff _ _).2 ⟨_, rfl⟩)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
⊢ ∃! h', h' ≫ ofLE P Q h₁ = f
[PROOFSTEP]
refine' ⟨factorThru _ _ this, _, fun g (hg : g ≫ _ = f) => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
⊢ (fun h' => h' ≫ ofLE P Q h₁ = f) (factorThru P (f ≫ arrow Q) this)
[PROOFSTEP]
simp only [← cancel_mono Q.arrow, Category.assoc, ofLE_arrow, factorThru_arrow]
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
𝒢 : Set C
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h₁ : P ≤ Q
h₂ : ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Factors Q f → Factors P f
G : C
hG : G ∈ 𝒢
f : G ⟶ underlying.obj Q
this : Factors P (f ≫ arrow Q)
g : G ⟶ underlying.obj P
hg : g ≫ ofLE P Q h₁ = f
⊢ g = factorThru P (f ≫ arrow Q) this
[PROOFSTEP]
simp only [← cancel_mono (Subobject.ofLE _ _ h₁), ← cancel_mono Q.arrow, hg, Category.assoc, ofLE_arrow,
  factorThru_arrow]
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasPullbacks C
𝒢 : Set C
inst✝ : Small.{v₁, u₁} ↑𝒢
h𝒢 : IsDetecting 𝒢
X : C
P Q : Subobject X
h : (fun P => {f | Subobject.Factors P f.snd}) P = (fun P => {f | Subobject.Factors P f.snd}) Q
⊢ ∀ (G : C), G ∈ 𝒢 → ∀ {f : G ⟶ X}, Subobject.Factors P f ↔ Subobject.Factors Q f
[PROOFSTEP]
simpa [Set.ext_iff] using h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
⊢ IsCoseparating ((proj S T).toPrefunctor.obj ⁻¹' 𝒢)
[PROOFSTEP]
refine' fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
𝒢 : Set C
h𝒢 : IsCoseparating 𝒢
X Y : StructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : StructuredArrow S T), G ∈ (proj S T).toPrefunctor.obj ⁻¹' 𝒢 → ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
G : C
hG : G ∈ 𝒢
h : Y.right ⟶ G
⊢ f.right ≫ h = g.right ≫ h
[PROOFSTEP]
exact congr_arg CommaMorphism.right (hfg (mk (Y.hom ≫ T.map h)) hG (homMk h rfl))
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
⊢ IsSeparating ((proj S T).toPrefunctor.obj ⁻¹' 𝒢)
[PROOFSTEP]
refine' fun X Y f g hfg => ext _ _ (h𝒢 _ _ fun G hG h => _)
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : C ⥤ D
T : D
𝒢 : Set C
h𝒢 : IsSeparating 𝒢
X Y : CostructuredArrow S T
f g : X ⟶ Y
hfg : ∀ (G : CostructuredArrow S T), G ∈ (proj S T).toPrefunctor.obj ⁻¹' 𝒢 → ∀ (h : G ⟶ X), h ≫ f = h ≫ g
G : C
hG : G ∈ 𝒢
h : G ⟶ X.left
⊢ h ≫ f.left = h ≫ g.left
[PROOFSTEP]
exact congr_arg CommaMorphism.left (hfg (mk (S.map h ≫ X.hom)) hG (homMk h rfl))
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
⊢ IsSeparator (op G) ↔ IsCoseparator G
[PROOFSTEP]
rw [IsSeparator, IsCoseparator, ← isSeparating_op_iff, Set.singleton_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
⊢ IsCoseparator (op G) ↔ IsSeparator G
[PROOFSTEP]
rw [IsSeparator, IsCoseparator, ← isCoseparating_op_iff, Set.singleton_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : Cᵒᵖ
⊢ IsCoseparator G.unop ↔ IsSeparator G
[PROOFSTEP]
rw [IsSeparator, IsCoseparator, ← isCoseparating_unop_iff, Set.singleton_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : Cᵒᵖ
⊢ IsSeparator G.unop ↔ IsCoseparator G
[PROOFSTEP]
rw [IsSeparator, IsCoseparator, ← isSeparating_unop_iff, Set.singleton_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
⊢ IsDetector (op G) ↔ IsCodetector G
[PROOFSTEP]
rw [IsDetector, IsCodetector, ← isDetecting_op_iff, Set.singleton_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
⊢ IsCodetector (op G) ↔ IsDetector G
[PROOFSTEP]
rw [IsDetector, IsCodetector, ← isCodetecting_op_iff, Set.singleton_op]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : Cᵒᵖ
⊢ IsCodetector G.unop ↔ IsDetector G
[PROOFSTEP]
rw [IsDetector, IsCodetector, ← isCodetecting_unop_iff, Set.singleton_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : Cᵒᵖ
⊢ IsDetector G.unop ↔ IsCodetector G
[PROOFSTEP]
rw [IsDetector, IsCodetector, ← isDetecting_unop_iff, Set.singleton_unop]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsSeparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
H : C
hH : H ∈ {G}
h : H ⟶ X
⊢ h ≫ f = h ≫ g
[PROOFSTEP]
obtain rfl := Set.mem_singleton_iff.1 hH
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f g : X ⟶ Y
H : C
h : H ⟶ X
hG : IsSeparator H
hfg : ∀ (h : H ⟶ X), h ≫ f = h ≫ g
hH : H ∈ {H}
⊢ h ≫ f = h ≫ g
[PROOFSTEP]
exact hfg h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsCoseparator G
X Y : C
f g : X ⟶ Y
hfg : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
H : C
hH : H ∈ {G}
h : Y ⟶ H
⊢ f ≫ h = g ≫ h
[PROOFSTEP]
obtain rfl := Set.mem_singleton_iff.1 hH
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f g : X ⟶ Y
H : C
h : Y ⟶ H
hG : IsCoseparator H
hfg : ∀ (h : Y ⟶ H), f ≫ h = g ≫ h
hH : H ∈ {H}
⊢ f ≫ h = g ≫ h
[PROOFSTEP]
exact hfg h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsDetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
H : C
hH : H ∈ {G}
h : H ⟶ Y
⊢ ∃! h', h' ≫ f = h
[PROOFSTEP]
obtain rfl := Set.mem_singleton_iff.1 hH
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
H : C
h : H ⟶ Y
hG : IsDetector H
hf : ∀ (h : H ⟶ Y), ∃! h', h' ≫ f = h
hH : H ∈ {H}
⊢ ∃! h', h' ≫ f = h
[PROOFSTEP]
exact hf h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsCodetector G
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
H : C
hH : H ∈ {G}
h : X ⟶ H
⊢ ∃! h', f ≫ h' = h
[PROOFSTEP]
obtain rfl := Set.mem_singleton_iff.1 hH
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y : C
f : X ⟶ Y
H : C
h : X ⟶ H
hG : IsCodetector H
hf : ∀ (h : X ⟶ H), ∃! h', f ≫ h' = h
hH : H ∈ {H}
⊢ ∃! h', f ≫ h' = h
[PROOFSTEP]
exact hf h
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
⊢ IsSeparator G ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)
[PROOFSTEP]
rw [isSeparator_def]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g) ↔ ∀ (A : C), Epi (Sigma.desc fun f => f)
[PROOFSTEP]
refine' ⟨fun h A => ⟨fun u v huv => h _ _ fun i => _⟩, fun h X Y f g hh => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : G ⟶ X), h ≫ f = h ≫ g) → f = g
A Z✝ : C
u v : A ⟶ Z✝
huv : (Sigma.desc fun f => f) ≫ u = (Sigma.desc fun f => f) ≫ v
i : G ⟶ A
⊢ i ≫ u = i ≫ v
[PROOFSTEP]
simpa using Sigma.ι _ i ≫= huv
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
⊢ f = g
[PROOFSTEP]
haveI := h X
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f => f)
⊢ f = g
[PROOFSTEP]
refine' (cancel_epi (Sigma.desc fun f : G ⟶ X => f)).1 (colimit.hom_ext fun j => _)
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasCoproduct fun x => G
h : ∀ (A : C), Epi (Sigma.desc fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : G ⟶ X), h ≫ f = h ≫ g
this : Epi (Sigma.desc fun f => f)
j : Discrete (G ⟶ X)
⊢ colimit.ι (Discrete.functor fun f => G) j ≫ (Sigma.desc fun f => f) ≫ f =
    colimit.ι (Discrete.functor fun f => G) j ≫ (Sigma.desc fun f => f) ≫ g
[PROOFSTEP]
simpa using hh j.as
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
⊢ IsCoseparator G ↔ ∀ (A : C), Mono (Pi.lift fun f => f)
[PROOFSTEP]
rw [isCoseparator_def]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
⊢ (∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g) ↔ ∀ (A : C), Mono (Pi.lift fun f => f)
[PROOFSTEP]
refine' ⟨fun h A => ⟨fun u v huv => h _ _ fun i => _⟩, fun h X Y f g hh => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ ⦃X Y : C⦄ (f g : X ⟶ Y), (∀ (h : Y ⟶ G), f ≫ h = g ≫ h) → f = g
A Z✝ : C
u v : Z✝ ⟶ A
huv : (u ≫ Pi.lift fun f => f) = v ≫ Pi.lift fun f => f
i : A ⟶ G
⊢ u ≫ i = v ≫ i
[PROOFSTEP]
simpa using huv =≫ Pi.π _ i
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
⊢ f = g
[PROOFSTEP]
haveI := h Y
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f => f)
⊢ f = g
[PROOFSTEP]
refine' (cancel_mono (Pi.lift fun f : Y ⟶ G => f)).1 (limit.hom_ext fun j => _)
[GOAL]
case refine'_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
G : C
inst✝ : ∀ (A : C), HasProduct fun x => G
h : ∀ (A : C), Mono (Pi.lift fun f => f)
X Y : C
f g : X ⟶ Y
hh : ∀ (h : Y ⟶ G), f ≫ h = g ≫ h
this : Mono (Pi.lift fun f => f)
j : Discrete (Y ⟶ G)
⊢ (f ≫ Pi.lift fun f => f) ≫ limit.π (Discrete.functor fun f => G) j =
    (g ≫ Pi.lift fun f => f) ≫ limit.π (Discrete.functor fun f => G) j
[PROOFSTEP]
simpa using hh j.as
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
⊢ IsSeparator (G ⨿ H) ↔ IsSeparating {G, H}
[PROOFSTEP]
refine' ⟨fun h X Y u v huv => _, fun h => (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
⊢ u = v
[PROOFSTEP]
refine' h.def _ _ fun g => coprod.hom_ext _ _
[GOAL]
case refine'_1.refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ coprod.inl ≫ g ≫ u = coprod.inl ≫ g ≫ v
[PROOFSTEP]
simpa using huv G (by simp) (coprod.inl ≫ g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ G ∈ {G, H}
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ coprod.inr ≫ g ≫ u = coprod.inr ≫ g ≫ v
[PROOFSTEP]
simpa using huv H (by simp) (coprod.inr ≫ g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparator (G ⨿ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : G_1 ⟶ X), h ≫ u = h ≫ v
g : G ⨿ H ⟶ X
⊢ H ∈ {G, H}
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : G ⨿ H ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ {G, H}
g : Z ⟶ X
⊢ g ≫ u = g ≫ v
[PROOFSTEP]
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ
[GOAL]
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
h : IsSeparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : G ⨿ H ⟶ X), h ≫ u = h ≫ v
Z : C
g : Z ⟶ X
hZ : Z = G ∨ Z = H
⊢ g ≫ u = g ≫ v
[PROOFSTEP]
rcases hZ with (rfl | rfl)
[GOAL]
case refine'_2.inl
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
H X Y : C
u v : X ⟶ Y
Z : C
g : Z ⟶ X
inst✝ : HasBinaryCoproduct Z H
h : IsSeparating {Z, H}
huv : ∀ (h : Z ⨿ H ⟶ X), h ≫ u = h ≫ v
⊢ g ≫ u = g ≫ v
[PROOFSTEP]
simpa using coprod.inl ≫= huv (coprod.desc g 0)
[GOAL]
case refine'_2.inr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G X Y : C
u v : X ⟶ Y
Z : C
g : Z ⟶ X
inst✝ : HasBinaryCoproduct G Z
h : IsSeparating {G, Z}
huv : ∀ (h : G ⨿ Z ⟶ X), h ≫ u = h ≫ v
⊢ g ≫ u = g ≫ v
[PROOFSTEP]
simpa using coprod.inr ≫= huv (coprod.desc 0 g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hG : IsSeparator G
⊢ {G} ⊆ {G, H}
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryCoproduct G H
hH : IsSeparator H
⊢ {H} ⊆ {G, H}
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
⊢ IsSeparator (∐ f) ↔ IsSeparating (Set.range f)
[PROOFSTEP]
refine' ⟨fun h X Y u v huv => _, fun h => (isSeparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
⊢ u = v
[PROOFSTEP]
refine' h.def _ _ fun g => colimit.hom_ext fun b => _
[GOAL]
case refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
b : Discrete β
⊢ colimit.ι (Discrete.functor f) b ≫ g ≫ u = colimit.ι (Discrete.functor f) b ≫ g ≫ v
[PROOFSTEP]
simpa using huv (f b.as) (by simp) (colimit.ι (Discrete.functor f) _ ≫ g)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparator (∐ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : G ⟶ X), h ≫ u = h ≫ v
g : ∐ f ⟶ X
b : Discrete β
⊢ f b.as ∈ Set.range f
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
Z : C
hZ : Z ∈ Set.range f
g : Z ⟶ X
⊢ g ≫ u = g ≫ v
[PROOFSTEP]
obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ
[GOAL]
case refine'_2.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v
[PROOFSTEP]
classical simpa using Sigma.ι f b ≫= huv (Sigma.desc (Pi.single b g))
[GOAL]
case refine'_2.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
h : IsSeparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : ∐ f ⟶ X), h ≫ u = h ≫ v
b : β
hZ : f b ∈ Set.range f
g : f b ⟶ X
⊢ g ≫ u = g ≫ v
[PROOFSTEP]
simpa using Sigma.ι f b ≫= huv (Sigma.desc (Pi.single b g))
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasCoproduct f
b : β
hb : IsSeparator (f b)
⊢ {f b} ⊆ Set.range f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
⊢ IsCoseparator (G ⨯ H) ↔ IsCoseparating {G, H}
[PROOFSTEP]
refine' ⟨fun h X Y u v huv => _, fun h => (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
⊢ u = v
[PROOFSTEP]
refine' h.def _ _ fun g => prod.hom_ext _ _
[GOAL]
case refine'_1.refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ (u ≫ g) ≫ prod.fst = (v ≫ g) ≫ prod.fst
[PROOFSTEP]
simpa using huv G (by simp) (g ≫ Limits.prod.fst)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ G ∈ {G, H}
[PROOFSTEP]
simp
[GOAL]
case refine'_1.refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ (u ≫ g) ≫ prod.snd = (v ≫ g) ≫ prod.snd
[PROOFSTEP]
simpa using huv H (by simp) (g ≫ Limits.prod.snd)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparator (G ⨯ H)
X Y : C
u v : X ⟶ Y
huv : ∀ (G_1 : C), G_1 ∈ {G, H} → ∀ (h : Y ⟶ G_1), u ≫ h = v ≫ h
g : Y ⟶ G ⨯ H
⊢ H ∈ {G, H}
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ G ⨯ H), u ≫ h = v ≫ h
Z : C
hZ : Z ∈ {G, H}
g : Y ⟶ Z
⊢ u ≫ g = v ≫ g
[PROOFSTEP]
simp only [Set.mem_insert_iff, Set.mem_singleton_iff] at hZ
[GOAL]
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
h : IsCoseparating {G, H}
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ G ⨯ H), u ≫ h = v ≫ h
Z : C
g : Y ⟶ Z
hZ : Z = G ∨ Z = H
⊢ u ≫ g = v ≫ g
[PROOFSTEP]
rcases hZ with (rfl | rfl)
[GOAL]
case refine'_2.inl
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
H X Y : C
u v : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝ : HasBinaryProduct Z H
h : IsCoseparating {Z, H}
huv : ∀ (h : Y ⟶ Z ⨯ H), u ≫ h = v ≫ h
⊢ u ≫ g = v ≫ g
[PROOFSTEP]
simpa using huv (prod.lift g 0) =≫ Limits.prod.fst
[GOAL]
case refine'_2.inr
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G X Y : C
u v : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝ : HasBinaryProduct G Z
h : IsCoseparating {G, Z}
huv : ∀ (h : Y ⟶ G ⨯ Z), u ≫ h = v ≫ h
⊢ u ≫ g = v ≫ g
[PROOFSTEP]
simpa using huv (prod.lift 0 g) =≫ Limits.prod.snd
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hG : IsCoseparator G
⊢ {G} ⊆ {G, H}
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hH : IsCoseparator H
⊢ {H} ⊆ {G, H}
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
⊢ IsCoseparator (∏ f) ↔ IsCoseparating (Set.range f)
[PROOFSTEP]
refine' ⟨fun h X Y u v huv => _, fun h => (isCoseparator_def _).2 fun X Y u v huv => h _ _ fun Z hZ g => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
⊢ u = v
[PROOFSTEP]
refine' h.def _ _ fun g => limit.hom_ext fun b => _
[GOAL]
case refine'_1
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ ∏ f
b : Discrete β
⊢ (u ≫ g) ≫ limit.π (Discrete.functor f) b = (v ≫ g) ≫ limit.π (Discrete.functor f) b
[PROOFSTEP]
simpa using huv (f b.as) (by simp) (g ≫ limit.π (Discrete.functor f) _)
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparator (∏ f)
X Y : C
u v : X ⟶ Y
huv : ∀ (G : C), G ∈ Set.range f → ∀ (h : Y ⟶ G), u ≫ h = v ≫ h
g : Y ⟶ ∏ f
b : Discrete β
⊢ f b.as ∈ Set.range f
[PROOFSTEP]
simp
[GOAL]
case refine'_2
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ f), u ≫ h = v ≫ h
Z : C
hZ : Z ∈ Set.range f
g : Y ⟶ Z
⊢ u ≫ g = v ≫ g
[PROOFSTEP]
obtain ⟨b, rfl⟩ := Set.mem_range.1 hZ
[GOAL]
case refine'_2.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ f), u ≫ h = v ≫ h
b : β
hZ : f b ∈ Set.range f
g : Y ⟶ f b
⊢ u ≫ g = v ≫ g
[PROOFSTEP]
classical simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b
[GOAL]
case refine'_2.intro
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
h : IsCoseparating (Set.range f)
X Y : C
u v : X ⟶ Y
huv : ∀ (h : Y ⟶ ∏ f), u ≫ h = v ≫ h
b : β
hZ : f b ∈ Set.range f
g : Y ⟶ f b
⊢ u ≫ g = v ≫ g
[PROOFSTEP]
simpa using huv (Pi.lift (Pi.single b g)) =≫ Pi.π f b
[GOAL]
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms C
β : Type w
f : β → C
inst✝ : HasProduct f
b : β
hb : IsCoseparator (f b)
⊢ {f b} ⊆ Set.range f
[PROOFSTEP]
simp
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
⊢ IsDetector G ↔ ReflectsIsomorphisms (coyoneda.obj (op G))
[PROOFSTEP]
refine' ⟨fun hG => ⟨fun f hf => hG.def _ fun h => _⟩, fun h => (isDetector_def _).2 fun X Y f hf => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : IsIso ((coyoneda.obj (op G)).map f)
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h
[PROOFSTEP]
rw [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsDetector G
A✝ B✝ : C
f : A✝ ⟶ B✝
hf : ∀ (b : (coyoneda.obj (op G)).obj B✝), ∃! a, (coyoneda.obj (op G)).map f a = b
h : G ⟶ B✝
⊢ ∃! h', h' ≫ f = h
[PROOFSTEP]
exact hf h
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : ReflectsIsomorphisms (coyoneda.obj (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso f
[PROOFSTEP]
suffices IsIso ((coyoneda.obj (op G)).map f) by exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : ReflectsIsomorphisms (coyoneda.obj (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
this : IsIso ((coyoneda.obj (op G)).map f)
⊢ IsIso f
[PROOFSTEP]
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (coyoneda.obj (op G)) _ h
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : ReflectsIsomorphisms (coyoneda.obj (op G))
X Y : C
f : X ⟶ Y
hf : ∀ (h : G ⟶ Y), ∃! h', h' ≫ f = h
⊢ IsIso ((coyoneda.obj (op G)).map f)
[PROOFSTEP]
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
⊢ IsCodetector G ↔ ReflectsIsomorphisms (yoneda.obj G)
[PROOFSTEP]
refine' ⟨fun hG => ⟨fun f hf => _⟩, fun h => (isCodetector_def _).2 fun X Y f hf => _⟩
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ IsIso f
[PROOFSTEP]
refine' (isIso_unop_iff _).1 (hG.def _ _)
[GOAL]
case refine'_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
hG : IsCodetector G
A✝ B✝ : Cᵒᵖ
f : A✝ ⟶ B✝
hf : IsIso ((yoneda.obj G).map f)
⊢ ∀ (h : B✝.unop ⟶ G), ∃! h', f.unop ≫ h' = h
[PROOFSTEP]
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique] at hf
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f
[PROOFSTEP]
rw [← isIso_op_iff]
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso f.op
[PROOFSTEP]
suffices IsIso ((yoneda.obj G).map f.op) by exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
[GOAL]
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
this : IsIso ((yoneda.obj G).map f.op)
⊢ IsIso f.op
[PROOFSTEP]
exact @isIso_of_reflects_iso _ _ _ _ _ _ _ (yoneda.obj G) _ h
[GOAL]
case refine'_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
G : C
h : ReflectsIsomorphisms (yoneda.obj G)
X Y : C
f : X ⟶ Y
hf : ∀ (h : X ⟶ G), ∃! h', f ≫ h' = h
⊢ IsIso ((yoneda.obj G).map f.op)
[PROOFSTEP]
rwa [isIso_iff_bijective, Function.bijective_iff_existsUnique]


[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
⊢ IsIso f ↔ f ≠ 0
[PROOFSTEP]
haveI : Mono (f ≫ i.hom) := mono_comp _ _
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ IsIso f ↔ f ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ IsIso f → f ≠ 0
[PROOFSTEP]
intro h w
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
⊢ False
[PROOFSTEP]
have j : IsIso (f ≫ i.hom)
[GOAL]
case j
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
⊢ IsIso (f ≫ i.hom)
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False
[PROOFSTEP]
infer_instance
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j : IsIso (f ≫ i.hom)
⊢ False
[PROOFSTEP]
rw [Simple.mono_isIso_iff_nonzero] at j
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : IsIso f
w : f = 0
j✝ : IsIso (f ≫ i.hom)
j : f ≫ i.hom ≠ 0
⊢ False
[PROOFSTEP]
subst w
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
m : Mono 0
this : Mono (0 ≫ i.hom)
h : IsIso 0
j✝ : IsIso (0 ≫ i.hom)
j : 0 ≫ i.hom ≠ 0
⊢ False
[PROOFSTEP]
simp at j
[GOAL]
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
⊢ f ≠ 0 → IsIso f
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ IsIso f
[PROOFSTEP]
have j : IsIso (f ≫ i.hom) := by
  apply isIso_of_mono_of_nonzero
  intro w
  apply h
  simpa using (cancel_mono i.inv).2 w
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ IsIso (f ≫ i.hom)
[PROOFSTEP]
apply isIso_of_mono_of_nonzero
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
⊢ f ≫ i.hom ≠ 0
[PROOFSTEP]
intro w
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ False
[PROOFSTEP]
apply h
[GOAL]
case w
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
w : f ≫ i.hom = 0
⊢ f = 0
[PROOFSTEP]
simpa using (cancel_mono i.inv).2 w
[GOAL]
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso f
[PROOFSTEP]
rw [← Category.comp_id f, ← i.hom_inv_id, ← Category.assoc]
[GOAL]
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X Y : C
inst✝ : Simple Y
i : X ≅ Y
Y✝ : C
f : Y✝ ⟶ X
m : Mono f
this : Mono (f ≫ i.hom)
h : f ≠ 0
j : IsIso (f ≫ i.hom)
⊢ IsIso ((f ≫ i.hom) ≫ i.inv)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
⊢ kernel.ι f = 0
[PROOFSTEP]
classical
by_contra h
haveI := isIso_of_mono_of_nonzero h
exact w (eq_zero_of_epi_kernel f)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
⊢ kernel.ι f = 0
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
h : ¬kernel.ι f = 0
⊢ False
[PROOFSTEP]
haveI := isIso_of_mono_of_nonzero h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : HasKernel f
w : f ≠ 0
h : ¬kernel.ι f = 0
this : IsIso (kernel.ι f)
⊢ False
[PROOFSTEP]
exact w (eq_zero_of_epi_kernel f)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi f
[PROOFSTEP]
rw [← image.fac f]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
⊢ Epi (factorThruImage f ≫ image.ι f)
[PROOFSTEP]
haveI : IsIso (image.ι f) := isIso_of_mono_of_nonzero fun h => w (eq_zero_of_image_eq_zero h)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasEqualizers C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : HasImage f
w : f ≠ 0
this : IsIso (image.ι f)
⊢ Epi (factorThruImage f ≫ image.ι f)
[PROOFSTEP]
apply epi_comp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0
[PROOFSTEP]
classical
by_contra h
exact w (isIso_of_mono_of_nonzero h)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
⊢ f = 0
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
X Y : C
inst✝¹ : Simple Y
f : X ⟶ Y
inst✝ : Mono f
w : IsIso f → False
h : ¬f = 0
⊢ False
[PROOFSTEP]
exact w (isIso_of_mono_of_nonzero h)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ IsIso (𝟙 X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ ¬IsZero X
[PROOFSTEP]
simpa [Limits.IsZero.iff_id_eq_zero] using id_nonzero X
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
inst✝ : Simple 0
⊢ 0 ≫ 0 = 𝟙 0 ∧ 0 ≫ 0 = 𝟙 0
[PROOFSTEP]
aesop_cat
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0
[PROOFSTEP]
classical
fconstructor
· intros
  have hx := cokernel.π_of_epi f
  by_contra h
  subst h
  exact (h _).mp (cokernel.π_of_zero _ _) hx
· intro hf
  suffices Epi f by exact isIso_of_mono_of_epi _
  apply Preadditive.epi_of_cokernel_zero
  by_contra h'
  exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f ↔ f ≠ 0
[PROOFSTEP]
fconstructor
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ IsIso f → f ≠ 0
[PROOFSTEP]
intros
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
⊢ f ≠ 0
[PROOFSTEP]
have hx := cokernel.π_of_epi f
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
hx : cokernel.π f = 0
⊢ f ≠ 0
[PROOFSTEP]
by_contra h
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h✝ : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
a✝ : IsIso f
hx : cokernel.π f = 0
h : f = 0
⊢ False
[PROOFSTEP]
subst h
[GOAL]
case mp
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
I : Mono 0
a✝ : IsIso 0
hx : cokernel.π 0 = 0
⊢ False
[PROOFSTEP]
exact (h _).mp (cokernel.π_of_zero _ _) hx
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
⊢ f ≠ 0 → IsIso f
[PROOFSTEP]
intro hf
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ IsIso f
[PROOFSTEP]
suffices Epi f by exact isIso_of_mono_of_epi _
[GOAL]
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
this : Epi f
⊢ IsIso f
[PROOFSTEP]
exact isIso_of_mono_of_epi _
[GOAL]
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ Epi f
[PROOFSTEP]
apply Preadditive.epi_of_cokernel_zero
[GOAL]
case mpr.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
⊢ cokernel.π f = 0
[PROOFSTEP]
by_contra h'
[GOAL]
case mpr.w
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
h : ∀ {Z : C} (f : X ⟶ Z) [inst : Epi f], IsIso f ↔ f ≠ 0
Y : C
f : Y ⟶ X
I : Mono f
hf : f ≠ 0
h' : ¬cokernel.π f = 0
⊢ False
[PROOFSTEP]
exact cokernel_not_iso_of_nonzero hf ((h _).mpr h')
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0
[PROOFSTEP]
classical
by_contra h
haveI := isIso_of_epi_of_nonzero h
exact w (eq_zero_of_mono_cokernel f)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
⊢ cokernel.π f = 0
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
⊢ False
[PROOFSTEP]
haveI := isIso_of_epi_of_nonzero h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
X Y : C
inst✝ : Simple Y
f : X ⟶ Y
w : f ≠ 0
h : ¬cokernel.π f = 0
this : IsIso (cokernel.π f)
⊢ False
[PROOFSTEP]
exact w (eq_zero_of_mono_cokernel f)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
⊢ f = 0
[PROOFSTEP]
classical
by_contra h
exact w (isIso_of_epi_of_nonzero h)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
⊢ f = 0
[PROOFSTEP]
by_contra h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Abelian C
X Y : C
inst✝¹ : Simple X
f : X ⟶ Y
inst✝ : Epi f
w : IsIso f → False
h : ¬f = 0
⊢ False
[PROOFSTEP]
exact w (isIso_of_epi_of_nonzero h)
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsIso biprod.inl ↔ IsZero Y
[PROOFSTEP]
rw [biprod.isIso_inl_iff_id_eq_fst_comp_inl, ← biprod.total, add_right_eq_self]
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 ↔ IsZero Y
[PROOFSTEP]
constructor
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ biprod.snd ≫ biprod.inr = 0 → IsZero Y
[PROOFSTEP]
intro h
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd ≫ biprod.inr = 0
⊢ IsZero Y
[PROOFSTEP]
replace h := h =≫ biprod.snd
[GOAL]
case mp
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : (biprod.snd ≫ biprod.inr) ≫ biprod.snd = 0 ≫ biprod.snd
⊢ IsZero Y
[PROOFSTEP]
simpa [← IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] using h
[GOAL]
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
⊢ IsZero Y → biprod.snd ≫ biprod.inr = 0
[PROOFSTEP]
intro h
[GOAL]
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : IsZero Y
⊢ biprod.snd ≫ biprod.inr = 0
[PROOFSTEP]
rw [IsZero.iff_isSplitEpi_eq_zero (biprod.snd : X ⊞ Y ⟶ Y)] at h
[GOAL]
case mpr
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X Y : C
h : biprod.snd = 0
⊢ biprod.snd ≫ biprod.inr = 0
[PROOFSTEP]
rw [h, zero_comp]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
⊢ IsZero Y ∨ IsZero Z
[PROOFSTEP]
refine' or_iff_not_imp_left.mpr fun h => _
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬IsZero Y
⊢ IsZero Z
[PROOFSTEP]
rw [IsZero.iff_isSplitMono_eq_zero (biprod.inl : Y ⟶ Y ⊞ Z)] at h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : ¬biprod.inl = 0
⊢ IsZero Z
[PROOFSTEP]
change biprod.inl ≠ 0 at h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
⊢ IsZero Z
[PROOFSTEP]
have : Simple (Y ⊞ Z) := Simple.of_iso i.symm
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : biprod.inl ≠ 0
this : Simple (Y ⊞ Z)
⊢ IsZero Z
[PROOFSTEP]
rw [← Simple.mono_isIso_iff_nonzero biprod.inl] at h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasBinaryBiproducts C
X : C
inst✝ : Simple X
Y Z : C
i : X ≅ Y ⊞ Z
h : IsIso biprod.inl
this : Simple (Y ⊞ Z)
⊢ IsZero Z
[PROOFSTEP]
rwa [Biprod.isIso_inl_iff_isZero] at h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
⊢ ∀ (a : Subobject X), a = ⊥ ∨ a = ⊤
[PROOFSTEP]
rintro ⟨⟨⟨Y : C, ⟨⟨⟩⟩, f : Y ⟶ X⟩, m : Mono f⟩⟩
[GOAL]
case mk.mk.mk.mk.unit
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
a✝ : Subobject X
Y : C
f : Y ⟶ X
m : Mono f
⊢ Quot.mk Setoid.r { obj := { left := Y, right := { as := PUnit.unit }, hom := f }, property := m } = ⊥ ∨
    Quot.mk Setoid.r { obj := { left := Y, right := { as := PUnit.unit }, hom := f }, property := m } = ⊤
[PROOFSTEP]
change mk f = ⊥ ∨ mk f = ⊤
[GOAL]
case mk.mk.mk.mk.unit
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
a✝ : Subobject X
Y : C
f : Y ⟶ X
m : Mono f
⊢ mk f = ⊥ ∨ mk f = ⊤
[PROOFSTEP]
by_cases h : f = 0
[GOAL]
case pos
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
a✝ : Subobject X
Y : C
f : Y ⟶ X
m : Mono f
h : f = 0
⊢ mk f = ⊥ ∨ mk f = ⊤
[PROOFSTEP]
exact Or.inl (mk_eq_bot_iff_zero.mpr h)
[GOAL]
case neg
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : Simple X
a✝ : Subobject X
Y : C
f : Y ⟶ X
m : Mono f
h : ¬f = 0
⊢ mk f = ⊥ ∨ mk f = ⊤
[PROOFSTEP]
refine' Or.inr ((isIso_iff_mk_eq_top _).mp ((Simple.mono_isIso_iff_nonzero f).mpr h))
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ Simple X
[PROOFSTEP]
constructor
[GOAL]
case mono_isIso_iff_nonzero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
⊢ ∀ {Y : C} (f : Y ⟶ X) [inst : Mono f], IsIso f ↔ f ≠ 0
[PROOFSTEP]
intros Y f hf
[GOAL]
case mono_isIso_iff_nonzero
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f ↔ f ≠ 0
[PROOFSTEP]
constructor
[GOAL]
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ IsIso f → f ≠ 0
[PROOFSTEP]
intro i
[GOAL]
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : IsIso f
⊢ f ≠ 0
[PROOFSTEP]
rw [Subobject.isIso_iff_mk_eq_top] at i
[GOAL]
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
⊢ f ≠ 0
[PROOFSTEP]
intro w
[GOAL]
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w : f = 0
⊢ False
[PROOFSTEP]
rw [← Subobject.mk_eq_bot_iff_zero] at w
[GOAL]
case mono_isIso_iff_nonzero.mp
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : mk f = ⊤
w✝ : f = 0
w : mk f = ⊥
⊢ False
[PROOFSTEP]
exact IsSimpleOrder.bot_ne_top (w.symm.trans i)
[GOAL]
case mono_isIso_iff_nonzero.mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
⊢ f ≠ 0 → IsIso f
[PROOFSTEP]
intro i
[GOAL]
case mono_isIso_iff_nonzero.mpr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
⊢ IsIso f
[PROOFSTEP]
rcases IsSimpleOrder.eq_bot_or_eq_top (Subobject.mk f) with (h | h)
[GOAL]
case mono_isIso_iff_nonzero.mpr.inl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊥
⊢ IsIso f
[PROOFSTEP]
rw [Subobject.mk_eq_bot_iff_zero] at h
[GOAL]
case mono_isIso_iff_nonzero.mpr.inl
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h✝ : mk f = ⊥
h : f = 0
⊢ IsIso f
[PROOFSTEP]
exact False.elim (i h)
[GOAL]
case mono_isIso_iff_nonzero.mpr.inr
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
X : C
inst✝ : IsSimpleOrder (Subobject X)
Y : C
f : Y ⟶ X
hf : Mono f
i : f ≠ 0
h : mk f = ⊤
⊢ IsIso f
[PROOFSTEP]
exact (Subobject.isIso_iff_mk_eq_top _).mpr h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ Simple X → IsSimpleOrder (Subobject X)
[PROOFSTEP]
intro h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Simple X
⊢ IsSimpleOrder (Subobject X)
[PROOFSTEP]
infer_instance
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
⊢ IsSimpleOrder (Subobject X) → Simple X
[PROOFSTEP]
intro h
[GOAL]
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : IsSimpleOrder (Subobject X)
⊢ Simple X
[PROOFSTEP]
exact simple_of_isSimpleOrder_subobject X