English
The full faithfulness of preadditive Yoneda and its transported variants yields that the preadditive Yoneda functor is full when composed with suitable whiskerings and forgetful functors.
Русский
Полнота и полнота предадитивной Yoneda сохраняется под композициями с подходящими whiskering и забывающими функторными преобразованиями.
LaTeX
$$$\text{preadditiveYoneda}$ is full after appropriate whiskering and forgetting$$
Lean4
theorem finrank_hom_simple_simple_eq_one_iff (X Y : C) [FiniteDimensional 𝕜 (X ⟶ X)] [FiniteDimensional 𝕜 (X ⟶ Y)]
[Simple X] [Simple Y] : finrank 𝕜 (X ⟶ Y) = 1 ↔ Nonempty (X ≅ Y) :=
by
fconstructor
· intro h
rw [finrank_eq_one_iff'] at h
obtain ⟨f, nz, -⟩ := h
rw [← isIso_iff_nonzero] at nz
exact ⟨asIso f⟩
· rintro ⟨f⟩
have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y
have zero_lt : 0 < finrank 𝕜 (X ⟶ Y) :=
finrank_pos_iff_exists_ne_zero.mpr ⟨f.hom, (isIso_iff_nonzero f.hom).mp inferInstance⟩
cutsat
