Documentation

Mathlib.CategoryTheory.Comma.CardinalArrow

Cardinal of Arrow #

We obtain various results about the cardinality of Arrow C. For example, If A 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.

Equations
    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
      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.

      Equations
        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.

          Equations
            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 κ