restrictionMap_f'

Mathlib.Algebra.Homology.Embedding.Restriction

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.restrictionMap_f'

← MathLib Explorer

English

For ψ : K ⟶ L.extend e, the morphism e.homRestrict ψ has a lift along e.

Русский

Для ψ: K ⟶ L.extend e, морфизм e.homRestrict ψ имеет подъем вдоль e.

LaTeX

$$$$ e.HasLift (e.homRestrict ψ) $$$$

Lean4

@[reassoc]
theorem restrictionMap_f' {i : ι} {i' : ι'} (hi : e.f i = i') :
    (restrictionMap φ e).f i = (K.restrictionXIso e hi).hom ≫ φ.f i' ≫ (L.restrictionXIso e hi).inv :=
  by
  subst hi
  simp [restrictionXIso]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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