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_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
      @[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
      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_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
        @[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
        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