mathlib3 documentation

category_theory.punit

The category discrete punit #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define star : C ⥤ discrete punit sending everything to punit.star, show that any two functors to discrete punit are naturally isomorphic, and construct the equivalence (discrete punit ⥤ C) ≌ C.

source
def category_theory.functor.star (C : Type u) [category_theory.category C] :
C ⥤ category_theory.discrete punit

The constant functor sending everything to punit.star.

Equations
source
@[simp]
theorem category_theory.functor.star_map_down_down (C : Type u) [category_theory.category C] (j j' : C) (f : j ⟶ j') :
_ = _
source
@[simp]
theorem category_theory.functor.punit_ext_inv_app {C : Type u} [category_theory.category C] (F G : C ⥤ category_theory.discrete punit) (X : C) :
(F.punit_ext G).inv.app X = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.functor.punit_ext_hom_app {C : Type u} [category_theory.category C] (F G : C ⥤ category_theory.discrete punit) (X : C) :
(F.punit_ext G).hom.app X = category_theory.eq_to_hom _
source
def category_theory.functor.punit_ext {C : Type u} [category_theory.category C] (F G : C ⥤ category_theory.discrete punit) :
F ≅ G

Any two functors to discrete punit are isomorphic.

Equations
source
theorem category_theory.functor.punit_ext' {C : Type u} [category_theory.category C] (F G : C ⥤ category_theory.discrete punit) :
F = G

Any two functors to discrete punit are equal. You probably want to use punit_ext instead of this.

source
@[reducible]
def category_theory.functor.from_punit {C : Type u} [category_theory.category C] (X : C) :
category_theory.discrete punit ⥤ C

The functor from discrete punit sending everything to the given object.

source
@[simp]
theorem category_theory.functor.equiv_inverse {C : Type u} [category_theory.category C] :
category_theory.functor.equiv.inverse = category_theory.functor.const (category_theory.discrete punit)
source
@[simp]
theorem category_theory.functor.equiv_unit_iso {C : Type u} [category_theory.category C] :
category_theory.functor.equiv.unit_iso = category_theory.nat_iso.of_components (λ (X : category_theory.discrete punit ⥤ C), category_theory.discrete.nat_iso (λ (i : category_theory.discrete punit), i.cases_on (λ (i : punit), i.cases_on (category_theory.iso.refl (((𝟭 (category_theory.discrete punit ⥤ C)).obj X).obj {as := punit.star}))))) category_theory.functor.equiv._proof_3
source
@[simp]
theorem category_theory.functor.equiv_functor_map {C : Type u} [category_theory.category C] (F G : category_theory.discrete punit ⥤ C) (θ : F ⟶ G) :
category_theory.functor.equiv.functor.map θ = θ.app {as := punit.star}
source
@[simp]
theorem category_theory.functor.equiv_counit_iso {C : Type u} [category_theory.category C] :
category_theory.functor.equiv.counit_iso = category_theory.nat_iso.of_components category_theory.iso.refl category_theory.functor.equiv._proof_4
source
def category_theory.functor.equiv {C : Type u} [category_theory.category C] :
category_theory.discrete punit ⥤ C ≌ C

Functors from discrete punit are equivalent to the category itself.

Equations
source
@[simp]
theorem category_theory.functor.equiv_functor_obj {C : Type u} [category_theory.category C] (F : category_theory.discrete punit ⥤ C) :
category_theory.functor.equiv.functor.obj F = F.obj {as := punit.star}
source
theorem category_theory.equiv_punit_iff_unique (C : Type u) [category_theory.category C] :
nonempty (C ≌ category_theory.discrete punit) ↔ nonempty C ∧ ∀ (x y : C), nonempty (unique (x ⟶ y))

A category being equivalent to punit is equivalent to it having a unique morphism between any two objects. (In fact, such a category is also a groupoid; see groupoid.of_hom_unique)