W_iff — Mathlib

English

For all f, W f is equivalent to IsIso of the mapped presheaf to sheaf morphism.

Русский

Для любого f, W f эквивалентно тому, что отображение под presheafToSheaf является изоморфизмом.

LaTeX

$$$J.W f \iff \mathrm{IsIso}\big((\mathrm{presheafToSheaf}(J,A)).map f\big).$$$

Lean4

theorem W_iff {P₁ P₂ : Cᵒᵖ ⥤ A} (f : P₁ ⟶ P₂) : J.W f ↔ IsIso ((presheafToSheaf J A).map f) :=
  J.W_iff_isIso_map_of_adjunction (sheafificationAdjunction J A) f

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