Documentation

Mathlib.CategoryTheory.GradedObject.Single

The graded object in a single degree #

In this file, we define the functor GradedObject.single j : C ⥤ GradedObject J C which sends an object X : C to the graded object which is X in degree j and the initial object of C in other degrees.

source
🔸 coverage
noncomputable def CategoryTheory.GradedObject.single {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) :
Functor C (GradedObject J C)

The functor which sends X : C to the graded object which is X in degree j and the initial object in other degrees.

Instances For
    source
    🔸 coverage
    @[reducible, inline]
    noncomputable abbrev CategoryTheory.GradedObject.single₀ (J : Type u_1) {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] [Zero J] :
    Functor C (GradedObject J C)

    The functor which sends X : C to the graded object which is X in degree 0 and the initial object in nonzero degrees.

    Instances For
      source
      🔸 coverage
      noncomputable def CategoryTheory.GradedObject.singleObjApplyIsoOfEq {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i = j) :
      (single j).obj X i ≅ X

      The canonical isomorphism (single j).obj X i ≅ X when i = j.

      Instances For
        source
        🔸 coverage
        @[reducible, inline]
        noncomputable abbrev CategoryTheory.GradedObject.singleObjApplyIso {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) :
        (single j).obj X j ≅ X

        The canonical isomorphism (single j).obj X j ≅ X.

        Instances For
          source
          🔸 coverage
          noncomputable def CategoryTheory.GradedObject.isInitialSingleObjApply {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i ≠ j) :
          Limits.IsInitial ((single j).obj X i)

          The object (single j).obj X i is initial when i ≠ j.

          Instances For
            source
            📐 coverage
            theorem CategoryTheory.GradedObject.singleObjApplyIsoOfEq_inv_single_map {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) (i : J) (h : i = j) :
            CategoryStruct.comp (singleObjApplyIsoOfEq j X i h).inv ((single j).map f i) = CategoryStruct.comp f (singleObjApplyIsoOfEq j Y i h).inv
            source
            📐 coverage
            theorem CategoryTheory.GradedObject.single_map_singleObjApplyIsoOfEq_hom {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) (i : J) (h : i = j) :
            CategoryStruct.comp ((single j).map f i) (singleObjApplyIsoOfEq j Y i h).hom = CategoryStruct.comp (singleObjApplyIsoOfEq j X i h).hom f
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) :
            CategoryStruct.comp (singleObjApplyIso j X).inv ((single j).map f j) = CategoryStruct.comp f (singleObjApplyIso j Y).inv
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (single j).obj Y j ⟶ Z) :
            CategoryStruct.comp (singleObjApplyIso j X).inv (CategoryStruct.comp ((single j).map f j) h) = CategoryStruct.comp f (CategoryStruct.comp (singleObjApplyIso j Y).inv h)
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) :
            CategoryStruct.comp ((single j).map f j) (singleObjApplyIso j Y).hom = CategoryStruct.comp (singleObjApplyIso j X).hom f
            source
            📐 coverage
            @[simp]
            theorem CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) :
            CategoryStruct.comp ((single j).map f j) (CategoryStruct.comp (singleObjApplyIso j Y).hom h) = CategoryStruct.comp (singleObjApplyIso j X).hom (CategoryStruct.comp f h)
            source
            🔸 coverage
            noncomputable def CategoryTheory.GradedObject.singleCompEval {J : Type u_1} (C : Type u_2) [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) :
            (single j).comp (eval j) ≅ Functor.id C

            The composition of the single functor single j : C ⥤ GradedObject J C and the evaluation functor eval j identifies to the identity functor.

            Instances For
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.GradedObject.singleCompEval_inv_app {J : Type u_1} (C : Type u_2) [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) :
              (singleCompEval C j).inv.app X = (singleObjApplyIso j X).inv
              source
              📐 coverage
              @[simp]
              theorem CategoryTheory.GradedObject.singleCompEval_hom_app {J : Type u_1} (C : Type u_2) [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) :
              (singleCompEval C j).hom.app X = (singleObjApplyIso j X).hom