case a
C : Type u
inst✝¹² : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category D
E : Type w₂
inst✝¹⁰ : Category E
F : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁵ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝⁴ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝³ : ConcreteCategory D
inst✝² : PreservesLimits (forget D)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
⊢ toSheafify J (P ⋙ F) ≫ (sheafifyCompIso J F P).inv = whiskerRight (toSheafify J P) F
C : Type u
inst✝¹² : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category D
E : Type w₂
inst✝¹⁰ : Category E
F : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁵ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝⁴ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝³ : ConcreteCategory D
inst✝² : PreservesLimits (forget D)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
⊢ (sheafifyCompIso J F P).inv =
    sheafifyLift J (whiskerRight (toSheafify J P) F) (_ : Presheaf.IsSheaf J (sheafify J P ⋙ F))
apply J.sheafifyLift_unique
case a
C : Type u
inst✝¹² : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category D
E : Type w₂
inst✝¹⁰ : Category E
F : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁵ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝⁴ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝³ : ConcreteCategory D
inst✝² : PreservesLimits (forget D)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
⊢ toSheafify J (P ⋙ F) = whiskerRight (toSheafify J P) F ≫ (sheafifyCompIso J F P).hom
case a
C : Type u
inst✝¹² : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category D
E : Type w₂
inst✝¹⁰ : Category E
F : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁵ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝⁴ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝³ : ConcreteCategory D
inst✝² : PreservesLimits (forget D)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
⊢ toSheafify J (P ⋙ F) ≫ (sheafifyCompIso J F P).inv = whiskerRight (toSheafify J P) F
rw [Iso.comp_inv_eq]
no goals
case a
C : Type u
inst✝¹² : Category C
J : GrothendieckTopology C
D : Type w₁
inst✝¹¹ : Category D
E : Type w₂
inst✝¹⁰ : Category E
F : D ⥤ E
inst✝⁹ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) D
inst✝⁸ : ∀ (α β : Type (max v u)) (fst snd : β → α), HasLimitsOfShape (WalkingMulticospan fst snd) E
inst✝⁷ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ D
inst✝⁶ : ∀ (X : C), HasColimitsOfShape (Cover J X)ᵒᵖ E
inst✝⁵ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ F
inst✝⁴ : (X : C) → (W : Cover J X) → (P : Cᵒᵖ ⥤ D) → PreservesLimit (MulticospanIndex.multicospan (Cover.index W P)) F
P : Cᵒᵖ ⥤ D
inst✝³ : ConcreteCategory D
inst✝² : PreservesLimits (forget D)
inst✝¹ : (X : C) → PreservesColimitsOfShape (Cover J X)ᵒᵖ (forget D)
inst✝ : ReflectsIsomorphisms (forget D)
⊢ toSheafify J (P ⋙ F) = whiskerRight (toSheafify J P) F ≫ (sheafifyCompIso J F P).hom
simp