isIso_fst'_self — Mathlib

English

The projection hf.rep.fst' f is an isomorphism under suitable assumptions (e.g., monomorphism base).

Русский

Проекция hf.rep.fst' f является изоморфизмом при разумных предпосылках (например, базовый мономорфизм).

LaTeX

$$$IsIso(hf.rep.fst' f)$$$

Lean4

theorem isIso_fst'_self (hP : P ≤ MorphismProperty.monomorphisms C) {X : C} {f : yoneda.obj X ⟶ G} (hf : P.presheaf f) :
    IsIso (hf.rep.fst' f) :=
  have := P.presheaf_mono_of_le hP hf
  have := (hf.rep.isPullback' f).isIso_fst_of_mono
  Yoneda.fullyFaithful.isIso_of_isIso_map _

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