instReflectsMonomorphismsFintypeCat

English

Fiber functors reflect monomorphisms.

Русский

Фибровые функторы отражают мономорфизмами.

LaTeX

$$$\\mathrm{ReflectsMonomorphisms}(F)$$$

Lean4

/-- Fiber functors reflect monomorphisms. -/
instance : ReflectsMonomorphisms F :=
  ReflectsMonomorphisms.mk <| by
    intro X Y f _
    haveI : IsIso (pullback.fst (F.map f) (F.map f)) := isIso_fst_of_mono (F.map f)
    haveI : IsIso (F.map (pullback.fst f f)) :=
      by
      rw [← PreservesPullback.iso_hom_fst]
      exact IsIso.comp_isIso
    haveI : IsIso (pullback.fst f f) := isIso_of_reflects_iso (pullback.fst _ _) F
    exact (pullback.diagonal_isKernelPair f).mono_of_isIso_fst

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