isGroupoid — Mathlib

English

If D is a groupoid and F: C → D, then the induced category InducedCategory D F is a groupoid.

Русский

Если D — группоида и F: C → D, то индуцированная категория InducedCategory D F является групоидом.

LaTeX

$$$\mathrm{IsGroupoid}(\mathrm{InducedCategory}\, D\, F)$$$

Lean4

instance isGroupoid {C : Type u} (D : Type u₂) [Category.{v} D] [IsGroupoid D] (F : C → D) :
    IsGroupoid (InducedCategory D F) :=
  isGroupoid_of_reflects_iso (inducedFunctor F)

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