functorP

Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ShortComplex.SnakeInput.functorP

Lean4

/-- The functor which sends `S : SnakeInput C` to the auxiliary object `S.P`,
which is `pullback S.L₁.g S.v₀₁.τ₃`. -/
@[simps]
noncomputable def functorP : SnakeInput C ⥤ C where
  obj S := S.P
  map f := pullback.map _ _ _ _ f.f₁.τ₂ f.f₀.τ₃ f.f₁.τ₃ f.f₁.comm₂₃.symm (congr_arg ShortComplex.Hom.τ₃ f.comm₀₁.symm)
  map_id _ := by dsimp [P]; simp
  map_comp _ _ := by dsimp [P]; cat_disch

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

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

Разделы

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

Аффилиация

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