freeMap_comp — Mathlib

English

For functors F: V₁ ⥤ V₂ and G: V₂ ⥤ V₃, the freeMap functor preserves composition: freeMap (F ⋙q G) = freeMap F ⋙ freeMap G.

Русский

Для функторов F: V₁ ⥤ V₂ и G: V₂ ⥤ V₃ свободная конструкция отображения сохраняет композицию: freeMap (F ⋙q G) = freeMap F ⋙ freeMap G.

LaTeX

$$$ \mathrm{freeMap}(F \circ G) = \mathrm{freeMap}(F) \circ \mathrm{freeMap}(G) $$$

Lean4

theorem freeMap_comp {V₁ : Type u₁} {V₂ : Type u₂} {V₃ : Type u₃} [Quiver.{v₁ + 1} V₁] [Quiver.{v₂ + 1} V₂]
    [Quiver.{v₃ + 1} V₃] (F : V₁ ⥤q V₂) (G : V₂ ⥤q V₃) : freeMap (F ⋙q G) = freeMap F ⋙ freeMap G :=
  Functor.ext_of_iso (freeMapCompIso F G) (fun _ ↦ rfl)

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