doc-next-gen

Mathlib.CategoryTheory.Products.Unitor

Module docstring

{"# The left/right unitor equivalences 1 × C ≌ C and C × 1 ≌ C. "}

CategoryTheory.prod.rightUnitor definition
: C × Discrete (PUnit : Type w) ⥤ C
Full source 
/-- The right unitor functor `C × 1 ⥤ C` -/
@[simps]
def rightUnitor : C × Discrete (PUnit : Type w)C × Discrete (PUnit : Type w) ⥤ C where
  obj X := X.1
  map f := f.1
Right unitor functor for product categories
Informal description
The right unitor functor maps an object $(X, \ast)$ in the product category $C \times \mathrm{Discrete}\,\{\ast\}$ to the object $X$ in $C$, and a morphism $(f, \mathrm{id}_{\ast})$ to the morphism $f$.
CategoryTheory.prod.leftInverseUnitor definition
: C ⥤ Discrete (PUnit : Type w) × C
Full source 
/-- The left inverse unitor `C ⥤ 1 × C` -/
@[simps]
def leftInverseUnitor : C ⥤ Discrete (PUnit : Type w) × C where
  obj X := ⟨⟨PUnit.unit⟩, X⟩
  map f := ⟨𝟙 _, f⟩
Left inverse unitor functor
Informal description
The functor from a category $C$ to the product category $1 \times C$, where $1$ is the discrete category on the unit type, defined by mapping each object $X$ in $C$ to the pair $(\mathrm{unit}, X)$ and each morphism $f$ to the pair $(\mathrm{id}_{\mathrm{unit}}, f)$.
CategoryTheory.prod.rightInverseUnitor definition
: C ⥤ C × Discrete (PUnit : Type w)
Full source 
/-- The right inverse unitor `C ⥤ C × 1` -/
@[simps]
def rightInverseUnitor : C ⥤ C × Discrete (PUnit : Type w) where
  obj X := ⟨X, ⟨PUnit.unit⟩⟩
  map f := ⟨f, 𝟙 _⟩
Right inverse unitor functor
Informal description
The functor from a category $C$ to the product category $C \times \mathrm{Discrete}\,(\mathrm{PUnit})$, which maps an object $X$ in $C$ to the pair $(X, \mathrm{PUnit}.\mathrm{unit})$ and a morphism $f$ in $C$ to the pair $(f, \mathrm{id})$.
CategoryTheory.prod.leftUnitorEquivalence definition
: Discrete (PUnit : Type w) × C ≌ C
Full source 
/-- The equivalence of categories expressing left unity of products of categories. -/
@[simps]
def leftUnitorEquivalence : DiscreteDiscrete (PUnit : Type w) × CDiscrete (PUnit : Type w) × C ≌ C where
  functor := leftUnitor C
  inverse := leftInverseUnitor C
  unitIso := Iso.refl _
  counitIso := Iso.refl _
Left unitor equivalence for product categories ($1 \times C \simeq C$)
Informal description
The equivalence of categories between the product category $1 \times C$ and $C$, where $1$ is the discrete category on the unit type. This equivalence consists of: - A functor from $1 \times C$ to $C$ that projects onto the second component (the left unitor functor) - An inverse functor from $C$ to $1 \times C$ that pairs each object with the unit object (the left inverse unitor functor) - Identity natural isomorphisms for both the unit and counit This equivalence expresses the left unity property of the categorical product with the unit category.
CategoryTheory.prod.rightUnitorEquivalence definition
: C × Discrete (PUnit : Type w) ≌ C
Full source 
/-- The equivalence of categories expressing right unity of products of categories. -/
@[simps]
def rightUnitorEquivalence : C × Discrete (PUnit : Type w)C × Discrete (PUnit : Type w) ≌ C where
  functor := rightUnitor C
  inverse := rightInverseUnitor C
  unitIso := Iso.refl _
  counitIso := Iso.refl _
Right unitor equivalence for product categories
Informal description
The equivalence of categories expressing right unity of products of categories, which establishes an equivalence between the product category $C \times \mathrm{Discrete}\,(\mathrm{PUnit})$ and $C$ itself. This equivalence consists of: - A functor mapping $(X, \ast)$ to $X$ (the right unitor functor) - An inverse functor mapping $X$ to $(X, \ast)$ (the right inverse unitor functor) - Identity natural isomorphisms for both the unit and counit