A cartesian closed category with zero object is trivial #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A cartesian closed category with zero object is trivial: it is equivalent to the category with one object and one morphism.
References #
noncomputable
def
category_theory.unique_homset_of_initial_iso_terminal
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
[category_theory.cartesian_closed C]
[category_theory.limits.has_initial C]
(i : ⊥_ C ≅ ⊤_ C)
(X Y : C) :
If a cartesian closed category has an initial object which is isomorphic to the terminal object, then each homset has exactly one element.
Equations
- category_theory.unique_homset_of_initial_iso_terminal i X Y = ((((category_theory.limits.prod.right_unitor X).symm.hom_congr (category_theory.iso.refl Y)).trans ((category_theory.limits.prod.map_iso (category_theory.iso.refl X) i.symm).hom_congr (category_theory.iso.refl Y))).trans ((category_theory.exp.adjunction X).hom_equiv (⊥_ C) Y)).unique
noncomputable
def
category_theory.unique_homset_of_zero
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
[category_theory.cartesian_closed C]
[category_theory.limits.has_zero_object C]
(X Y : C) :
If a cartesian closed category has a zero object, each homset has exactly one element.
Equations
noncomputable
def
category_theory.equiv_punit
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_finite_products C]
[category_theory.cartesian_closed C]
[category_theory.limits.has_zero_object C] :
A cartesian closed category with a zero object is equivalent to the category with one object and one morphism.
Equations
- category_theory.equiv_punit = category_theory.equivalence.mk (category_theory.functor.star C) (category_theory.functor.from_punit 0) (category_theory.nat_iso.of_components (λ (X : C), {hom := inhabited.default unique.inhabited, inv := inhabited.default unique.inhabited, hom_inv_id' := _, inv_hom_id' := _}) category_theory.equiv_punit._proof_3) ((category_theory.functor.from_punit 0 ⋙ category_theory.functor.star C).punit_ext (𝟭 (category_theory.discrete punit)))