instFaithfulFintypeCat — Mathlib

English

There is a colimit for shape SingleObj(G) for finite groups G.

Русский

Существует колимит по форме SingleObj(G) для конечной группы G.

LaTeX

$$$\\forall G\\,[\\mathrm{Group}(G) \\land \\mathrm{Finite}(G) \\Rightarrow \\mathrm{HasColimitsOfShape}(\\mathrm{SingleObj}(G), C)]$$

Lean4

/-- Fiber functors are faithful. -/
instance : F.Faithful where
  map_injective {X Y} f g
    h := by
    haveI : IsIso (equalizer.ι (F.map f) (F.map g)) := equalizer.ι_of_eq h
    haveI : IsIso (F.map (equalizer.ι f g)) :=
      by
      rw [← equalizerComparison_comp_π f g F]
      exact IsIso.comp_isIso
    haveI : IsIso (equalizer.ι f g) := isIso_of_reflects_iso _ F
    exact eq_of_epi_equalizer

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