rightDistributor_ext_right — Mathlib

English

If two maps from (⨁f) ⊗ Y to Z agree after composing with the projections/barycentric factors, then they are equal.

Русский

Если два отображения из (⨁f) ⊗ Y в Z совпадают после композиции с проекциями/распределителями, то они равны.

LaTeX

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

Lean4

@[ext]
theorem rightDistributor_ext_right {J : Type} [Finite J] {f : J → C} {X Y : C} {g h : X ⟶ (⨁ f) ⊗ Y}
    (w : ∀ j, g ≫ (biproduct.π f j ▷ Y) = h ≫ (biproduct.π f j ▷ Y)) : g = h := by
  classical
  cases nonempty_fintype J
  apply (cancel_mono (rightDistributor f Y).hom).mp
  ext
  simp [w]

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