CategoryTheory.Preadditive.exact_of_iso_of_exact'
theorem CategoryTheory.Preadditive.exact_of_iso_of_exact' :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasImages V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] [inst_3 : CategoryTheory.Preadditive V]
[inst_4 : CategoryTheory.Limits.HasKernels V] [inst_5 : CategoryTheory.Limits.HasCokernels V]
{A₁ B₁ C₁ A₂ B₂ C₂ : V} (f₁ : A₁ ⟶ B₁) (g₁ : B₁ ⟶ C₁) (f₂ : A₂ ⟶ B₂) (g₂ : B₂ ⟶ C₂) (α : A₁ ≅ A₂) (β : B₁ ≅ B₂)
(γ : C₁ ≅ C₂),
CategoryTheory.CategoryStruct.comp α.hom f₂ = CategoryTheory.CategoryStruct.comp f₁ β.hom →
CategoryTheory.CategoryStruct.comp β.hom g₂ = CategoryTheory.CategoryStruct.comp g₁ γ.hom →
CategoryTheory.Exact f₁ g₁ → CategoryTheory.Exact f₂ g₂
The theorem `CategoryTheory.Preadditive.exact_of_iso_of_exact'` states that in any preadditive category `V` with images, a zero object, kernels, and cokernels, for any objects `A₁`, `B₁`, `C₁`, `A₂`, `B₂`, `C₂` in `V` and morphisms `f₁` from `A₁` to `B₁`, `g₁` from `B₁` to `C₁`, `f₂` from `A₂` to `B₂`, `g₂` from `B₂` to `C₂`, along with isomorphisms `α` between `A₁` and `A₂`, `β` between `B₁` and `B₂`, `γ` between `C₁` and `C₂`, if the composition of `α.hom` and `f₂` equals the composition of `f₁` and `β.hom`, and the composition of `β.hom` and `g₂` equals the composition of `g₁` and `γ.hom`, and if `f₁` and `g₁` form an exact sequence, then `f₂` and `g₂` also form an exact sequence. In other words, exactness is preserved in this category under these conditions.
More concisely: In a preadditive category with images, a zero object, kernels, and cokernels, if isomorphisms `α: A₁ ≅ A₂`, `β: B₁ ≅ B₂`, `γ: C₁ ≅ C₂`, and `f₁ ◦ β = α ◦ f₂`, `β ◦ g₂ = g₁ ◦ γ` hold for morphisms `f₁: A₁ → B₁`, `g₁: B₁ → C₁`, `f₂: A₂ → B₂`, and `g₂: B₂ → C₂`, and `[f₁, g₁]` is an exact sequence, then `[f₂, g₂]` is also an exact sequence.
|
CategoryTheory.Preadditive.exact_iff_homology'_zero
theorem CategoryTheory.Preadditive.exact_iff_homology'_zero :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasImages V]
[inst_2 : CategoryTheory.Limits.HasZeroObject V] [inst_3 : CategoryTheory.Preadditive V]
[inst_4 : CategoryTheory.Limits.HasKernels V] [inst_5 : CategoryTheory.Limits.HasCokernels V] {A B C : V}
(f : A ⟶ B) (g : B ⟶ C),
CategoryTheory.Exact f g ↔ ∃ (w : CategoryTheory.CategoryStruct.comp f g = 0), Nonempty (homology' f g w ≅ 0)
The theorem `CategoryTheory.Preadditive.exact_iff_homology'_zero` states that for any preadditive category with objects `A`, `B`, and `C`, and morphisms `f` from `A` to `B` and `g` from `B` to `C`, the morphisms `f` and `g` are exactly composable if and only if the composition of `f` and `g` is equal to zero and there exists a homology of `f` and `g` that is isomorphic to zero. This theorem is relevant in the context of category theory, where it provides a condition for the exactness of two composable morphisms in a preadditive category.
More concisely: In a preadditive category, morphisms `f` from `A` to `B` and `g` from `B` to `C` are exactly composable if and only if their composition `g ∘ f` is zero and there exists an isomorphism of their homologies to the zero object.
|
CategoryTheory.exact_comp_mono_iff
theorem CategoryTheory.exact_comp_mono_iff :
∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasImages V] {A B C D : V}
{f : A ⟶ B} {g : B ⟶ C} {h : C ⟶ D} [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V]
[inst_3 : CategoryTheory.Limits.HasEqualizers V] [inst_4 : CategoryTheory.Mono h],
CategoryTheory.Exact f (CategoryTheory.CategoryStruct.comp g h) ↔ CategoryTheory.Exact f g
The theorem `CategoryTheory.exact_comp_mono_iff` states that for any category `V` with zero morphisms and equalizers, where `V` also has images, and for any objects `A`, `B`, `C`, and `D` in `V`, with morphisms `f : A ⟶ B`, `g : B ⟶ C`, and `h : C ⟶ D` such that `h` is a monomorphism, the composition of `f` and `g` followed by `h` (represented as `CategoryTheory.CategoryStruct.comp g h`) is exact if and only if `f` and `g` are exact.
In other words, the theorem establishes an equivalence between the exactness of the sequence `f`, `g` followed by `h` and the exactness of the sequence `f`, `g`, given that `h` is a monomorphism. Note that the dual of this theorem is only true when `V` is an abelian category.
More concisely: In a category with zero morphisms, equalizers, and images, given objects `A`, `B`, `C`, `D`, morphisms `f : A ⟶ B`, `g : B ⟶ C`, and `h : C ⟶ D` such that `h` is a monomorphism, the composition `h . g . f` is exact if and only if both `g . f` and `h` are exact.
|