Documentation

Mathlib.CategoryTheory.Join.Sum

Embedding of C ⊕ D into C ⋆ D #

This file constructs a canonical functor Join.fromSum from C ⊕ D to C ⋆ D and give its characterization in terms of the canonical inclusions. We also provide Faithful and EssSurj instances on this functor.

source
def CategoryTheory.Join.fromSum (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] :
Functor (C ⊕ D) (Join C D)

The canonical functor from the sum to the join. It sends inl c to left c and inr d to right d.

Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Join.fromSum_obj (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (x✝ : C ⊕ D) :
      (fromSum C D).obj x✝ = match x✝ with | Sum.inl X => left X | Sum.inr X => right X
      source
      @[simp]
      theorem CategoryTheory.Join.fromSum_map_inl {C : Type u_1} (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] {c c' : C} (f : c ⟶ c') :
      (fromSum C D).map ((Sum.inl_ C D).map f) = (inclLeft C D).map f
      source
      @[simp]
      theorem CategoryTheory.Join.fromSum_map_inr (C : Type u_1) {D : Type u_2} [Category.{u_4, u_1} C] [Category.{u_3, u_2} D] {d d' : D} (f : d ⟶ d') :
      (fromSum C D).map ((Sum.inr_ C D).map f) = (inclRight C D).map f
      source
      def CategoryTheory.Join.inlCompFromSum (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] :
      (Sum.inl_ C D).comp (fromSum C D) ≅ inclLeft C D

      Characterization of fromSum with respect to the left inclusion.

      Equations
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Join.inlCompFromSum_inv_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (X : C) :
          (inlCompFromSum C D).inv.app X = CategoryStruct.id (left X)
          source
          @[simp]
          theorem CategoryTheory.Join.inlCompFromSum_hom_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (X : C) :
          (inlCompFromSum C D).hom.app X = CategoryStruct.id (left X)
          source
          def CategoryTheory.Join.inrCompFromSum (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] :
          (Sum.inr_ C D).comp (fromSum C D) ≅ inclRight C D

          Characterization of fromSum with respect to the right inclusion.

          Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Join.inrCompFromSum_inv_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (X : D) :
              (inrCompFromSum C D).inv.app X = CategoryStruct.id (right X)
              source
              @[simp]
              theorem CategoryTheory.Join.inrCompFromSum_hom_app (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (X : D) :
              (inrCompFromSum C D).hom.app X = CategoryStruct.id (right X)
              source
              instance CategoryTheory.Join.instEssSurjSumFromSum (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] :
              (fromSum C D).EssSurj
              source
              instance CategoryTheory.Join.instFaithfulSumFromSum (C : Type u_1) (D : Type u_2) [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] :
              (fromSum C D).Faithful