theorem SecondIsomorphism.kernelDesc_pullback_condition {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A B X : C} (f : A ⟶ X) (g : B ⟶ X) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.biprod.desc f g)) CategoryTheory.Limits.biprod.fst) f = CategoryTheory.CategoryStruct.comp (-CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.biprod.desc f g)) CategoryTheory.Limits.biprod.snd) g

For morphisms f : A ⟶ X and g : B ⟶ X in an abelian category, the two compositions out of kernel (biprod.desc f g) through the biproduct projections satisfy the pullback square condition (up to a sign on the second leg). This is the equation that lets us identify the kernel of f - g : A ⊕ B → X with the pullback A ×_X B.

noncomputable def SecondIsomorphism.pullbackIsoKernelOfDesc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A B X : C} (f : A ⟶ X) (g : B ⟶ X) : CategoryTheory.Limits.pullback f g ≅ CategoryTheory.Limits.kernel (CategoryTheory.Limits.biprod.desc f g)

For monomorphisms f : A ↪ X and g : B ↪ X in an abelian category, the pullback A ×_X B is canonically isomorphic to the kernel of biprod.desc f g : A ⊕ B ⟶ X. This is the standard identification of intersections of subobjects via biproducts.

theorem SecondIsomorphism.pullbackIsoKernelOfDesc_hom_ι {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A B X : C} (f : A ⟶ X) (g : B ⟶ X) : CategoryTheory.CategoryStruct.comp (pullbackIsoKernelOfDesc f g).hom (CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.biprod.desc f g)) = CategoryTheory.Limits.biprod.lift (CategoryTheory.Limits.pullback.fst f g) (-CategoryTheory.Limits.pullback.snd f g)

The forward direction of pullbackIsoKernelOfDesc, composed with the kernel inclusion, is the biproduct lift ⟨π₁, −π₂⟩ of the pullback projections.

theorem SecondIsomorphism.isPushout_pullback_image {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Abelian C] {A B X : C} (f : A ⟶ X) (g : B ⟶ X) [CategoryTheory.Mono f] [CategoryTheory.Mono g] : CategoryTheory.IsPushout (CategoryTheory.Limits.pullback.fst f g) (CategoryTheory.Limits.pullback.snd f g) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc f g))) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.Limits.factorThruImage (CategoryTheory.Limits.biprod.desc f g)))

Second isomorphism / pullback-pushout square. In an abelian category, for monomorphisms f : A ↪ X and g : B ↪ X, the square

A ×_X B ─→ A
   │        │
   ↓        ↓
   B ───→ image(f ⊕ g)

formed by the pullback projections and the canonical maps from A and B to the image of biprod.desc f g is a pushout. Equivalently, the image of A ⊕ B → X is the pushout A ⊔_{A ∩ B} B of subobjects, exhibiting the second isomorphism theorem at the level of subobjects of X.