countableCategoryUlift — Mathlib

English

Applying ULift to morphisms and objects preserves countability: if J is countable, then ULiftHom(ULift J) is a countable category.

Русский

Применение ULift к объектам и морфизмам сохраняет счетность: если J счетна, то ULiftHom(ULift J) счетна.

LaTeX

$$$\operatorname{CountableCategory}(\mathrm{ULiftHom}(\mathrm{ULift}(J)))$$$

Lean4

/-- Applying `ULift` to morphisms and objects of a category preserves countability. -/
instance countableCategoryUlift {J : Type v} [Category J] [CountableCategory J] :
    CountableCategory.{max w v} (ULiftHom.{w, max w v} (ULift.{w, v} J))
    where
  countableObj := instCountableULift
  countableHom := fun i j =>
    have : Countable ((ULiftHom.objDown i).down ⟶ (ULiftHom.objDown j).down) := inferInstance
    instCountableULift

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