Jacobson's lemma in a preadditive category

For morphisms a : X ⟶ Y and b : Y ⟶ X, the endomorphisms 𝟙 X - a ≫ b and 𝟙 Y - b ≫ a are invertible together. The inverse in one direction is obtained from the other by the formula (𝟙 Y - b ≫ a)⁻¹ = 𝟙 Y + b ≫ (𝟙 X - a ≫ b)⁻¹ ≫ a.

CategoryTheory.isIso_id_sub_comp_comm is the categorical form of Jacobson's lemma for rings. It applies even when the two morphisms have different sources and targets, and gives the left-right symmetry of the radical of a preadditive category.

theorem CategoryTheory.isIso_id_sub_comp_comm {C : Type u} [Category.{v, u} C] [Preadditive C] {X Y : C} (a : X ⟶ Y) (b : Y ⟶ X) : IsIso (CategoryStruct.id X - CategoryStruct.comp a b) ↔ IsIso (CategoryStruct.id Y - CategoryStruct.comp b a)

Jacobson's lemma: 𝟙 X - a ≫ b is invertible exactly when 𝟙 Y - b ≫ a is.