The constant functor sending everything to punit.star.
Equations
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
- F.punit_ext G = category_theory.nat_iso.of_components (λ (_x : C), category_theory.eq_to_iso _) _
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.
def
category_theory.functor.from_punit
{C : Type u}
[category_theory.category C] :
C → category_theory.discrete punit ⥤ C
The functor from discrete punit sending everything to the given object.
Functors from discrete punit are equivalent to the category itself.
Equations
- category_theory.functor.equiv = {functor := {obj := λ (F : category_theory.discrete punit ⥤ C), F.obj punit.star, map := λ (F G : category_theory.discrete punit ⥤ C) (θ : F ⟶ G), θ.app punit.star, map_id' := _, map_comp' := _}, inverse := category_theory.functor.const (category_theory.discrete punit) _inst_1, unit_iso := category_theory.nat_iso.of_components (λ (X : category_theory.discrete punit ⥤ C), category_theory.discrete.nat_iso (λ (i : category_theory.discrete punit), punit.cases_on i (category_theory.iso.refl (((𝟭 (category_theory.discrete punit ⥤ C)).obj X).obj punit.star)))) category_theory.functor.equiv._proof_3, counit_iso := category_theory.nat_iso.of_components category_theory.iso.refl category_theory.functor.equiv._proof_4, functor_unit_iso_comp' := _}
@[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
@[simp]
@[simp]
theorem
category_theory.functor.equiv_functor_obj
{C : Type u}
[category_theory.category C]
(F : category_theory.discrete punit ⥤ C) :
@[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), punit.cases_on i (category_theory.iso.refl (((𝟭 (category_theory.discrete punit ⥤ C)).obj X).obj punit.star)))) category_theory.functor.equiv._proof_3
@[simp]
theorem
category_theory.functor.equiv_functor_map
{C : Type u}
[category_theory.category C]
(F G : category_theory.discrete punit ⥤ C)
(θ : F ⟶ G) :