LeanPool.DirectedTopologyLean4.MorphismAux #
theorem
eq_of_morphism
{C : CategoryTheory.Cat}
{a b₀ b₁ c : ↑C}
{f₀ : a ⟶ b₀}
{f₁ : a ⟶ b₁}
{g₀ : b₀ ⟶ c}
{g₁ : b₁ ⟶ c}
(hb : b₁ = b₀)
(hf : f₀ = CategoryTheory.CategoryStruct.comp f₁ (CategoryTheory.eqToHom hb))
(hg : g₀ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) g₁)
:
If we have two compositions a --f₀--> b₀ --g₀--> c and a --f₁--> b₁ --g₁--> c, where b₀ = b₀, f₀ = f₁ and g₀ = g₁, then f₀ ≫ g₀ = f₁ ≫ g₁
theorem
obj_eq_obj_of_eq
{C C' : CategoryTheory.Cat}
{F₁ F₂ : CategoryTheory.Functor ↑C ↑C'}
(h : F₁ = F₂)
(x : ↑C)
:
If two functors are equal, they map objects to the same image
theorem
map_eq_map_of_eq
{C C' : CategoryTheory.Cat}
{F₁ F₂ : CategoryTheory.Functor ↑C ↑C'}
(h : F₁ = F₂)
{x y : ↑C}
(f : x ⟶ y)
:
If two functors are equal, they map morphisms to the same image