mk₀_homEquiv₀_apply

Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.Ext.mk₀_homEquiv₀_apply

English

Applying mk₀ to the image under homEquiv₀ of f returns f; i.e., mk₀(homEquiv₀ f) = f.

Русский

Применяя mk₀ к образу под homEquiv₀ от f, получаем обратно f; то есть mk₀(homEquiv₀ f) = f.

LaTeX

$$$\\mathrm{mk_0}(\\mathrm{homEquiv}_0(f)) = f$$$

Lean4

@[simp]
theorem mk₀_homEquiv₀_apply (f : Ext X Y 0) : mk₀ (homEquiv₀ f) = f :=
  homEquiv₀.left_inv f

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

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

Разделы

Аффилиация

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