isConnected_iff_of_final — Mathlib

English

The domain of a final functor is connected if and only if the codomain is connected.

Русский

Область определения финального функторa связна тогда и только тогда, когда кодомен связан.

LaTeX

$$$\IsConnected C \iff \IsConnected D$ \quad \text{given } F: C \to D \text{ with } F\text{ Final}$$$

Lean4

/-- The domain of a final functor is connected if and only if its codomain is connected. -/
theorem isConnected_iff_of_final (F : C ⥤ D) [F.Final] : IsConnected C ↔ IsConnected D :=
  by
  rw [isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} C,
    isConnected_iff_colimit_constPUnitFunctor_iso_pUnit.{max v u v₂ u₂} D]
  exact
    Equiv.nonempty_congr <|
      Iso.isoCongrLeft <| CategoryTheory.Functor.Final.colimitIso F <| constPUnitFunctor.{max u v u₂ v₂} D

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