W_adj_unit_app — Mathlib

English

For an adjunction G ⊣ sheafToPresheaf J A and any P, J.W of the unit component at P holds.

Русский

Для сопряжения G ⊣ sheafToPresheaf J A и любого P имеет место, что J.W(единица) на P удовлетворяет условию.

LaTeX

$$$(\mathrm{adj} : G \dashv \mathrm{sheafToPresheaf}(J,A))\ (P) :\ J.W(\mathrm{adj}.\mathrm{unit}.\mathrm{app} \ P).$$$

Lean4

theorem W_adj_unit_app (adj : G ⊣ sheafToPresheaf J A) (P : Cᵒᵖ ⥤ A) : J.W (adj.unit.app P) :=
  by
  rw [W_eq_W_range_sheafToPresheaf_obj]
  exact LeftBousfield.W_adj_unit_app adj P

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