CategoryTheory.Functor.preservesZeroMorphisms_of_map_exact
theorem CategoryTheory.Functor.preservesZeroMorphisms_of_map_exact :
∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A]
[inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Abelian A]
[inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B),
(∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g)) →
L.PreservesZeroMorphisms
This theorem states that if a functor 'L' from category 'A' to category 'B' preserves the exactness of morphisms, then it also preserves zero morphisms. Here, 'A' and 'B' are both assumed to be abelian categories. Essentially, if a morphism sequence is exact in category 'A', and its image under functor 'L' in category 'B' is also exact, then any zero morphism in 'A' is mapped to a zero morphism in 'B' by 'L'.
More concisely: If functor L from abelian category A to abelian category B preserves exact sequences, then it maps zero morphisms in A to zero morphisms in B.
|
CategoryTheory.Abelian.exact_iff_image_eq_kernel
theorem CategoryTheory.Abelian.exact_iff_image_eq_kernel :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z),
CategoryTheory.Exact f g ↔ CategoryTheory.Limits.imageSubobject f = CategoryTheory.Limits.kernelSubobject g
This theorem states that in an abelian category, a pair of morphisms, `f` from `X` to `Y` and `g` from `Y` to `Z`, is exact if and only if the image of `f` is equal to the kernel of `g`. Here, the image of `f` and the kernel of `g` are considered as subobjects of `Y`. The exactness of a sequence in an abelian category is a central concept in homological algebra and this theorem provides a characterization of it in terms of images and kernels of morphisms.
More concisely: In an abelian category, a morphism pair `(f : X → Y, g : Y → Z)` is exact if and only if `im(f) = ker(g)` as subobjects of `Y`.
|
CategoryTheory.Functor.preservesMonomorphisms_of_map_exact
theorem CategoryTheory.Functor.preservesMonomorphisms_of_map_exact :
∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A]
[inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Abelian A]
[inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B),
(∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g)) →
L.PreservesMonomorphisms
This theorem states that for any categories `A` and `B`, given `A` and `B` are both Abelian categories and `L` is a functor between `A` and `B`, if `L` preserves exact sequences from `A` to `B` (i.e., for any objects `X`, `Y`, and `Z` in `A` and morphisms `f : X ⟶ Y` and `g : Y ⟶ Z`, if `f` and `g` form an exact sequence in `A`, then their images under `L` form an exact sequence in `B`), then `L` also preserves monomorphisms. In other words, if a morphism is a monomorphism (injective) in `A`, its image under `L` is also a monomorphism in `B`.
More concisely: If `L` is a functor between Abelian categories `A` and `B` that preserves exact sequences, then `L` also preserves monomorphisms.
|
CategoryTheory.Abelian.isIso_cokernel_desc_of_exact_of_epi
theorem CategoryTheory.Abelian.isIso_cokernel_desc_of_exact_of_epi :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z) (ex : CategoryTheory.Exact f g) [inst_2 : CategoryTheory.Epi g],
CategoryTheory.IsIso (CategoryTheory.Limits.cokernel.desc f g ⋯)
In the context of an Abelian category, given three objects X, Y, Z, and morphisms `f : X ⟶ Y` and `g : Y ⟶ Z` such that `f` and `g` form an exact sequence (`ex : Exact f g`), if `g` is an epimorphism (`epi g`), then the cokernel descriptor of `f` and `g` is an isomorphism. This states a property about the structure of Abelian categories and the relationship between exact sequences, epimorphisms, and isomorphisms.
More concisely: In an Abelian category, if an exact sequence `X ⟶ Y ⟶ Z` has epimorphic last map `g : Y ⟶ Z`, then the cokernel of `f : X ⟶ Y` is isomorphic to `Z`.
|
CategoryTheory.Abelian.exact_iff
theorem CategoryTheory.Abelian.exact_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z),
CategoryTheory.Exact f g ↔
CategoryTheory.CategoryStruct.comp f g = 0 ∧
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.Limits.cokernel.π f) =
0
This theorem, `CategoryTheory.Abelian.exact_iff`, states that for any given category `C` with Abelian properties (`CategoryTheory.Abelian C`), and any three objects in the category: `X`, `Y`, `Z`, and any two morphisms `f: X ⟶ Y` and `g: Y ⟶ Z`, the sequence `f, g` is exact (i.e., `CategoryTheory.Exact f g`) if and only if two conditions are met:
1) The composition of `f` and `g` (i.e., `f ≫ g`) is a zero morphism, and
2) The composition of the map from the kernel of `g` to `X` and the map from `Y` to the cokernel of `f` (i.e., `CategoryTheory.Limits.kernel.ι g ≫ CategoryTheory.Limits.cokernel.π f`) is also a zero morphism.
In simpler terms, this theorem defines the exactness property in Abelian categories, which essentially states that the image of one morphism is the kernel of the next.
More concisely: In an Abelian category, a sequence of morphisms is exact if and only if its composition is zero and the composition of the kernel of the last morphism with the cokernel of the first morphism is zero.
|
CategoryTheory.Abelian.exact_epi_comp_iff
theorem CategoryTheory.Abelian.exact_epi_comp_iff :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C}
(f : X ⟶ Y) (g : Y ⟶ Z) {W : C} (h : W ⟶ X) [inst_2 : CategoryTheory.Epi h],
CategoryTheory.Exact (CategoryTheory.CategoryStruct.comp h f) g ↔ CategoryTheory.Exact f g
The theorem `CategoryTheory.Abelian.exact_epi_comp_iff` states that, for any category `C` that is also an Abelian category, given objects `X`, `Y`, `Z`, and `W` from `C` and morphisms `f : X ⟶ Y`, `g : Y ⟶ Z`, and `h : W ⟶ X` where `h` is an epimorphism, the statement "the composition of `h` and `f` is exact with `g`" is equivalent to the statement " `f` is exact with `g`". This theorem is highlighting a characteristic property of Abelian categories and is also valid in non-Abelian categories, as stated in `CategoryTheory.exact_comp_mono_iff`. In the context of category theory, an "exact sequence" is a sequence of morphisms between objects such that the image of one morphism equals the kernel of the next.
More concisely: In an Abelian category, for morphisms `f: X ⟶ Y`, `g: Y ⟶ Z`, and `h: W ⟶ X` with `h` an epimorphism, the composition `h ∘ f` is exact with `g` if and only if `f` is exact with `g`.
|
CategoryTheory.Functor.preservesEpimorphisms_of_map_exact
theorem CategoryTheory.Functor.preservesEpimorphisms_of_map_exact :
∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A]
[inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Abelian A]
[inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B),
(∀ ⦃X Y Z : A⦄ {f : X ⟶ Y} {g : Y ⟶ Z}, CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g)) →
L.PreservesEpimorphisms
This theorem states that for any two types `A` and `B` which form categories, if `A` and `B` are abelian, and we have a functor `L` mapping from `A` to `B`, then if this functor `L` preserves the exactness of sequences (`CategoryTheory.Exact f g` implies `CategoryTheory.Exact (L.map f) (L.map g)` for all `f` and `g`), it also preserves epimorphisms. In mathematical terms, a functor between abelian categories that preserves exact sequences also preserves epimorphisms. An epimorphism is a morphism that is right-cancellable, and exactness refers to a specific property of sequences in an abelian category.
More concisely: A functor between two abelian categories preserves epimorphisms if it preserves exact sequences.
|
CategoryTheory.Functor.map_exact
theorem CategoryTheory.Functor.map_exact :
∀ {A : Type u₁} {B : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} A]
[inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Abelian A]
[inst_3 : CategoryTheory.Abelian B] (L : CategoryTheory.Functor A B)
[inst_4 : CategoryTheory.Limits.PreservesFiniteLimits L]
[inst_5 : CategoryTheory.Limits.PreservesFiniteColimits L] {X Y Z : A} (f : X ⟶ Y) (g : Y ⟶ Z),
CategoryTheory.Exact f g → CategoryTheory.Exact (L.map f) (L.map g)
This theorem states that for any two types `A` and `B` that form categories, if `A` and `B` are Abelian categories, and `L` is a functor from `A` to `B` that preserves finite limits and finite colimits, then for any objects `X`, `Y`, and `Z` in `A` and morphisms `f : X ⟶ Y` and `g : Y ⟶ Z`, if `f` and `g` form an exact sequence in `A`, then their images under `L` also form an exact sequence in `B`. The reverse of this theorem also holds, as indicated by `Functor.preservesFiniteLimitsOfMapExact` and `Functor.preservesFiniteColimitsOfMapExact`.
More concisely: If functors L : A -> B between Abelian categories preserve finite limits and finite colimits, then for any exact sequence X ⟶ Y ⟶ Z in A, the image sequence L(X) ⟶ L(Y) ⟶ L(Z) is exact in B.
|