precomp — Mathlib

English

A constructor for composable arrows of length 2 is obtained by precomposing the single arrow g with an arrow f: X0 → X1, yielding the composable arrows C 2.

Русский

Конструктор двух стрел для последовательности композиции получается как предопределение стрелы g через стрелу f: X0 → X1.

LaTeX

$$$$ \\text{mk}_2\\; f\\; g = (\\text{mk}_1\\; g).\\text{precomp}\\; f $$$$

Lean4

/-- "Precomposition" of `F : ComposableArrows C n` by a morphism `f : X ⟶ F.left`. -/
@[simps]
def precomp {X : C} (f : X ⟶ F.left) : ComposableArrows C (n + 1)
    where
  obj := Precomp.obj F X
  map g := Precomp.map F f _ _ (leOfHom g)
  map_id := Precomp.map_id F f
  map_comp g g' := Precomp.map_comp F f (leOfHom g) (leOfHom g')

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