homRestrict_comp_extendMap

Mathlib.Algebra.Homology.Embedding.HomEquiv

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.homRestrict_comp_extendMap

Lean4

@[reassoc]
theorem homRestrict_comp_extendMap (ψ : K ⟶ L.extend e) (β : L ⟶ L') :
    e.homRestrict (ψ ≫ extendMap β e) = e.homRestrict ψ ≫ β :=
  by
  ext i
  simp [homRestrict_f _ _ rfl, extendMap_f β e rfl]

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

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

Разделы

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

Аффилиация

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