case mp
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
⊢ Presieve.EffectiveEpimorphic (Presieve.singleton f) → EffectiveEpi f

case mpr
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
⊢ EffectiveEpi f → Presieve.EffectiveEpimorphic (Presieve.singleton f)
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
⊢ Presieve.EffectiveEpimorphic (Presieve.singleton f) ↔ EffectiveEpi f
constructor
case mp
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (Presieve.cocone (generate (Presieve.singleton f)).arrows))
⊢ EffectiveEpi f
case mp
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
⊢ Presieve.EffectiveEpimorphic (Presieve.singleton f) → EffectiveEpi f
intro (h : Nonempty _)
case mp
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (Presieve.cocone (generateSingleton f).arrows))
⊢ EffectiveEpi f
case mp
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (Presieve.cocone (generate (Presieve.singleton f)).arrows))
⊢ EffectiveEpi f
rw [Sieve.generateSingleton_eq] at h
case mp.effectiveEpi
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (Presieve.cocone (generateSingleton f).arrows))
⊢ Nonempty (EffectiveEpiStruct f)
case mp
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (Presieve.cocone (generateSingleton f).arrows))
⊢ EffectiveEpi f
constructor
no goals
case mp.effectiveEpi
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (IsColimit (Presieve.cocone (generateSingleton f).arrows))
⊢ Nonempty (EffectiveEpiStruct f)
apply Nonempty.map (effectiveEpiStructOfIsColimit _) h
case mpr.mk
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Presieve.EffectiveEpimorphic (Presieve.singleton f)
case mpr
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
⊢ EffectiveEpi f → Presieve.EffectiveEpimorphic (Presieve.singleton f)
rintro ⟨h⟩
case mpr.mk
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (Presieve.cocone (generate (Presieve.singleton f)).arrows))
case mpr.mk
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Presieve.EffectiveEpimorphic (Presieve.singleton f)
show Nonempty _
case mpr.mk
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (Presieve.cocone (generateSingleton f).arrows))
case mpr.mk
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (Presieve.cocone (generate (Presieve.singleton f)).arrows))
rw [Sieve.generateSingleton_eq]
no goals
case mpr.mk
C : Type u_2
inst✝ : Category C
X Y : C
f : Y ⟶ X
h : Nonempty (EffectiveEpiStruct f)
⊢ Nonempty (IsColimit (Presieve.cocone (generateSingleton f).arrows))
apply Nonempty.map (isColimitOfEffectiveEpiStruct _) h