mapOfIsLimit_ι — Mathlib

English

Given an IsLimit structure on a kernel fork, a natural map between kernel forks respects the universal property.

Русский

Пусть дано структуру IsLimit на ядровой вилке; естественная карта между вилками сохраняет универсальное свойство.

LaTeX

$$$\\forall (kf:kernelfork\\;f) (kf':kernelfork\\;f'),\\ (hf':IsLimit\\;kf')\\ (\\varphi:\\mathrm{Arrow}(f)\\to \\mathrm{Arrow}(f')),\n\\; \\, \\text{Eq}(kf.mapOfIsLimit hf' \\varphi) \\;\\text{согласуется с } \\mathrm{ι}.$$$

Lean4

@[reassoc (attr := simp)]
theorem mapOfIsLimit_ι (kf : KernelFork f) {kf' : KernelFork f'} (hf' : IsLimit kf') (φ : Arrow.mk f ⟶ Arrow.mk f') :
    kf.mapOfIsLimit hf' φ ≫ kf'.ι = kf.ι ≫ φ.left :=
  hf'.fac _ _

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