essentiallySmall_iff — Mathlib

English

Let C be a category. Then C is essentially small if and only if Skeleton(C) is small and C is locally small.

Русский

Пусть C — категория. Тогда C является существенно малой тогда и только тогда, когда Skeleton(C) есть малый тип множества объектов и C локально мал.

LaTeX

$$$\text{EssentiallySmall}(C) \iff (\text{Small}(\text{Skeleton}(C)) \wedge \text{LocallySmall}(C))$$$

Lean4

/-- A category is essentially small if and only if
the underlying type of its skeleton (i.e. the "set" of isomorphism classes) is small,
and it is locally small.
-/
theorem essentiallySmall_iff (C : Type u) [Category.{v} C] :
    EssentiallySmall.{w} C ↔ Small.{w} (Skeleton C) ∧ LocallySmall.{w} C := by
  -- This theorem is the only bit of real work in this file.

  fconstructor
  · intro h
    fconstructor
    · rcases h with ⟨S, 𝒮, ⟨e⟩⟩
      refine ⟨⟨Skeleton S, ⟨?_⟩⟩⟩
      exact e.skeletonEquiv
    · infer_instance
  · rintro ⟨⟨S, ⟨e⟩⟩, L⟩
    let e' := (ShrinkHoms.equivalence C).skeletonEquiv.symm
    letI : Category S := InducedCategory.category (e'.trans e).symm
    refine ⟨⟨S, this, ⟨?_⟩⟩⟩
    refine
      (ShrinkHoms.equivalence C).trans <|
        (skeletonEquivalence (ShrinkHoms C)).symm.trans ((inducedFunctor (e'.trans e).symm).asEquivalence.symm)

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