English
A naturality relation holds between toSheafify, sheafifyLift, and η: P ⟶ Q; the composed map equals η up to the adjunction unit.
Русский
Для отображения η между P и Q выполняется натуральное отношение между toSheafify, sheafifyLift и η; композиция равна η через единицу анализируемого фрагмента.
LaTeX
$$$toSheafify\, J\, P \; \getsto\; toSheafify J Q$ и равенство последовательностей: $\eta \;=\; toSheafify J P \circ \mathrm{sheafifyLift} J \eta hQ$$$
Lean4
@[reassoc (attr := simp)]
theorem toSheafify_sheafifyLift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) :
toSheafify J P ≫ sheafifyLift J η hQ = η :=
by
rw [toSheafify, sheafifyLift, Adjunction.homEquiv_counit]
change _ ≫ (sheafToPresheaf J D).map _ ≫ _ = _
simp only [Adjunction.unit_naturality_assoc]
change _ ≫ (sheafificationAdjunction J D).unit.app ((sheafToPresheaf J D).obj ⟨Q, hQ⟩) ≫ _ = _
change _ ≫ _ ≫ (sheafToPresheaf J D).map _ = _
rw [sheafificationAdjunction J D |>.right_triangle_components (Y := ⟨Q, hQ⟩)]
simp
