W_iff_isIso_map_of_adjunction — Mathlib

English

For an adjunction G ⊣ sheafToPresheaf J A and any f, W f is equivalent to IsIso(G.map f).

Русский

Для сопряжения G ⊣ sheafToPresheaf J A и любого f, W f эквивалентно тому, что G.map f является изоморфизмом.

LaTeX

$$$J.W f \iff \mathrm{IsIso}(G.map f).$$$

Lean4

theorem W_iff_isIso_map_of_adjunction (adj : G ⊣ sheafToPresheaf J A) {P₁ P₂ : Cᵒᵖ ⥤ A} (f : P₁ ⟶ P₂) :
    J.W f ↔ IsIso (G.map f) := by
  rw [W_eq_W_range_sheafToPresheaf_obj]
  exact LeftBousfield.W_iff_isIso_map adj f

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