C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ generate (functorPushforward F ⊤).arrows = ⊤
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ functorPushforward F ⊤ = ⊤
refine' (generate_sieve _).symm.trans _
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ (functorPushforward F ⊤).arrows (𝟙 (F.obj X))
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ generate (functorPushforward F ⊤).arrows = ⊤
apply generate_of_contains_isSplitEpi (𝟙 (F.obj X))
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ (functorPushforward F ⊤).arrows (𝟙 (F.obj X))
refine' ⟨X, 𝟙 _, 𝟙 _, trivial, by simp⟩
no goals
C : Type u₁
inst✝² : Category C
D : Type u₂
inst✝¹ : Category D
F✝ : C ⥤ D
X✝ Y Z : C
f : Y ⟶ X✝
S R : Sieve X✝
E : Type u₃
inst✝ : Category E
G : D ⥤ E
F : C ⥤ D
X : C
⊢ 𝟙 (F.obj X) = 𝟙 (F.obj X) ≫ F.map (𝟙 X)
simp