leftDistributor_ext₂_left — Mathlib

English

Dually, if two morphisms from ⨁f ⊗ X to Y agree after postcomposing with biproduct injections, they are equal.

Русский

Аналогично слева: если два морфизма из ⨁f ⊗ X в Y совпадают после постсочетания с инъекторами двоичного двупродукта, то они равны.

LaTeX

$$$$\\big(\\forall j, (\\mathrm{biproduct}.\\mathrm{ι}_f j \\triangleright X) \\circ g = (\\mathrm{biproduct}.\\mathrm{ι}_f j \\triangleright X) \\circ h\\big) \\Rightarrow g = h,$$$$

Lean4

@[ext]
theorem leftDistributor_ext₂_left {J : Type} [Finite J] {X Y Z : C} {f : J → C} {g h : X ⊗ (Y ⊗ ⨁ f) ⟶ Z}
    (w : ∀ j, (X ◁ (Y ◁ biproduct.ι f j)) ≫ g = (X ◁ (Y ◁ biproduct.ι f j)) ≫ h) : g = h :=
  by
  apply (cancel_epi (α_ _ _ _).hom).mp
  ext
  simp [w]

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