Documentation

TauCeti.CategoryTheory.Limits.Shapes.BinaryProducts

Binary products with a terminal object #

Mathlib's CategoryTheory.Limits.prod.leftUnitor and CategoryTheory.Limits.prod.rightUnitor identify ⊤_ C ⨯ X and X ⨯ ⊤_ C with X for the chosen terminal object ⊤_ C. This file gives the same identifications, natural in X, for an arbitrary terminal object T.

Main definitions #

source
noncomputable def CategoryTheory.Limits.IsTerminal.prodRightUnitor {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {T : C} (hT : IsTerminal T) :
prod.functor.flip.obj T ≅ Functor.id C

For a terminal object T, the projections X ⨯ T ⟶ X onto the first factor form a natural isomorphism (- ⨯ T) ≅ 𝟭 C.

Instances For
    source
    @[simp]
    theorem CategoryTheory.Limits.IsTerminal.prodRightUnitor_hom_app {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {T : C} (hT : IsTerminal T) (X : C) :
    hT.prodRightUnitor.hom.app X = prod.fst

    The component of prodRightUnitor at X is the first projection X ⨯ T ⟶ X.

    source
    @[simp]
    theorem CategoryTheory.Limits.IsTerminal.prodRightUnitor_inv_app {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {T : C} (hT : IsTerminal T) (X : C) :
    hT.prodRightUnitor.inv.app X = prod.lift (CategoryStruct.id X) (hT.from X)

    The inverse component of prodRightUnitor at X is prod.lift (𝟙 X) (hT.from X).

    source
    noncomputable def CategoryTheory.Limits.IsTerminal.prodLeftUnitor {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {T : C} (hT : IsTerminal T) :
    prod.functor.obj T ≅ Functor.id C

    For a terminal object T, the projections T ⨯ X ⟶ X onto the second factor form a natural isomorphism (T ⨯ -) ≅ 𝟭 C.

    Instances For
      source
      @[simp]
      theorem CategoryTheory.Limits.IsTerminal.prodLeftUnitor_hom_app {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {T : C} (hT : IsTerminal T) (X : C) :
      hT.prodLeftUnitor.hom.app X = prod.snd

      The component of prodLeftUnitor at X is the second projection T ⨯ X ⟶ X.

      source
      @[simp]
      theorem CategoryTheory.Limits.IsTerminal.prodLeftUnitor_inv_app {C : Type u} [Category.{v, u} C] [HasBinaryProducts C] {T : C} (hT : IsTerminal T) (X : C) :
      hT.prodLeftUnitor.inv.app X = prod.lift (hT.from X) (CategoryStruct.id X)

      The inverse component of prodLeftUnitor at X is prod.lift (hT.from X) (𝟙 X).