CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages
theorem CategoryTheory.Abelian.OfCoimageImageComparisonIsIso.hasImages :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
[inst_4 : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.IsIso (CategoryTheory.Abelian.coimageImageComparison f)],
CategoryTheory.Limits.HasImages C
This theorem states that in a category with certain properties, if all coimage-image comparisons are isomorphisms, then the category has images. More precisely, the category must be preadditive and have kernels and cokernels. The coimage-image comparison for a morphism from one object to another in the category is defined as an isomorphism. In this context, an image is a particular kind of limit, and a coimage is a particular kind of colimit.
More concisely: In a preadditive category with kernels and cokernels, if the coimage-image comparisons are isomorphisms for all morphisms, then every morphism has a right adjoint, and hence the category has images and coimages.
|
CategoryTheory.Abelian.hasFiniteBiproducts
theorem CategoryTheory.Abelian.hasFiniteBiproducts :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
CategoryTheory.Limits.HasFiniteBiproducts C
This theorem states that in the field of category theory, if we have an abelian category `C`, then `C` has finite biproducts. Here, an abelian category is a concept in mathematics that generalizes some of the properties of abelian groups, such as the ability to take kernels and cokernels. A biproduct in an abelian category is a generalization of the direct sum of modules. So, this theorem is essentially saying that in such categories, we can define a finite biproduct.
More concisely: In an abelian category, finite biproducts exist.
|
CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization
theorem CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
[inst_2 : CategoryTheory.Limits.HasPushouts C] {W X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) (g₁ : X ⟶ W)
[inst_3 : CategoryTheory.Epi g₁] (g₂ : W ⟶ Z) [inst_4 : CategoryTheory.Mono g₂],
CategoryTheory.CategoryStruct.comp g₁ g₂ = g →
∀ (f' : W ⟶ Y),
CategoryTheory.CategoryStruct.comp g₁ f' = f →
∀ (t : CategoryTheory.Limits.PushoutCocone f g),
CategoryTheory.Limits.IsColimit t → CategoryTheory.Mono t.inl
The theorem `CategoryTheory.Abelian.mono_inl_of_factor_thru_epi_mono_factorization` states that in any abelian category with pushouts, if we have two morphisms `f` and `g` with a common domain, and if `g` can be factored into an epimorphism followed by a monomorphism, then if `f` can be factored through the epimorphism part of `g`, then the left morphism of any pushout cocone of `g` along `f` is a monomorphism. In simpler terms, it says that in this setting, if `f` can be factored through the initial part of a factorization of `g`, then any pushout of `g` along `f` results in a monomorphism. This is part of the abelian category theory and is used in further development of the theory.
More concisely: In an abelian category with pushouts, if a morphism can be factored through the epimorphic part of another morphism with a common domain, then the left morphism of the pushout along the first morphism is a monomorphism.
|
CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization
theorem CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
[inst_2 : CategoryTheory.Limits.HasPullbacks C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (g₁ : Y ⟶ W)
[inst_3 : CategoryTheory.Epi g₁] (g₂ : W ⟶ Z) [inst_4 : CategoryTheory.Mono g₂],
CategoryTheory.CategoryStruct.comp g₁ g₂ = g →
∀ (f' : X ⟶ W),
CategoryTheory.CategoryStruct.comp f' g₂ = f →
∀ (t : CategoryTheory.Limits.PullbackCone f g),
CategoryTheory.Limits.IsLimit t → CategoryTheory.Epi t.fst
The theorem `CategoryTheory.Abelian.epi_fst_of_factor_thru_epi_mono_factorization` states that in a category `C` which has pullbacks and is abelian, given two morphisms `f` and `g` from `X` and `Y` to `Z` respectively, if `g` can be factored into an epimorphism `g₁` followed by a monomorphism `g₂`, then if `f` factors through the mono part `g₂` of this factorization, any pullback of `g` along `f` will be an epimorphism. This theorem is essentially saying that under these conditions, pulling back along `f` preserves the property of being an epimorphism.
More concisely: In an abelian category with pullbacks, if a morphism `g` factors as an epimorphism followed by a monomorphism and another morphism `f` factors through the monomorphism, then the pullback of `g` along `f` is an epimorphism.
|