inl_φ

Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp

URI: https://scilib.ai/kg/mathlib#CategoryTheory.kernelCokernelCompSequence.inl_φ

English

A left leg of the φ-map coincides with precomposition by f on the left leg.

Русский

Левая ножка отображения φ совместима с композициями слева через f.

LaTeX

$$biprod.inl \circ φ f g = f \circ biprod.inl$$

Lean4

@[reassoc (attr := simp)]
theorem inl_φ : biprod.inl ≫ φ f g = f ≫ biprod.inl := by simp [φ]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru