Documentation

Mathlib.CategoryTheory.Products.Unitor

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

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

    Instances For
      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
      @[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
      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

      Instances For
        source
        @[simp]
        theorem CategoryTheory.prod.leftInverseUnitor_map (C : Type u) [Category.{v, u} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) :
        (leftInverseUnitor C).map f = Prod.mkHom (CategoryStruct.id { as := PUnit.unit }) f
        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
        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

        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 = Prod.mkHom f (CategoryStruct.id { as := PUnit.unit })
          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.

          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_functor (C : Type u) [Category.{v, u} C] :
            (leftUnitorEquivalence C).functor = 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_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.

            Instances For
              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_inverse (C : Type u) [Category.{v, u} C] :
              (rightUnitorEquivalence C).inverse = rightInverseUnitor 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