Documentation

Mathlib.CategoryTheory.Comma.CardinalArrow

Cardinal of Arrow #

We obtain various results about the cardinality of Arrow C. For example, if C is a (small) category, Arrow C is finite iff FinCategory C holds.

source
๐Ÿ“ coverage
theorem CategoryTheory.Arrow.finite_iff (C : Type u) [SmallCategory C] :
Finite (Arrow C) โ†” Nonempty (FinCategory C)
source
๐Ÿ“ coverage
instance CategoryTheory.Arrow.finite {C : Type u} [SmallCategory C] [FinCategory C] :
Finite (Arrow C)
source
๐Ÿ”ธ coverage
def CategoryTheory.Arrow.opEquiv (C : Type u) [Category.{v, u} C] :
Arrow Cแต’แต– โ‰ƒ Arrow C

The bijection Arrow Cแต’แต– โ‰ƒ Arrow C.

Instances For
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem CategoryTheory.hasCardinalLT_arrow_op_iff (C : Type u) [Category.{v, u} C] (ฮบ : Cardinal.{w}) :
    HasCardinalLT (Arrow Cแต’แต–) ฮบ โ†” HasCardinalLT (Arrow C) ฮบ
    source
    ๐Ÿ“ coverage
    @[simp]
    theorem CategoryTheory.hasCardinalLT_arrow_discrete_iff {X : Type u} (ฮบ : Cardinal.{w}) :
    HasCardinalLT (Arrow (Discrete X)) ฮบ โ†” HasCardinalLT X ฮบ
    source
    ๐Ÿ“ coverage
    instance CategoryTheory.instFiniteArrowDiscrete (X : Type u) [Finite X] :
    Finite (Arrow (Discrete X))
    source
    ๐Ÿ“ coverage
    theorem CategoryTheory.small_of_small_arrow (C : Type u) [Category.{v, u} C] [Small.{w, max u v} (Arrow C)] :
    Small.{w, u} C
    source
    ๐Ÿ“ coverage
    theorem CategoryTheory.locallySmall_of_small_arrow (C : Type u) [Category.{v, u} C] [Small.{w, max u v} (Arrow C)] :
    LocallySmall.{w, v, u} C
    source
    ๐Ÿ”ธ coverage
    noncomputable def CategoryTheory.Arrow.shrinkHomsEquiv (C : Type u) [Category.{v, u} C] [LocallySmall.{w, v, u} C] :
    Arrow (ShrinkHoms.{u} C) โ‰ƒ Arrow C

    The bijection Arrow.{w} (ShrinkHoms C) โ‰ƒ Arrow C.

    Instances For
      source
      ๐Ÿ”ธ coverage
      noncomputable def CategoryTheory.Arrow.shrinkEquiv (C : Type u) [Category.{v, u} C] [Small.{w, u} C] :
      Arrow (Shrink.{w, u} C) โ‰ƒ Arrow C

      The bijection Arrow (Shrink C) โ‰ƒ Arrow C.

      Instances For
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem CategoryTheory.hasCardinalLT_arrow_shrinkHoms_iff (C : Type u) [Category.{v, u} C] [LocallySmall.{w', v, u} C] (ฮบ : Cardinal.{w}) :
        HasCardinalLT (Arrow (ShrinkHoms.{u} C)) ฮบ โ†” HasCardinalLT (Arrow C) ฮบ
        source
        ๐Ÿ“ coverage
        @[simp]
        theorem CategoryTheory.hasCardinalLT_arrow_shrink_iff (C : Type u) [Category.{v, u} C] [Small.{w', u} C] (ฮบ : Cardinal.{w}) :
        HasCardinalLT (Arrow (Shrink.{w', u} C)) ฮบ โ†” HasCardinalLT (Arrow C) ฮบ
        source
        ๐Ÿ“ coverage
        theorem CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow {C : Type u} [Category.{v, u} C] {ฮบ : Cardinal.{w}} (h : HasCardinalLT (Arrow C) ฮบ) :
        HasCardinalLT C ฮบ