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
theorem CategoryTheory.Arrow.finite_iff (C : Type u) [SmallCategory C] :
Finite (Arrow C) ↔ Nonempty (FinCategory C)
source
instance CategoryTheory.Arrow.finite {C : Type u} [SmallCategory C] [FinCategory C] :
Finite (Arrow C)
source
def CategoryTheory.Arrow.opEquiv (C : Type u) [Category.{v, u} C] :
Arrow Cᵒᵖ ≃ Arrow C

The bijection Arrow Cᵒᵖ ≃ Arrow C.

Instances For
    source
    @[simp]
    theorem CategoryTheory.hasCardinalLT_arrow_op_iff (C : Type u) [Category.{v, u} C] (κ : Cardinal.{w}) :
    HasCardinalLT (Arrow Cᵒᵖ) κ ↔ HasCardinalLT (Arrow C) κ
    source
    @[simp]
    theorem CategoryTheory.hasCardinalLT_arrow_discrete_iff {X : Type u} (κ : Cardinal.{w}) :
    HasCardinalLT (Arrow (Discrete X)) κ ↔ HasCardinalLT X κ
    source
    instance CategoryTheory.instFiniteArrowDiscrete (X : Type u) [Finite X] :
    Finite (Arrow (Discrete X))
    source
    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
    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
    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
      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
        @[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
        @[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
        theorem CategoryTheory.hasCardinalLT_of_hasCardinalLT_arrow {C : Type u} [Category.{v, u} C] {κ : Cardinal.{w}} (h : HasCardinalLT (Arrow C) κ) :
        HasCardinalLT C κ