CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up
theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₃_up :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), (CategoryTheory.ShortComplex.mk S.v₀₁.τ₃ S.v₁₂.τ₃ ⋯).Exact
This theorem states that the upper part of the third column of the snake diagram is exact in a category theory context. This is applicable for any type `C` that forms a category and is abelian. The exactness is established for a short complex created from the third morphisms (notated as `τ₃`) of the first and second complexes of a `SnakeInput`. In category theory, a sequence of objects and morphisms is said to be "exact" at a particular object if the image of the morphism to that object is equal to the kernel of the morphism from that object. In this case, the theorem asserts such a property for a specific part of the so-called "snake diagram".
More concisely: For any abelian category C, the sequence obtained from the third morphisms of the first and second complexes in a SnakeInput is exact.
|
CategoryTheory.ShortComplex.SnakeInput.L₀'_exact
theorem CategoryTheory.ShortComplex.SnakeInput.L₀'_exact :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), S.L₀'.Exact
The theorem `CategoryTheory.ShortComplex.SnakeInput.L₀'_exact` states that for any category `C`, which is an instance of the `CategoryTheory.Category` and `CategoryTheory.Abelian` typeclasses, and for any `S` which is an instance of `CategoryTheory.ShortComplex.SnakeInput` on `C`, the short complex `L₀'` associated with `S` is exact. In the language of category theory, a short complex is exact if the image of each morphism equals the kernel of the next morphism, meaning that the sequence of morphisms depicts an exact sequence.
More concisely: For any Abelian category `C` and an instance `S` of `CategoryTheory.ShortComplex.SnakeInput` on `C`, the associated short complex `L₀'` is an exact sequence of abelian group objects in `C`.
|
CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down
theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₂_down :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), (CategoryTheory.ShortComplex.mk S.v₁₂.τ₂ S.v₂₃.τ₂ ⋯).Exact
This theorem states that in the context of a category `C` that is Abelian, for any 'snake input' `S` in the short complex of `C`, the lower part of the second column of the snake diagram is exact. The exactness is constructed from the morphisms `S.v₁₂.τ₂` and `S.v₂₃.τ₂` using the `CategoryTheory.ShortComplex.mk` method. In the language of category theory, a sequence of objects and morphisms is said to be exact if the image of each morphism is equal to the kernel of the next.
More concisely: In an Abelian category `C`, the lower part of the second column in the snake diagram of any short exact sequence is exact, where exactness is defined as the image of each morphism being equal to the kernel of the next, constructed using the morphisms `τ₂` from the connecting homomorphisms `v₁₂` and `v₂₃` of the short complex.
|
CategoryTheory.ShortComplex.SnakeInput.L₀'.proof_1
theorem CategoryTheory.ShortComplex.SnakeInput.L₀'.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C),
CategoryTheory.CategoryStruct.comp S.L₁.f S.L₁.g = CategoryTheory.CategoryStruct.comp 0 S.v₀₁.τ₃
This theorem, named `CategoryTheory.ShortComplex.SnakeInput.L₀'.proof_1`, states that for any type `C` which is a Category and also an Abelian category, given a `SnakeInput` `S` in the category `C`, the composition of the morphisms `f` and `g` of the object `L₁` in the category is equal to the composition of the morphism 0 and the τ₃ component of the object `v₀₁` of `S`. This theorem is a part of the Snake Lemma in Category theory, often used in homological algebra.
More concisely: For any Abelian category `C` and `SnakeInput` `S` in `C`, the composition of morphisms `f` and `g` of the object `L₁` equals the composition of morphism `0` and the `τ₃` component of `v₀₁` of `S`.
|
CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP.proof_1
theorem CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP.proof_1 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C),
CategoryTheory.CategoryStruct.comp S.v₀₁.τ₂ S.L₁.g = CategoryTheory.CategoryStruct.comp S.L₀.g S.v₀₁.τ₃
The theorem `CategoryTheory.ShortComplex.SnakeInput.L₀X₂ToP.proof_1` states that for any category `C`, which is an abelian category, and a given short complex `S` in `C`, the composition of the morphisms `S.v₀₁.τ₂` and `S.L₁.g` is equal to the composition of the morphisms `S.L₀.g` and `S.v₀₁.τ₃`. In the context of category theory, this essentially means that we have commutativity between these two paths of morphisms in the short complex `S`.
More concisely: For any short complex `S` in an abelian category `C`, the compositions `S.v₀₁.τ₂ ∘ S.L₁.g` and `S.L₀.g ∘ S.v₀₁.τ₃` are equal.
|
CategoryTheory.ShortComplex.SnakeInput.Hom.ext
theorem CategoryTheory.ShortComplex.SnakeInput.Hom.ext :
∀ {C : Type u_1} {inst : CategoryTheory.Category.{u_2, u_1} C} {inst_1 : CategoryTheory.Abelian C}
{S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (x y : S₁.Hom S₂),
x.f₀ = y.f₀ → x.f₁ = y.f₁ → x.f₂ = y.f₂ → x.f₃ = y.f₃ → x = y
This theorem states that in the context of a category `C` that is also Abelian, for any two morphisms `x` and `y` between two objects `S₁` and `S₂` in the `SnakeInput` structure of the `ShortComplex` in the category `C`, if the first four components of `x` and `y` (specifically `x.f₀`, `x.f₁`, `x.f₂`, `x.f₃` and `y.f₀`, `y.f₁`, `y.f₂`, `y.f₃`) are equal, then `x` and `y` are equal.
More concisely: In an Abelian category `C`, if the first four components of two morphisms `x` and `y` in the `ShortComplex` of objects `S₁` and `S₂` have equal images under the `f₀`, `f₁`, `f₂`, and `f₃` functions, then `x` and `y` are equal.
|
CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down
theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₁_down :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), (CategoryTheory.ShortComplex.mk S.v₁₂.τ₁ S.v₂₃.τ₁ ⋯).Exact
This theorem states that for any category `C` of type `u_1` with properties `CategoryTheory.Category.{u_2, u_1} C` and `CategoryTheory.Abelian C`, and any short complex `S` of type `CategoryTheory.ShortComplex.SnakeInput C`, the lower part of the first column of the associated snake diagram is exact. Here, the term "exact" refers to the property in category theory that the image of one morphism is equal to the kernel of the next. The lower part of the first column of the snake diagram is constructed using `CategoryTheory.ShortComplex.mk` with `S.v₁₂.τ₁` and `S.v₂₃.τ₁` as arguments.
More concisely: For any Abelian category `C` with the structure of a Category, the lower part of the first column in the associated snake diagram of a short complex `S` is exact.
|
CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f
theorem CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.φ₁ S.L₂.f = S.φ₂
The theorem `CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f` states that for any category `C` that is also an Abelian category, and for any short complex `S` within that category, the composition of the canonical map `φ₁` with the map `S.L₂.f` is equal to the canonical map `φ₂`. In the language of category theory, this can be written as `φ₁ ∘ S.L₂.f = φ₂`. This theorem is fundamental to the definition of a short complex and its properties in the context of categories.
More concisely: For any short complex `S` in an Abelian category `C`, the composition of `S.L₂.f` with the canonical map `φ₁` equals the canonical map `φ₂`, i.e., `φ₁ ∘ S.L₂.f = φ₂`.
|
CategoryTheory.ShortComplex.SnakeInput.δ.proof_2
theorem CategoryTheory.ShortComplex.SnakeInput.δ.proof_2 :
∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C),
CategoryTheory.CategoryStruct.comp S.L₀'.f (CategoryTheory.CategoryStruct.comp S.φ₁ S.v₂₃.τ₁) = 0
This theorem states that for any category `C` of Abelian type, and any short complex `S`, the composition of the morphism `f` from the short complex `L₀'` of `S` and the composition of the canonical map `φ₁` from `S` and `τ₁` from the third step of `v₂₃` of `S` is equal to zero. In mathematical terms, this corresponds to the condition of exactness in a short exact sequence in the category of chain complexes, where the composition of certain morphisms results in the zero morphism.
More concisely: For any short complex `S` in an Abelian category `C`, the composition of the morphisms from the first complex in `S` to the third complex in `S` via `τ₁` and `φ₁`, and from the first complex in `S` to the second complex in `S` via `f` from the first complex in `L₀'`, is the zero morphism.
|
CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc
theorem CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₂ ⟶ Z),
CategoryTheory.CategoryStruct.comp S.φ₁ (CategoryTheory.CategoryStruct.comp S.L₂.f h) =
CategoryTheory.CategoryStruct.comp S.φ₂ h
The theorem `CategoryTheory.ShortComplex.SnakeInput.φ₁_L₂_f_assoc` states that for any category `C`, which is also an Abelian category, and given `S`, an object of type `CategoryTheory.ShortComplex.SnakeInput C`, and an arbitrary morphism `h` from `S.L₂.X₂` to `Z`, the composition of the canonical map `φ₁` with the composition of `S.L₂.f` and `h` is the same as the composition of the canonical map `φ₂` with `h`. In mathematical notation, this is saying that `(φ₁ ∘ (S.L₂.f ∘ h)) = (φ₂ ∘ h)`.
More concisely: For any Abelian category `C`, given an object `S` in `CategoryTheory.ShortComplex.SnakeInput C`, and a morphism `h` from `S.L₂.X₂` to `Z`, the composition of `φ₁` with `h` and `S.L₂.f` is equal to the composition of `φ₂` with `h`. That is, `(φ₁ ∘ h ∘ S.L₂.f) = (φ₂ ∘ h)`.
|
CategoryTheory.ShortComplex.SnakeInput.L₁'_exact
theorem CategoryTheory.ShortComplex.SnakeInput.L₁'_exact :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), S.L₁'.Exact
The theorem `CategoryTheory.ShortComplex.SnakeInput.L₁'_exact` states that for any type `C`, given it forms a category and is abelian, for any snake input `S` in the context of the short complex in category theory, the short complex `L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁` derived from `S` is exact. This means that the image of each morphism in the complex is equal to the kernel of the next morphism, a property important in the study of homological algebra.
More concisely: In an abelian category `C`, the short exact sequence `0 ⟶ L₀.X₂ ⟶ L₀.X₃ ⟶ L₃.X₁ ⟶ 0` derived from a snake input `S` in the short complex is exact.
|
CategoryTheory.ShortComplex.SnakeInput.L₂'_exact
theorem CategoryTheory.ShortComplex.SnakeInput.L₂'_exact :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), S.L₂'.Exact
This theorem states that for any category `C` that is an instance of the category theory and is Abelian, the short complex `S` generated from `C` satisfies the condition of exactness at `L₂'`. The exactness here refers to the specific property of category theory, where the image of one morphism equals the kernel of the next morphism, for the sequence `L₀.X₃ ⟶ L₃.X₁ ⟶ L₃.X₂`.
More concisely: In an Abelian category `C`, the short complex `S` generated from `C` is exact at degree 2.
|
CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up
theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₁_up :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), (CategoryTheory.ShortComplex.mk S.v₀₁.τ₁ S.v₁₂.τ₁ ⋯).Exact
This theorem, called `exact_C₁_up`, states that, for any given `SnakeInput` in the `ShortComplex` of a `CategoryTheory`, the upper part of the first column of the snake diagram is exact. This holds true for any category `C`, given that `C` is an abelian category. The theorem's proof involves constructing an exact sequence using the given `SnakeInput`. The exactness of the sequence is denoted by `(CategoryTheory.ShortComplex.mk S.v₀₁.τ₁ S.v₁₂.τ₁ ⋯).Exact`.
More concisely: In an abelian category, the upper part of the first column of a snake diagram for any given SnakeInput in a ShortComplex is exact.
|
CategoryTheory.ShortComplex.SnakeInput.L₀_exact
theorem CategoryTheory.ShortComplex.SnakeInput.L₀_exact :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), S.L₀.Exact
This theorem states that for any given category `C` of type `u_1`, where `C` is assumed to be a category in the sense of category theory and furthermore an Abelian category, and for a given short complex `S` defined on `C`, the zeroth term `L₀` of the short complex `S` is exact. In category theory, a complex is said to be exact at a term if the image of the morphism from the previous term equals the kernel of the morphism to the next term.
More concisely: In an Abelian category `C` of type `u_1`, the zeroth term of a given short complex `S` is exact, meaning the image of the morphism from the preceding term equals the kernel of the morphism to the next term.
|
CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down
theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), (CategoryTheory.ShortComplex.mk S.v₁₂.τ₃ S.v₂₃.τ₃ ⋯).Exact
This theorem states that, in the context of Abelian categories, the lower part of the third column of the snake diagram is exact. Here, the snake diagram is a specific diagram used in homological algebra, and "exact" refers to a certain property of sequences in category theory, specifically that the image of one morphism is the kernel of the next. The theorem takes as input a `SnakeInput` instance `S` (which presumably encapsulates some aspects of the diagram), and constructs a `ShortComplex` from parts of `S`, proving that this constructed sequence is exact.
More concisely: In the context of Abelian categories, the lower part of the snake diagram is exact.
|
CategoryTheory.ShortComplex.SnakeInput.snake_lemma
theorem CategoryTheory.ShortComplex.SnakeInput.snake_lemma :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), S.composableArrows.Exact
This theorem states that, for any given `SnakeInput` `S` in an Abelian category `C`, the sequence of morphisms `S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃` is exact. Here, `SnakeInput` represents a specific structure of objects and morphisms in the category `C`, and the exactness of the sequence implies that the image of each morphism is equal to the kernel of the next.
More concisely: For any object `S` in an Abelian category `C` with the structure of a `SnakeInput`, the sequence of morphisms `S.L₀.X₁ ⟶ S.L₀.X₂ ⟶ S.L₀.X₃ ⟶ S.L₃.X₁ ⟶ S.L₃.X₂ ⟶ S.L₃.X₃` is an exact sequence in `C`.
|
CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up
theorem CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
(S : CategoryTheory.ShortComplex.SnakeInput C), (CategoryTheory.ShortComplex.mk S.v₀₁.τ₂ S.v₁₂.τ₂ ⋯).Exact
This theorem, `CategoryTheory.ShortComplex.SnakeInput.exact_C₂_up`, states that for any `SnakeInput` `S` in a category `C` that is abelian, the upper part of the second column of the snake diagram constructed from `S` is exact. Here, "exact" refers to the property of a sequence in category theory where the image of one morphism equals the kernel of the next morphism. In this context, the sequence referenced is `(CategoryTheory.ShortComplex.mk S.v₀₁.τ₂ S.v₁₂.τ₂ ⋯)`.
More concisely: For any abelian category `C` and its `SnakeInput` `S`, the sequence obtained from `S` by taking the second column of the snake diagram is exact.
|