isGroupoid_of_reflects_iso — Mathlib

English

If F: C → D reflects isomorphisms and D is a groupoid, then C is a groupoid.

Русский

Если F: C → D отражает изоморфизмы и D является групоида, то C является групоидом.

LaTeX

$$$\mathrm{IsGroupoid}(C)$$$

Lean4

theorem isGroupoid_of_reflects_iso {C D : Type*} [Category C] [Category D] (F : C ⥤ D) [F.ReflectsIsomorphisms]
    [IsGroupoid D] : IsGroupoid C where all_isIso _ := isIso_of_reflects_iso _ F

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