ρ₂₃

Mathlib.Algebra.Homology.ComplexShapeSigns

URI: https://scilib.ai/kg/mathlib#ComplexShape.ρ₂₃

Lean4

/-- The `GradedObject.BifunctorComp₂₃IndexData` which arises from complex shapes. -/
@[reducible]
def ρ₂₃ : GradedObject.BifunctorComp₂₃IndexData (r c₁ c₂ c₃ c₁₂ c)
    where
  I₂₃ := I₂₃
  p := π c₂ c₃ c₂₃
  q := π c₁ c₂₃ c
  hpq := fun ⟨i₁, i₂, i₃⟩ ↦ (assoc c₁ c₂ c₃ c₁₂ c₂₃ c i₁ i₂ i₃).symm

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

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

Разделы

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

Аффилиация

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