ιTruncLE

Mathlib.Algebra.Homology.Embedding.TruncLE

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.ιTruncLE

Lean4

/-- The canonical morphism `K.truncLE e ⟶ K` when `e` is an embedding of complex
shapes which satisfy `e.IsTruncLE`. -/
noncomputable def ιTruncLE : K.truncLE e ⟶ K :=
  (unopFunctor C c'.symm).map (K.op.πTruncGE e.op).op

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

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

Разделы

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

Аффилиация

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