hom_inr_inl_false — Mathlib

English

Dually, there are no morphisms from an object in the right component to an object in the left component in the sum of two categories.

Русский

Соответственно, нет морфизмов от правой компоненты к левой в сумме категорий.

LaTeX

$$$$ \mathrm{Hom}(\mathrm{inr} X, \mathrm{inl} Y) = \emptyset. $$$$

Lean4

@[aesop norm -10 destruct (rule_sets := [CategoryTheory])]
theorem hom_inr_inl_false {X : C} {Y : D} (f : Sum.inr X ⟶ Sum.inl Y) : False := by cases f

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