congr_mk₁_map — Mathlib

English

If two morphisms f and g in a refl-quiver are identified by hx and hy and map to the same underlying arrow, then mk₁ applied to their images are equal.

Русский

Если две стрелки f и g в ReflQuiver идентифицируются через hx и hy и отображаются на одну и ту же стрелку, то mk₁ изображений равны.

LaTeX

$$$\text{If } f,g\text{ satisfy } hfg,\; \mathrm{mk}_1(F(f)) = \mathrm{mk}_1(F(g)).$$$

Lean4

theorem congr_mk₁_map {Y : Type u'} [ReflQuiver.{v'} Y] {C : Type u} [Category.{v} C]
    (F : ReflPrefunctor Y (ReflQuiv.of C)) {x₁ y₁ x₂ y₂ : Y} (f : x₁ ⟶ y₁) (g : x₂ ⟶ y₂) (hx : x₁ = x₂) (hy : y₁ = y₂)
    (hfg : Quiver.homOfEq f hx hy = g) :
    ComposableArrows.mk₁ (C := C) (F.map f) = ComposableArrows.mk₁ (C := C) (F.map g) := by subst hx hy hfg; rfl

Похожие утверждения