W_iff_isIso_map — Mathlib

English

For any morphism f in D, the left/right variant of W applied to f is equivalent to G.map f being an isomorphism after localization.

Русский

Для любого морфизма f в D: применение W к f эквивалентно тому, что G.map f становится изоморфизмом после локализации.

LaTeX

$$$W (\\cdot \\in Set.range F.obj) f \\;\\iff\\; IsIso (G.map f)$$$

Lean4

theorem W_iff_isIso_map {X Y : D} (f : X ⟶ Y) : W (· ∈ Set.range F.obj) f ↔ IsIso (G.map f) :=
  by
  rw [← (W (· ∈ Set.range F.obj)).postcomp_iff _ _ (W_adj_unit_app adj Y)]
  erw [adj.unit.naturality f]
  rw [(W (· ∈ Set.range F.obj)).precomp_iff _ _ (W_adj_unit_app adj X), W_iff_isIso _ _ ⟨_, rfl⟩ ⟨_, rfl⟩]
  constructor
  · intro h
    dsimp at h
    exact isIso_of_fully_faithful F (G.map f)
  · intro
    rw [Functor.comp_map]
    infer_instance

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