CategoryTheory.ShortComplex.RightHomologyData.exact_iff
theorem CategoryTheory.ShortComplex.RightHomologyData.exact_iff :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} [inst_2 : S.HasHomology] (h : S.RightHomologyData),
S.Exact ↔ CategoryTheory.Limits.IsZero h.H
This theorem states that for any type `C` which forms a category with zero morphisms, and any `ShortComplex` `S` that has a homology, a `RightHomologyData` `h` of `S` implies that `S` is exact if and only if `h.H` is a zero object. In simpler terms, in a given short complex of a certain category, a certain right homology data is equivalent to zero if and only if the short complex is exact.
More concisely: A ShortComplex in a category with zero morphisms has zero right homology if and only if it is exact.
|
CategoryTheory.ShortComplex.Splitting.id
theorem CategoryTheory.ShortComplex.Splitting.id :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C} (self : S.Splitting),
CategoryTheory.CategoryStruct.comp self.r S.f + CategoryTheory.CategoryStruct.comp S.g self.s =
CategoryTheory.CategoryStruct.id S.X₂
The theorem `CategoryTheory.ShortComplex.Splitting.id` states that for any category `C` that is preadditive, and any short complex `S` in `C`, if `S` has a splitting `self`, then the composition of the retraction `self.r` with the morphism `S.f` plus the composition of the morphism `S.g` with the section `self.s` equals the identity morphism on the object `S.X₂`. In other words, it asserts the compatibility between the given section and retraction in the context of category theory.
More concisely: For any preadditive category `C` and short complex `S` with a splitting `self`, the composite of `self.r` with `S.f` and `S.g` with `self.s` equals the identity morphism on `S.X₂`.
|
CategoryTheory.ShortComplex.Exact.mono_g'
theorem CategoryTheory.ShortComplex.Exact.mono_g' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}, S.Exact → ∀ (h : S.RightHomologyData), CategoryTheory.Mono h.g'
This theorem states that for any category 'C' with zero morphisms, any short complex 'S' in 'C', and if 'S' is exact, then for any right homology data 'h' of 'S', the morphism 'g'' induced by 'S.g' and the fact that 'h.Q' is a cokernel of 'S.f' is a monomorphism. Essentially, in the context of category theory, this theorem shows that the particular morphism 'g'' is left-cancellative, i.e., for any morphisms 'f' and 'f'' such that 'g''∘f = g''∘f'', we have 'f = f'''. This result is related to the structure and properties of short complexes in category theory.
More concisely: In a category with zero morphisms, if a short exact complex has exact homology, then the induced morphism from the differential of a map that is a cokernel of another map is a monomorphism.
|
CategoryTheory.ShortComplex.exact_iff_of_iso
theorem CategoryTheory.ShortComplex.exact_iff_of_iso :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C}, (S₁ ≅ S₂) → (S₁.Exact ↔ S₂.Exact)
This theorem states that for any category 'C', which has zero morphisms, if there are two short complexes 'S₁' and 'S₂' defined over this category such that 'S₁' is isomorphic to 'S₂', then 'S₁' is exact if and only if 'S₂' is exact. Here, 'exact' refers to the property of a short complex in Category Theory, where the image of each morphism equals the kernel of the next.
More concisely: In any category with zero morphisms, two isomorphic short complexes are exact if and only if they both are.
|
CategoryTheory.ShortComplex.Exact.unop
theorem CategoryTheory.ShortComplex.Exact.unop :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex Cᵒᵖ}, S.Exact → S.unop.Exact
The theorem `CategoryTheory.ShortComplex.Exact.unop` states that for any type `C` that forms a category with zero morphisms, if `S` is a short complex in the opposite category `Cᵒᵖ` that is exact, then the unopposite of `S` (obtained by applying the `CategoryTheory.ShortComplex.unop` function) is also an exact short complex in `C`. In other words, the exactness property is preserved when switching from the opposite category to the original category.
More concisely: If `C` is a category with zero morphisms and `S` is an exact short complex in the opposite category `Cᵒᵖ`, then the unopposite `CategoryTheory.ShortComplex.unop S` is an exact short complex in `C`.
|
CategoryTheory.ShortComplex.Exact.mono_fromOpcycles
theorem CategoryTheory.ShortComplex.Exact.mono_fromOpcycles :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C},
S.Exact → ∀ [inst_2 : S.HasRightHomology], CategoryTheory.Mono S.fromOpcycles
This theorem states that for any category `C` that is preadditive, and for any short complex `S` in `C`, if `S` is exact and has right homology, then the morphism from the opposite cycles of `S` is a monomorphism. In the context of category theory, a category is preadditive if its hom-sets are equipped with an abelian group structure, a short complex is a sequence of objects and morphisms with certain properties, and a monomorphism is a morphism that is left-cancellable.
More concisely: In a preadditive category `C`, if a short exact and right-homologous complex `S` has a monomorphic opposite cycles morphism.
|
CategoryTheory.ShortComplex.exact_iff_epi
theorem CategoryTheory.ShortComplex.exact_iff_epi :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasZeroObject C],
S.g = 0 → (S.Exact ↔ CategoryTheory.Epi S.f)
This theorem states that in any preadditive category `C` with a zero object, for a given short complex `S` in `C`, if the map `S.g` is zero, then `S` is exact if and only if `S.f` is an epimorphism. Here, an exact short complex means that the image of `S.f` matches the kernel of `S.g`, and an epimorphism is a morphism where the condition of right-cancellation holds.
More concisely: In a preadditive category with a zero object, a short complex is exact if and only if its gap map is zero and its front map is an epimorphism.
|
CategoryTheory.ShortComplex.Exact.hasHomology
theorem CategoryTheory.ShortComplex.Exact.hasHomology :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}, S.Exact → S.HasHomology
This theorem states that for any type `C` that has a category structure (as specified by `CategoryTheory.Category`) and zero morphisms (as specified by `CategoryTheory.Limits.HasZeroMorphisms`), and for any short complex `S` of that category, if `S` is an exact sequence (as denoted by `CategoryTheory.ShortComplex.Exact S`), then `S` has homology (as denoted by `CategoryTheory.ShortComplex.HasHomology S`). In mathematical terms, this theorem is confirming the fundamental property of exact sequences in category theory, which ensures that the homology of any exact sequence is well defined.
More concisely: Any short exact sequence in a category with zero morphisms has well-defined homology.
|
CategoryTheory.ShortComplex.Exact.comp_descToInjective
theorem CategoryTheory.ShortComplex.Exact.comp_descToInjective :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C} (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [inst_2 : CategoryTheory.Injective J]
(hf : CategoryTheory.CategoryStruct.comp S.f f = 0),
CategoryTheory.CategoryStruct.comp S.g (hS.descToInjective f hf) = f
This theorem is part of category theory and states that for any category `C` which is also an Abelian category, and any short complex `S` in `C` that is exact, given morphism `f` from `S.X₂` to some object `J` in `C` (where `J` is injective), if the composition of `S.f` and `f` is the zero morphism, then the composition of `S.g` and the descriptor to injective of `hS`, `f`, and `hf` is `f`. Essentially, in the context of exact sequences in Abelian categories, this theorem outlines a particular compositional property of morphisms involving injective objects.
More concisely: In an Abelian category `C`, if `S` is an exact short complex, `f : S.X₂ → J` is a morphism with `J` injective, and `S.f ∘ f = 0`, then `f = S.g ∘ hS(f) ∘ hf`.
|
CategoryTheory.ShortComplex.quasiIso_iff_of_zeros'
theorem CategoryTheory.ShortComplex.quasiIso_iff_of_zeros' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
S₁.g = 0 →
∀ (hf₂ : S₂.f = 0),
S₂.g = 0 →
(CategoryTheory.ShortComplex.QuasiIso φ ↔
(CategoryTheory.ShortComplex.mk S₁.f φ.τ₂ ⋯).Exact ∧ CategoryTheory.Epi φ.τ₂)
The theorem states that given a morphism `φ` between two short complexes `S₁` and `S₂` in an abelian category, if the `g` map of `S₁` is zero (meaning `S₁` is in the form `S₁.X₁ ⟶ S₁.X₂ ⟶ 0`) and both the `f` and `g` maps of `S₂` are zero (meaning `S₂` is in the form `0 ⟶ S₂.X₂ ⟶ 0`), then `φ` is a quasi-isomorphism if and only if the obvious short complex `S₁.X₂ ⟶ S₁.X₂ ⟶ S₂.X₂` is exact and `φ.τ₂` is an epimorphism. In other words, the property of `φ` being a quasi-isomorphism is equivalent to the exactness of the constructed short complex and `φ.τ₂` being an epimorphism.
More concisely: A morphism between two short complexes in an abelian category is a quasi-isomorphism if and only if the corresponding complex of their middle terms is exact and the last map is an epimorphism.
|
CategoryTheory.ShortComplex.exact_of_g_is_cokernel
theorem CategoryTheory.ShortComplex.exact_of_g_is_cokernel :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C),
CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.g ⋯) →
∀ [inst_2 : S.HasHomology], S.Exact
The theorem `CategoryTheory.ShortComplex.exact_of_g_is_cokernel` states that for any category `C` (of type `u_1`), which has the structure of a category and is preadditive, given a short complex `S` in the category, if the morphism `S.g` determines a cokernel cofork that is a colimit, then `S` is exact. In other words, if the morphism `S.g` satisfies the universal property of a cokernel, the short complex `S` satisfies the exactness condition. This theorem is fundamental in homological algebra, where exact sequences and their properties are central topics. A short complex is exact when the image of each morphism is equal to the kernel of the next morphism. In the context of the theorem, this is expressed in terms of the cokernel of `S.g`.
More concisely: In a preadditive category `C`, a short complex `S` is exact if the morphism `S.g` determines a cokernel that is a colimit.
|
CategoryTheory.ShortComplex.exact_iff_isZero_homology
theorem CategoryTheory.ShortComplex.exact_iff_isZero_homology :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], S.Exact ↔ CategoryTheory.Limits.IsZero S.homology
The theorem `CategoryTheory.ShortComplex.exact_iff_isZero_homology` states that for any category `C` with zero morphisms and a given `ShortComplex` `S` on `C` with a defined homology, the `ShortComplex` `S` is exact if and only if the homology of `S` is zero. In categorical terms, this means that the sequence of morphisms in the `ShortComplex` is exact precisely when the homology group, calculated from the given sequence, is the zero object in the category.
More concisely: A ShortComplex in a category with zero morphisms is exact if and only if its homology is the zero object.
|
CategoryTheory.ShortComplex.exact_of_iso
theorem CategoryTheory.ShortComplex.exact_of_iso :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S₁ S₂ : CategoryTheory.ShortComplex C}, (S₁ ≅ S₂) → S₁.Exact → S₂.Exact
This theorem states that in any category `C` (with zero morphisms), if there is an isomorphism between two short complexes `S₁` and `S₂`, then `S₂` is exact whenever `S₁` is exact. In other words, exactness is preserved under isomorphism in the context of short complexes in a category. Here, a short complex is a specific type of diagram in category theory, and a complex is said to be exact if it satisfies certain conditions related to the objects and morphisms in the diagram.
More concisely: In any category with zero morphisms, the exactness of a short complex is preserved under isomorphism.
|
CategoryTheory.ShortComplex.Splitting.f_r
theorem CategoryTheory.ShortComplex.Splitting.f_r :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C} (self : S.Splitting),
CategoryTheory.CategoryStruct.comp S.f self.r = CategoryTheory.CategoryStruct.id S.X₁
The theorem `CategoryTheory.ShortComplex.Splitting.f_r` states that in the context of a category `C` that is preadditive, for any short complex `S` with a splitting `self`, the composition of the morphism `S.f` and the retraction `self.r` is equal to the identity morphism on the object `S.X₁`. In other words, `self.r` is a retraction of `S.f` in the category `C`.
More concisely: In a preadditive category `C`, for any short complex `S` with a splitting `self`, the retraction `self.r` of `S.f` is equal to the identity morphism on `S.X₁`.
|
CategoryTheory.ShortComplex.Exact.liftFromProjective_comp
theorem CategoryTheory.ShortComplex.Exact.liftFromProjective_comp :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{S : CategoryTheory.ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [inst_2 : CategoryTheory.Projective P]
(hf : CategoryTheory.CategoryStruct.comp f S.g = 0),
CategoryTheory.CategoryStruct.comp (hS.liftFromProjective f hf) S.f = f
This theorem is about the category theory in mathematics. It states that for any category `C` that is abelian, any short complex `S` that is exact, and any morphism `f` from a projective object `P` to the second object of the short complex `S`, if the composition of `f` with the morphism `g` from the short complex `S` is zero, then the composition of the lift from the projective `P` to `S` via `f` and the morphism `f` from the short complex `S` is equal to `f`.
In other words, we can imagine the objects and morphisms as forming a diagram, and this theorem is saying that if a certain square in this diagram commutes (i.e., the two different paths from `P` to `S.X₂` via `S.g` and `S.f` are equal), then a corresponding triangle also commutes.
More concisely: In an abelian category `C`, if a short exact sequence `S` has a projective object `P` and a morphism `f : P -> S.X₁` such that `S.g . f = 0`, then the lift of `f` to `S` is `f`.
|
CategoryTheory.ShortComplex.LeftHomologyData.exact_iff
theorem CategoryTheory.ShortComplex.LeftHomologyData.exact_iff :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} [inst_2 : S.HasHomology] (h : S.LeftHomologyData),
S.Exact ↔ CategoryTheory.Limits.IsZero h.H
This theorem states that for any category `C` (which is of type `u_1` and has zero morphisms) and any "short complex" `S` in this category (which has homology), the "short complex" `S` is "exact" (in the sense of category theory) if and only if the left homology data `h` of `S` is a zero object in the category `C`. In the context of category theory, a "short complex" is a specific kind of diagram of morphisms and objects, "exactness" is a property of such diagrams, and "homology" is a way to extract algebraic invariants from such diagrams.
More concisely: For any category C with zero morphisms and homology, a short complex S is exact if and only if its left homology data h is the zero object in C.
|
CategoryTheory.ShortComplex.Exact.epi_f'
theorem CategoryTheory.ShortComplex.Exact.epi_f' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}, S.Exact → ∀ (h : S.LeftHomologyData), CategoryTheory.Epi h.f'
The theorem `CategoryTheory.ShortComplex.Exact.epi_f'` states that for any category `C` that is preadditive and any short complex `S` that is exact, for any left homology data `h` of the short complex `S`, the morphism `f'` from the left homology data `h` is an epimorphism. In category theory, an epimorphism is a morphism f: X -> Y such that for all objects Z, and all morphisms g1, g2: Y -> Z, if g1 ∘ f = g2 ∘ f then g1 = g2. In the context of this theorem, it means that `f'` is "surjective" in a categorical sense.
More concisely: In a preadditive category `C` with exact short complexes, the morphism `f'` from the left homology data of an exact short complex is an epimorphism.
|
CategoryTheory.ShortComplex.exact_of_f_is_kernel
theorem CategoryTheory.ShortComplex.exact_of_f_is_kernel :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C),
CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯) →
∀ [inst_2 : S.HasHomology], S.Exact
The theorem `CategoryTheory.ShortComplex.exact_of_f_is_kernel` states that for any category `C` with a preadditive structure, and a short complex `S` in `C`, if `S.f` is a kernel (i.e., `CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι S.f ⋯)` holds), and `S` possesses a homology (`CategoryTheory.ShortComplex.HasHomology S`), then `S` is exact (`CategoryTheory.ShortComplex.Exact S`). In other words, in the context of category theory, this theorem guarantees exactness of a short complex if a certain morphism in the complex is a kernel and the complex has a homology.
More concisely: In a preadditive category `C`, a short complex `S` is exact if its morphism `S.f` is a kernel and `S` has homology.
|
Mathlib.Algebra.Homology.ShortComplex.Exact._auxLemma.1
theorem Mathlib.Algebra.Homology.ShortComplex.Exact._auxLemma.1 :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(X : C), CategoryTheory.Limits.IsZero X = (CategoryTheory.CategoryStruct.id X = 0)
This theorem, from the Mathematics Library in Algebra and Homology, states that for any type `C` which forms a category (with the category theory structure) and has zero morphisms, and for any object `X` in this category, the object `X` is considered as a "zero object" (i.e., both initial and terminal object, or an object having certain properties with respect to morphisms) if and only if the identity morphism on `X` is the zero morphism.
More concisely: A type `C` in a category with zero morphisms is the initial and terminal object if and only if its identity morphism is the zero morphism.
|
CategoryTheory.ShortComplex.HomologyData.exact_iff
theorem CategoryTheory.ShortComplex.HomologyData.exact_iff :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C} (h : S.HomologyData), S.Exact ↔ CategoryTheory.Limits.IsZero h.left.H
This theorem states that for any type `C` that forms a category with zero morphisms and any short complex `S` of `C`, the short complex `S` is exact if and only if the left homology of homology data `h` of `S` is zero. Here, exactness of a short complex refers to the property that the image of one morphism is equal to the kernel of the next morphism, and "zero homology" indicates that the homology at a particular point is trivial, i.e., isomorphic to the zero object of the category.
More concisely: For any short complex `S` in a category `C` with zero morphisms, `S` is exact if and only if its homology is zero.
|
CategoryTheory.ShortComplex.Exact.g_desc
theorem CategoryTheory.ShortComplex.Exact.g_desc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A)
(hk : CategoryTheory.CategoryStruct.comp S.f k = 0) [inst_3 : CategoryTheory.Epi S.g],
CategoryTheory.CategoryStruct.comp S.g (hS.desc k hk) = k
The theorem `CategoryTheory.ShortComplex.Exact.g_desc` states that for any category `C` which is preadditive and balanced, and any exact short complex `S` in this category, given an object `A` in `C` and a morphism `k` from `S.X₂` to `A` such that the composition of `S.f` and `k` is the zero morphism, if `S.g` is an epimorphism, then the composition of `S.g` and the description map of `S` with respect to `k` is equal to `k`. This theorem essentially describes a property of exact sequences in the context of category theory, specifically for short complexes.
More concisely: For any preadditive and balanced category `C`, exact short complex `S`, object `A` in `C`, and morphism `k` from `S.X₂` to `A` with `S.f ∘ k = 0` and `S.g` an epimorphism, `S.g ∘ S.desc(k) = k`.
|
CategoryTheory.ShortComplex.exact_of_isZero_X₂
theorem CategoryTheory.ShortComplex.exact_of_isZero_X₂ :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
(S : CategoryTheory.ShortComplex C), CategoryTheory.Limits.IsZero S.X₂ → S.Exact
This theorem states that for any short complex `S` in a category `C` that has zero morphisms, if the second object `X₂` of the short complex is a zero object, then the short complex `S` is exact. In the language of category theory, a short complex is a sequence of morphisms and objects that mimics the structure of a chain complex with only three nonzero terms. An exact short complex is one where the image of the morphism from the first object to the second object is equal to the kernel of the morphism from the second object to the third object. The condition that `X₂` is a zero object means that every morphism to `X₂` is a zero morphism and every morphism from `X₂` is a zero morphism.
More concisely: A short complex `S` in category `C` with zero morphisms is exact if its middle object `X₂` is a zero object.
|
CategoryTheory.ShortComplex.Splitting.s_g
theorem CategoryTheory.ShortComplex.Splitting.s_g :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C} (self : S.Splitting),
CategoryTheory.CategoryStruct.comp self.s S.g = CategoryTheory.CategoryStruct.id S.X₃
The theorem `CategoryTheory.ShortComplex.Splitting.s_g` states that for any category `C` with preadditive structure and any short complex `S` in `C`, if `s` is a splitting of `S`, then the composition of `s` and the morphism `S.g` is the identity morphism on the object `S.X₃`. In more mathematical terms, this theorem is stating the condition for `s` to be a right inverse (or section) of the morphism `S.g` in the category, i.e., `s` composed with `S.g` equals the identity morphism on `S.X₃`.
More concisely: For any short complex `S` in a preadditive category `C` and a morphism `s` that splits `S`, the composition `s ∘ S.g` equals the identity morphism on `S.X₃`.
|
CategoryTheory.ShortComplex.Exact.condition
theorem CategoryTheory.ShortComplex.Exact.condition :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}, S.Exact → ∃ h, CategoryTheory.Limits.IsZero h.left.H
This theorem states that for any category `C` that has zero morphisms, given a `ShortComplex` `S` in this category that is exact, there exists a homology data `h` such that the `left.H` field of `h` is a zero object. In the context of category theory, a zero object is an object that is both an initial object and a terminal object, and a zero morphism is a morphism that factors through a zero object.
More concisely: For any exact `ShortComplex` `S` in a category with zero morphisms, there exists homology data `h` such that the `left.H` object is a zero object.
|
CategoryTheory.ShortComplex.Splitting.exact
theorem CategoryTheory.ShortComplex.Splitting.exact :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Limits.HasZeroObject C], S.Splitting → S.Exact
The theorem `CategoryTheory.ShortComplex.Splitting.exact` states that for any category `C` (of a certain type `u_1`), which is also preadditive and has a zero object, any short complex `S` in `C` that is equipped with a splitting is exact. In simpler terms, it describes a property of short complexes in category theory - if a short complex has a certain structure called a "splitting", then it satisfies a property known as "exactness".
More concisely: In a preadditive category `C` with a zero object, any short complex `S` with a splitting is exact.
|
CategoryTheory.ShortComplex.Exact.op
theorem CategoryTheory.ShortComplex.Exact.op :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{S : CategoryTheory.ShortComplex C}, S.Exact → S.op.Exact
The theorem `CategoryTheory.ShortComplex.Exact.op` states that for any category `C` with zero morphisms, and a given short complex `S`, if `S` is exact, then the opposite short complex associated to `S` in the opposite category `Cᵒᵖ` is also exact. In other words, the exactness property is preserved under the operation of taking the opposite short complex.
More concisely: If `C` is a category with zero morphisms and `S` is a short complex in `C` that is exact, then the opposite short complex of `S` in the opposite category `Cᵒᵖ` is also exact.
|
CategoryTheory.ShortComplex.exact_map_iff_of_faithful
theorem CategoryTheory.ShortComplex.exact_map_iff_of_faithful :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C) [inst_4 : S.HasHomology]
(F : CategoryTheory.Functor C D) [inst_5 : F.PreservesZeroMorphisms] [inst_6 : F.PreservesLeftHomologyOf S]
[inst_7 : F.PreservesRightHomologyOf S] [inst_8 : F.Faithful], (S.map F).Exact ↔ S.Exact
This theorem states that for any two types `C` and `D` that are categories, if `C` and `D` have zero morphisms and `S` is a short complex in `C` with homology, and if `F` is a functor from `C` to `D` that preserves zero morphisms and both left and right homology of `S`, then if `F` is faithful (meaning it injectively maps morphisms), the short complex `S` is exact if and only if the short complex obtained by applying the functor `F` to `S` is exact. This theorem hence links the exactness of a short complex in a category with the exactness of the image of that short complex under a faithful functor in another category.
More concisely: For faithful functors preserving zero morphisms, zero homology, and exactness between two zero-morphism categories, the image of an exact short complex under the functor is exact.
|
CategoryTheory.ShortComplex.Exact.map
theorem CategoryTheory.ShortComplex.Exact.map :
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
[inst_1 : CategoryTheory.Category.{u_4, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S : CategoryTheory.ShortComplex C},
S.Exact →
∀ (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : F.PreservesLeftHomologyOf S]
[inst_6 : F.PreservesRightHomologyOf S], (S.map F).Exact
This theorem states that in the context of category theory, given a short complex `S` within category `C`, if `S` is exact, then for any functor `F` from `C` to another category `D` that preserves zero morphisms, left homology, and right homology, the short complex resulting from applying the functor `F` to `S` is also exact. This theorem holds for all types `C` and `D` that have the structure of a category and have zero morphisms.
More concisely: If `S` is a short exact sequence in a category `C` with zero morphisms and `F` is a functor from `C` to another category `D` preserving zero morphisms, left and right homologies, then `F(S)` is an exact sequence in `D`.
|
CategoryTheory.ShortComplex.quasiIso_iff_of_zeros
theorem CategoryTheory.ShortComplex.quasiIso_iff_of_zeros :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C]
{S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂),
S₁.f = 0 →
∀ (hg₁ : S₁.g = 0),
S₂.f = 0 →
(CategoryTheory.ShortComplex.QuasiIso φ ↔
(CategoryTheory.ShortComplex.mk φ.τ₂ S₂.g ⋯).Exact ∧ CategoryTheory.Mono φ.τ₂)
This theorem is stating that given a morphism `φ` between two short complexes `S₁` and `S₂` in an abelian category `C`, if the functions `S₁.f` and `S₁.g` are zero (such that `S₁` is of the form `0 ⟶ S₁.X₂ ⟶ 0`) and `S₂.f` is also zero (such that `S₂` is of the form `0 ⟶ S₂.X₂ ⟶ S₂.X₃`), then `φ` is a quasi-isomorphism if and only if the short complex formed by `S₁.X₂`, `S₂.X₂`, and `S₂.X₃` is exact and `φ.τ₂` is a monomorphism.
More concisely: Given morphisms φ between short complexes S₁ and S₂ in an abelian category C with zero terms S₁.X₂ and S₂.X₂, and zero morphisms S₁.f, S₁.g, and S₂.f, φ is a quasi-isomorphism if and only if the complex formed by S₁.X₂, S₂.X₂, and S₂.X₃ is exact and φ.τ₂ is a monomorphism.
|
CategoryTheory.ShortComplex.Exact.epi_toCycles
theorem CategoryTheory.ShortComplex.Exact.epi_toCycles :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C}, S.Exact → ∀ [inst_2 : S.HasLeftHomology], CategoryTheory.Epi S.toCycles
This theorem states that for any category `C` that has a preadditive structure (meaning that the category has an addition operation that satisfies some properties analogous to the addition of numbers), and for any short complex `S` in this category, if `S` is exact (which is a property of sequences of morphisms in category theory), then given that `S` has left homology, the morphism from `S` to its cycles is an epimorphism. In category theory, an epimorphism is a type of morphism that satisfies a certain property related to the factorization of morphisms.
More concisely: In any preadditive category with exact sequences and left homology, the morphism from a complex to its cycles is an epimorphism.
|
CategoryTheory.ShortComplex.exact_iff_mono
theorem CategoryTheory.ShortComplex.exact_iff_mono :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasZeroObject C],
S.f = 0 → (S.Exact ↔ CategoryTheory.Mono S.g)
This theorem states that for a given short complex `S` in a category `C`, which has a zero object and is preadditive, if the morphism `f` in `S` is equal to the zero morphism, then `S` is exact if and only if the morphism `g` in `S` is monic (i.e., a left-cancelable morphism). A short complex is a sequence of objects and morphisms in a category, and exactness is a property of such a sequence that pertains to certain equalities and kernel-cokernel relationships between the morphisms.
More concisely: In a preadditive category with a zero object, a short complex is exact if and only if every zero morphism in the complex is left-cancelable (monic).
|
CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f'
theorem CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f' :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C} [inst_2 : S.HasHomology] (h : S.LeftHomologyData),
S.Exact ↔ CategoryTheory.Epi h.f'
This theorem states that for any category `C` that is preadditive and any short complex `S` in `C` that has homology, given a left homology data `h` of `S`, the short complex `S` is exact if and only if the morphism `f'` in the left homology data `h` is an epimorphism. Here, a category is preadditive if it has a binary operation that is both associative and commutative, a short complex is a certain type of diagram in the category, homology is a type of mathematical object, 'exact' is a property of such diagrams, a left homology data is a specific type of mathematical structure associated with the diagram, and an epimorphism is a type of morphism in a category.
More concisely: In a preadditive category with homology, a short complex is exact if and only if the corresponding morphism in its left homology data is an epimorphism.
|
CategoryTheory.exact_iff_shortComplex_exact
theorem CategoryTheory.exact_iff_shortComplex_exact :
∀ {A : Type u_3} [inst : CategoryTheory.Category.{u_4, u_3} A] [inst_1 : CategoryTheory.Abelian A]
(S : CategoryTheory.ShortComplex A), CategoryTheory.Exact S.f S.g ↔ S.Exact
This theorem states that for any given abelian category `A` and any short complex `S` in that category, the notion of exactness as defined by `CategoryTheory.Exact` for the morphisms `S.f` and `S.g` of the short complex is equivalent to the exactness as defined by `S.Exact`. In other words, two different API definitions of exactness in the context of category theory and short complexes are effectively the same in the case of abelian categories.
More concisely: In an abelian category, the morphisms `f` and `g` of a short complex are exact according to `CategoryTheory.Exact` if and only if they are exact according to the complex's own definition `S.Exact`.
|
CategoryTheory.ShortComplex.Exact.lift_f
theorem CategoryTheory.ShortComplex.Exact.lift_f :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
{S : CategoryTheory.ShortComplex C} [inst_2 : CategoryTheory.Balanced C] (hS : S.Exact) {A : C} (k : A ⟶ S.X₂)
(hk : CategoryTheory.CategoryStruct.comp k S.g = 0) [inst_3 : CategoryTheory.Mono S.f],
CategoryTheory.CategoryStruct.comp (hS.lift k hk) S.f = k
This theorem, `CategoryTheory.ShortComplex.Exact.lift_f`, states that for any Category `C` (which is preadditive and balanced), given a Short Complex `S` that is exact, and a morphism `k` from an object `A` to `S.X₂` such that the composition of `k` with `S.g` is zero, if morphism `S.f` is monic (or injective), then the composition of `CategoryTheory.ShortComplex.Exact.lift` applied to `hS`, `k`, and `hk` with `S.f` is equal to `k`. In simpler terms, this theorem establishes a property of lifting morphisms in the context of exact sequences in category theory, specifically within short complexes.
More concisely: Given a preadditive and balanced category `C`, an exact short complex `S` in `C`, and a morphism `k` from an object to `S.X₂` with `S.g * k = 0` and monic `S.f`, the morphism `CategoryTheory.ShortComplex.Exact.lift(hS, k, hk) * S.f = k` holds.
|