# The left/right unitor equivalences `1 × C ≌ C` and `C × 1 ≌ C`. #

source
def CategoryTheory.prod.leftUnitor (C : Type u) [Category.{v, u} C] :
Functor (Discrete PUnit.{w + 1} × C) C

The left unitor functor `1 × C ⥤ C`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.prod.leftUnitor_obj (C : Type u) [Category.{v, u} C] (X : Discrete PUnit.{w + 1} × C) :
(leftUnitor C).obj X = X.2
source
@[simp]
theorem CategoryTheory.prod.leftUnitor_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : Discrete PUnit.{w + 1} × C} (f : X✝ ⟶ Y✝) :
(leftUnitor C).map f = f.2
source
def CategoryTheory.prod.rightUnitor (C : Type u) [Category.{v, u} C] :
Functor (C × Discrete PUnit.{w + 1}) C

The right unitor functor `C × 1 ⥤ C`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.prod.rightUnitor_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C × Discrete PUnit.{w + 1}} (f : X✝ ⟶ Y✝) :
(rightUnitor C).map f = f.1
source
@[simp]
theorem CategoryTheory.prod.rightUnitor_obj (C : Type u) [Category.{v, u} C] (X : C × Discrete PUnit.{w + 1}) :
(rightUnitor C).obj X = X.1
source
def CategoryTheory.prod.leftInverseUnitor (C : Type u) [Category.{v, u} C] :
Functor C (Discrete PUnit.{w + 1} × C)

The left inverse unitor `C ⥤ 1 × C`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.prod.leftInverseUnitor_obj (C : Type u) [Category.{v, u} C] (X : C) :
(leftInverseUnitor C).obj X = ({ as := PUnit.unit }, X)
source
@[simp]
theorem CategoryTheory.prod.leftInverseUnitor_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
(leftInverseUnitor C).map f = (CategoryStruct.id ({ as := PUnit.unit }, X✝).1, f)
source
def CategoryTheory.prod.rightInverseUnitor (C : Type u) [Category.{v, u} C] :
Functor C (C × Discrete PUnit.{w + 1})

The right inverse unitor `C ⥤ C × 1`

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.prod.rightInverseUnitor_obj (C : Type u) [Category.{v, u} C] (X : C) :
(rightInverseUnitor C).obj X = (X, { as := PUnit.unit })
source
@[simp]
theorem CategoryTheory.prod.rightInverseUnitor_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
(rightInverseUnitor C).map f = (f, CategoryStruct.id (X✝, { as := PUnit.unit }).2)
source
def CategoryTheory.prod.leftUnitorEquivalence (C : Type u) [Category.{v, u} C] :
Discrete PUnit.{w + 1} × C ≌ C

The equivalence of categories expressing left unity of products of categories.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.prod.leftUnitorEquivalence_counitIso (C : Type u) [Category.{v, u} C] :
(leftUnitorEquivalence C).counitIso = Iso.refl ((leftInverseUnitor C).comp (leftUnitor C))
source
@[simp]
theorem CategoryTheory.prod.leftUnitorEquivalence_inverse (C : Type u) [Category.{v, u} C] :
(leftUnitorEquivalence C).inverse = leftInverseUnitor C
source
@[simp]
theorem CategoryTheory.prod.leftUnitorEquivalence_functor (C : Type u) [Category.{v, u} C] :
(leftUnitorEquivalence C).functor = leftUnitor C
source
@[simp]
theorem CategoryTheory.prod.leftUnitorEquivalence_unitIso (C : Type u) [Category.{v, u} C] :
(leftUnitorEquivalence C).unitIso = Iso.refl (Functor.id (Discrete PUnit.{w + 1} × C))
source
def CategoryTheory.prod.rightUnitorEquivalence (C : Type u) [Category.{v, u} C] :
C × Discrete PUnit.{w + 1} ≌ C

The equivalence of categories expressing right unity of products of categories.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
@[simp]
theorem CategoryTheory.prod.rightUnitorEquivalence_inverse (C : Type u) [Category.{v, u} C] :
(rightUnitorEquivalence C).inverse = rightInverseUnitor C
source
@[simp]
theorem CategoryTheory.prod.rightUnitorEquivalence_counitIso (C : Type u) [Category.{v, u} C] :
(rightUnitorEquivalence C).counitIso = Iso.refl ((rightInverseUnitor C).comp (rightUnitor C))
source
@[simp]
theorem CategoryTheory.prod.rightUnitorEquivalence_unitIso (C : Type u) [Category.{v, u} C] :
(rightUnitorEquivalence C).unitIso = Iso.refl (Functor.id (C × Discrete PUnit.{w + 1}))
source
@[simp]
theorem CategoryTheory.prod.rightUnitorEquivalence_functor (C : Type u) [Category.{v, u} C] :
(rightUnitorEquivalence C).functor = rightUnitor C
source
instance CategoryTheory.prod.leftUnitor_isEquivalence (C : Type u) [Category.{v, u} C] :
(leftUnitor C).IsEquivalence
source
instance CategoryTheory.prod.rightUnitor_isEquivalence (C : Type u) [Category.{v, u} C] :
(rightUnitor C).IsEquivalence