nonempty_of_colim_preservesLimitsOfShapeFinZero

English

Auxiliary version: if F: C ⥤ D with Final F, and C is sifted, then D is sifted.

Русский

Вспомогательная версия: если F: C ⥤ D с Final F и C ситообразна, то D ситообразна.

LaTeX

$$IsSifted D$$

Lean4

theorem nonempty_of_colim_preservesLimitsOfShapeFinZero
    [PreservesLimitsOfShape (Discrete (Fin 0)) (colim : (C ⥤ Type u) ⥤ Type u)] : Nonempty C :=
  by
  suffices connected : IsConnected C by infer_instance
  rw [Types.isConnected_iff_colimit_constPUnitFunctor_iso_pUnit]
  constructor
  haveI : PreservesLimitsOfShape (Discrete PEmpty) (colim : (C ⥤ _) ⥤ Type u) :=
    preservesLimitsOfShape_of_equiv (Discrete.equivalence finZeroEquiv') _
  apply HasColimit.isoOfNatIso (_ : Types.constPUnitFunctor C ≅ (⊤_ (C ⥤ Type u))) |>.trans
  · apply PreservesTerminal.iso colim |>.trans
    exact Types.terminalIso
  · apply_rules [IsTerminal.uniqueUpToIso _ terminalIsTerminal, evaluationJointlyReflectsLimits]
    intro _
    exact isLimitChangeEmptyCone _ Types.isTerminalPunit _ <| Iso.refl _

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