Documentation

Mathlib.CategoryTheory.ComposableArrows.Two

API for compositions of two arrows #

Given morphisms f : i ⟶ j, g : j ⟶ k, and fg : i ⟶ k in a category C such that f ≫ g = fg, we define maps twoδ₂Toδ₁ : mk₁ f ⟶ mk₁ fg and twoδ₁Toδ₀ : mk₁ fg ⟶ mk₁ g in the category ComposableArrows C 1. The names are justified by the fact that ComposableArrow.mk₂ f g can be thought of as a 2-simplex in the simplicial set nerve C, and its faces (numbered from 0 to 2) are respectively mk₁ g, mk₁ fg and mk₁ f.

source
@[reducible, inline]
abbrev CategoryTheory.ComposableArrows.twoδ₂Toδ₁ {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg := by cat_disch) :
mk₁ f ⟶ mk₁ fg

The morphism mk₁ f ⟶ mk₁ fg when f ≫ g = fg for some morphism g.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[reducible, inline]
    abbrev CategoryTheory.ComposableArrows.twoδ₁Toδ₀ {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg := by cat_disch) :
    mk₁ fg ⟶ mk₁ g

    The morphism mk₁ fg ⟶ mk₁ g when f ≫ g = fg for some morphism f.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) :
      (twoδ₂Toδ₁ f g fg h).app 0 = CategoryStruct.id ((mk₁ f).obj 0)
      source
      @[simp]
      theorem CategoryTheory.ComposableArrows.twoδ₂Toδ₁_app_one {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) :
      (twoδ₂Toδ₁ f g fg h).app 1 = g
      source
      @[simp]
      theorem CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_zero {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) :
      (twoδ₁Toδ₀ f g fg h).app 0 = f
      source
      @[simp]
      theorem CategoryTheory.ComposableArrows.twoδ₁Toδ₀_app_one {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) :
      (twoδ₁Toδ₀ f g fg h).app 1 = CategoryStruct.id ((mk₁ fg).obj 1)
      source
      instance CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₂Toδ₁ {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) [IsIso g] :
      IsIso (twoδ₂Toδ₁ f g fg h)
      source
      instance CategoryTheory.ComposableArrows.instIsIsoOfNatNatTwoδ₁Toδ₀ {C : Type u_1} [Category.{v_1, u_1} C] {i j k : C} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k) (h : CategoryStruct.comp f g = fg) [IsIso f] :
      IsIso (twoδ₁Toδ₀ f g fg h)
      source
      @[reducible, inline]
      abbrev CategoryTheory.ComposableArrows.twoδ₁Toδ₀' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) :
      mk₁ (homOfLE ⋯) ⟶ mk₁ (homOfLE hi₁₂)

      Variant of twoδ₁Toδ₀ for preorders.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[reducible, inline]
        abbrev CategoryTheory.ComposableArrows.twoδ₂Toδ₁' {ι : Type u_1} [Preorder ι] (i₀ i₁ i₂ : ι) (hi₀₁ : i₀ ≤ i₁) (hi₁₂ : i₁ ≤ i₂) :
        mk₁ (homOfLE hi₀₁) ⟶ mk₁ (homOfLE ⋯)

        Variant of twoδ₂Toδ₁ for preorders.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For