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.
def
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)
:
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
def
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)
:
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
@[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)
:
@[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)
:
@[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)
:
@[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)
:
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]
:
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]
: