truncLEMap

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.truncLEMap

Lean4

/-- The morphism `K.truncLE e ⟶ L.truncLE e` induced by a morphism `K ⟶ L`. -/
noncomputable def truncLEMap : K.truncLE e ⟶ L.truncLE e :=
  (unopFunctor C c'.symm).map (truncGEMap ((opFunctor C c').map φ.op) e.op).op

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

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

Разделы

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

Аффилиация

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