sheafificationAdjunction_counit_app_val

English

The inverse of the isomorphism toSheafify J P is given by the sheafification lift of the identity on P.

Русский

Обратное изоморфизма toSheafify J P задано через перемещение (lift) идентичности на P.

LaTeX

$$((isoSheafify J hP).inv = sheafifyLift J (\mathbf{1}) hP)$$

Lean4

@[simp]
theorem sheafificationAdjunction_counit_app_val (P : Sheaf J D) :
    ((sheafificationAdjunction J D).counit.app P).val = sheafifyLift J (𝟙 P.val) P.cond :=
  by
  unfold sheafifyLift
  rw [Adjunction.homEquiv_counit]
  simp

Похожие утверждения