hom_ext — Mathlib

English

Extensionality: two morphisms from mapBifunctor X j to Y are equal if they agree on all summands via ιMapBifunctor.

Русский

Экстensionalность: две морфизмы из mapBifunctor X j в Y равны, если они согласованы на всех суммандах через ιMapBifunctor.

LaTeX

$$ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ext f g := ∀ i₁ i₂ h, ιMapBifunctor ... ≡ ιMapBifunctor ...$$

Lean4

@[ext]
theorem hom_ext {Y : D} {j : J} {f g : (mapBifunctor K₁ K₂ F c).X j ⟶ Y}
    (h :
      ∀ (i₁ : I₁) (i₂ : I₂) (h : ComplexShape.π c₁ c₂ c ⟨i₁, i₂⟩ = j),
        ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ f = ιMapBifunctor K₁ K₂ F c i₁ i₂ j h ≫ g) :
    f = g :=
  HomologicalComplex₂.total.hom_ext _ h

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