W_sheafToPresheaf_map_iff_isIso — Mathlib

English

For F1, F2 sheaves and φ: F1 ⟶ F2, W of the mapped morphism equals isomorphism condition: W((sheafToPresheaf J A).map φ) iff φ is an isomorphism.

Русский

Для гомоморфизмa φ между шейфами F1 и F2, равносильно условию: W((sheafToPresheaf J A).map φ) эквивалентно тому, что φ — изоморфизм.

LaTeX

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

Lean4

theorem W_sheafToPresheaf_map_iff_isIso {F₁ F₂ : Sheaf J A} (φ : F₁ ⟶ F₂) :
    J.W ((sheafToPresheaf J A).map φ) ↔ IsIso φ := by
  rw [W_eq_W_range_sheafToPresheaf_obj, LeftBousfield.W_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩, isIso_iff_of_reflects_iso]

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