hom_ext — Mathlib

English

Compatibility conditions ensure that composing the inclusion maps with the bifunctor maps yields coherent morphisms into the totalized object.

Русский

Условия совместимости гарантируют, что композиция включающих отображений с отображениями бифунктора даёт согласованные морфизмы во вплоть до итогового объекта.

LaTeX

$$$\\iota \\circ (\\text{mapBifunctor}) = (\\text{total map})$$$

Lean4

@[ext]
theorem hom_ext [HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] {j : ι₄} {A : C₄}
    {f g : (mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j ⟶ A}
    (hfg :
      ∀ (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j),
        ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ f = ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h ≫ g) :
    f = g :=
  GradedObject.mapBifunctor₁₂BifunctorMapObj_ext hfg

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