English
For a connected object X, the quotient X/Aut X is terminal if and only if the quotient F.obj X / Aut X has exactly one element (i.e., is unique).
Русский
Для связного объекта X квадрат X/Aut X является терминальным тогда и только тогда, когда квадрат F.obj X / Aut X содержит ровно по одному элементу (эквивалентно единственному элементу).
LaTeX
$$$\\text{IsTerminal}\\bigl(\\operatorname{colimit}(\\mathrm{SingleObj.functor}(\\mathrm{Aut.toEnd}\,X))\\bigr) \\ \\iff\\ \\mathrm{Unique}\\bigl(\\operatorname{MulAction.orbitRel.Quotient}(\\mathrm{Aut}\,X, F.obj X)\\bigr).$$$
Lean4
/-- For a connected object `X` of `C`, the quotient `X / Aut X` is terminal if and only if
the quotient `F.obj X / Aut X` has exactly one element. -/
noncomputable def quotientByAutTerminalEquivUniqueQuotient (X : C) [IsConnected X] :
IsTerminal (colimit <| SingleObj.functor <| Aut.toEnd X) ≃ Unique (MulAction.orbitRel.Quotient (Aut X) (F.obj X)) :=
by
let J : SingleObj (Aut X) ⥤ C := SingleObj.functor (Aut.toEnd X)
let e : (F ⋙ FintypeCat.incl).obj (colimit J) ≅ _ :=
preservesColimitIso (F ⋙ FintypeCat.incl) J ≪≫
(Equiv.toIso <| SingleObj.Types.colimitEquivQuotient (J ⋙ F ⋙ FintypeCat.incl))
apply Equiv.trans
·
apply
(IsTerminal.isTerminalIffObj (F ⋙ FintypeCat.incl) _).trans
(isLimitEmptyConeEquiv _ (asEmptyCone _) (asEmptyCone _) e)
exact Types.isTerminalEquivUnique _
