case mp
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ Presieve.EffectiveEpimorphic (Presieve.ofArrows X π) → EffectiveEpiFamily X π

case mpr
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpiFamily X π → Presieve.EffectiveEpimorphic (Presieve.ofArrows X π)
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ Presieve.EffectiveEpimorphic (Presieve.ofArrows X π) ↔ EffectiveEpiFamily X π
constructor
case mp
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (Presieve.cocone (generate (Presieve.ofArrows X π)).arrows))
⊢ EffectiveEpiFamily X π
case mp
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ Presieve.EffectiveEpimorphic (Presieve.ofArrows X π) → EffectiveEpiFamily X π
intro (h : Nonempty _)
case mp
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (Presieve.cocone (generateFamily X π).arrows))
⊢ EffectiveEpiFamily X π
case mp
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (Presieve.cocone (generate (Presieve.ofArrows X π)).arrows))
⊢ EffectiveEpiFamily X π
rw [Sieve.generateFamily_eq] at h
case mp.effectiveEpiFamily
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (Presieve.cocone (generateFamily X π).arrows))
⊢ Nonempty (EffectiveEpiFamilyStruct X π)
case mp
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (Presieve.cocone (generateFamily X π).arrows))
⊢ EffectiveEpiFamily X π
constructor
no goals
case mp.effectiveEpiFamily
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (IsColimit (Presieve.cocone (generateFamily X π).arrows))
⊢ Nonempty (EffectiveEpiFamilyStruct X π)
apply Nonempty.map (effectiveEpiFamilyStructOfIsColimit _ _) h
case mpr.mk
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Presieve.EffectiveEpimorphic (Presieve.ofArrows X π)
case mpr
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpiFamily X π → Presieve.EffectiveEpimorphic (Presieve.ofArrows X π)
rintro ⟨h⟩
case mpr.mk
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (Presieve.cocone (generate (Presieve.ofArrows X π)).arrows))
case mpr.mk
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Presieve.EffectiveEpimorphic (Presieve.ofArrows X π)
show Nonempty _
case mpr.mk
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (Presieve.cocone (generateFamily X π).arrows))
case mpr.mk
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (Presieve.cocone (generate (Presieve.ofArrows X π)).arrows))
rw [Sieve.generateFamily_eq]
no goals
case mpr.mk
C : Type u_3
inst✝ : Category C
B : C
α : Type u_1
X : α → C
π : (a : α) → X a ⟶ B
h : Nonempty (EffectiveEpiFamilyStruct X π)
⊢ Nonempty (IsColimit (Presieve.cocone (generateFamily X π).arrows))
apply Nonempty.map (isColimitOfEffectiveEpiFamilyStruct _ _) h