normalizeAux_nil_comp — Mathlib

English

In a free bicategory, normalizing along nil preserves composition: normalizeAux nil (f ∘ g) = normalizeAux nil f ∘ normalizeAux nil g.

Русский

В свободной би-категории нормализация по nil сохраняет композицию: normalizeAux nil (f ∘ g) = normalizeAux nil f ∘ normalizeAux nil g.

LaTeX

$$$normalizeAux(\\text{nil}, f \\circ g) = normalizeAux(\\text{nil}, f) \\circ normalizeAux(\\text{nil}, g)$$$

Lean4

theorem normalizeAux_nil_comp {a b c : B} (f : Hom a b) (g : Hom b c) :
    normalizeAux nil (f.comp g) = (normalizeAux nil f).comp (normalizeAux nil g) := by
  induction g generalizing a with
  | id => rfl
  | of => rfl
  | comp g _ ihf ihg => erw [ihg (f.comp g), ihf f, ihg g, comp_assoc]

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