ιObj_naturality — Mathlib

English

The injection ιObj is natural in the sense that composing with a morphism φ on the left after ιObj is the same as composing with φ on the right before ιObj.

Русский

Вставка ιObj естественна: композиция слева с ιObj равна композиции справа перед ιObj.

LaTeX

$$$\\iota\\_{Obj}^{I,\\kappa}\\; f.hom \\;\$\\;\$ \\; = \\; f.left \\; \\iota\\_{Obj}^{I,\\kappa}\\; g.hom$$$

Lean4

@[reassoc (attr := simp)]
theorem ιObj_naturality {f g : Arrow C} (φ : f ⟶ g) : ιObj I κ f.hom ≫ objMap I κ φ = φ.left ≫ ιObj I κ g.hom :=
  Arrow.leftFunc.congr_map ((ιIteration I κ).naturality φ).symm

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