mapBifunctorMapObj_ext — Mathlib

English

The map described by mapBifunctorMapObjDesc commutes with the action of homs on X and Y.

Русский

Описание отображения через mapBifunctorMapObjDesc commute c действия гомоморфизмов на X и Y.

LaTeX

$$$\text{(mapBifunctorMapObjDesc F p X Y k)}(f) = \dots$$$

Lean4

@[ext]
theorem mapBifunctorMapObj_ext {X : GradedObject I C₁} {Y : GradedObject J C₂} {A : C₃} {k : K}
    [HasMap (((mapBifunctor F I J).obj X).obj Y) p] {f g : mapBifunctorMapObj F p X Y k ⟶ A}
    (h :
      ∀ (i : I) (j : J) (hij : p ⟨i, j⟩ = k),
        ιMapBifunctorMapObj F p X Y i j k hij ≫ f = ιMapBifunctorMapObj F p X Y i j k hij ≫ g) :
    f = g := by
  apply mapObj_ext
  rintro ⟨i, j⟩ hij
  exact h i j hij

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