mapBifunctor₂₃Desc — Mathlib

English

There is a canonical morphism from the X j-component of the composite mapBifunctor to A, defined by a specified data f, and compatible with the underlying bifunctor structure.

Русский

Существует канонический морфизм из компоненты X_j композиции mapBifunctor в A, заданный данными f, и совместимый с базовой структурой бифункторa.

LaTeX

$$$\\text{mapBifunctor₂₃Desc}\\; c₁₂\\; f \; A$$$

Lean4

/-- Constructor for morphisms from
`(mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j`. -/
noncomputable def mapBifunctor₂₃Desc : (mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j ⟶ A :=
  GradedObject.mapBifunctorBifunctor₂₃Desc (ρ₂₃ := ComplexShape.ρ₂₃ c₁ c₂ c₃ c₁₂ c₂₃ c₄) f

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