lift_δ — Mathlib

English

For morphisms f: X ⟶ Y and g: X ⟶ Z in C, F.map (lift f g) ≫ δ F Y Z = lift (F.map f) (F.map g).

Русский

Для морфизмов f: X ⟶ Y и g: X ⟶ Z в C выполняется: F.map(lift f g) ; δ F Y Z = lift (F.map f) (F.map g).

LaTeX

$$$F.map(\mathrm{lift} f g) \;\; ≫\; δ F Y Z = \mathrm{lift}(F.map f)(F.map g)$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_δ (f : X ⟶ Y) (g : X ⟶ Z) : F.map (lift f g) ≫ δ F _ _ = lift (F.map f) (F.map g) := by
  ext <;> simp [← map_comp]

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