π_comp_hom — Mathlib

English

For two multicoforks K1, K2 and a cocone morphism f: K1 ⟶ K2, the leg maps π b commute with f.hom, i.e., K1.π b ≫ f.hom = K2.π b for every b.

Русский

Для двух мультиифорков K1, K2 и морфизма косого конуса f: K1 ⟶ K2, операция π-столбцов сдвигается через f.hom: K1.π b ≫ f.hom = K2.π b для каждого b.

LaTeX

$$$\forall b,\ K_1.\pi b \;\gg\; f.hom = K_2.\pi b$$$

Lean4

@[reassoc (attr := simp)]
theorem π_comp_hom (K₁ K₂ : Multicofork I) (f : K₁ ⟶ K₂) (b : J.R) : K₁.π b ≫ f.hom = K₂.π b :=
  f.w _

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