CategoryTheory.shiftComm'
theorem CategoryTheory.shiftComm' :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
[inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i j : A),
(CategoryTheory.shiftFunctor C j).map ((CategoryTheory.shiftFunctor C i).map f) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.shiftComm X i j).hom
(CategoryTheory.CategoryStruct.comp
((CategoryTheory.shiftFunctor C i).map ((CategoryTheory.shiftFunctor C j).map f))
(CategoryTheory.shiftComm Y j i).hom)
The theorem `CategoryTheory.shiftComm'` states that, in a category `C` equipped with a shift operation indexed by an additive commutative monoid `A`, the operation of shifting commutes with itself. More explicitly, given two objects `X` and `Y` in the category `C`, a morphism `f : X ⟶ Y`, and two elements `i, j` of the additive monoid `A`, applying the shift functor to `f` and then shifting by `j` is equivalent to first shifting `f` by `j`, then composing with the commutativity isomorphism at `X` and `Y`, and finally shifting by `i`. This is a formalisation of the intuition that shifting should behave nicely with respect to the monoidal structure of the category.
More concisely: In a category with a shift operation indexed by an additive commutative monoid, shifting a morphism and then shifting by another element is equivalent to first shifting by the second element, then composing with the commutativity isomorphism, and finally shifting by the first element.
|
CategoryTheory.shiftFunctorAdd'_zero_add
theorem CategoryTheory.shiftFunctorAdd'_zero_add :
∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
[inst_2 : CategoryTheory.HasShift C A] (a : A),
CategoryTheory.shiftFunctorAdd' C 0 a a ⋯ =
(CategoryTheory.shiftFunctor C a).leftUnitor.symm.trans
(CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorZero C A).symm
(CategoryTheory.shiftFunctor C a))
The theorem `CategoryTheory.shiftFunctorAdd'_zero_add` states that for any category `C` with an associated shift and an additive monoid `A` with an element `a`, the composition of shifting by `0` and `a` (in the category `C`) is equivalent to the composition of the symmetric of the left unitor of the shift functor applied to `a` and the symmetric of the zero shift functor whiskered to the right of the shift functor applied to `a`. This essentially says that shifting by 0 and `a` is the same as shifting by `a` alone, reflecting the additive identity property of the monoid in the category-theoretic context.
More concisely: For any category with shift functor and additive monoid, shifting by 0 and an element a is equivalent to shifting by a alone.
|
CategoryTheory.shiftFunctorZero_hom_app_shift
theorem CategoryTheory.shiftFunctorZero_hom_app_shift :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
[inst_2 : CategoryTheory.HasShift C A] {X : C} (n : A),
(CategoryTheory.shiftFunctorZero C A).hom.app ((CategoryTheory.shiftFunctor C n).obj X) =
CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm C n 0).hom.app X)
((CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorZero C A).hom.app X))
This theorem states that for any type `C` and `A` where `C` forms a category, `A` forms an additive commutative monoid, and `C` has a shift operation with `A`, and any object `X` in `C` and element `n` in `A`, the application of the natural transformation induced by the homeomorphism `(CategoryTheory.shiftFunctorZero C A).hom` to the object `X` shifted by `n`, is equivalent to the composition of the application of the homeomorphism `(CategoryTheory.shiftFunctorComm C n 0).hom` to `X` and the morphism map of `X` shifted by `n` under the functor `(CategoryTheory.shiftFunctor C n)`. This describes a property of the zero-shift functor and shift functor in the context of Category Theory, showing how they interact with the composition operation in the category.
More concisely: For any category `C` with a shift operation and additive commutative monoid `A`, and for any object `X` in `C` and element `n` in `A`, the application of the zero-shift functor's natural transformation to `X` shifted by `n` is equivalent to composing the shift of `X` by `n` under the shift functor with the morphism of `X` shifted by `n` under the same functor.
|
CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd
theorem CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd :
∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
[inst_2 : CategoryTheory.HasShift C A] (i j : A),
CategoryTheory.shiftFunctorAdd' C i j (i + j) ⋯ = CategoryTheory.shiftFunctorAdd C i j
This theorem, `CategoryTheory.shiftFunctorAdd'_eq_shiftFunctorAdd`, states that for any type `C`, an additive monoid `A` and elements `i` and `j` from `A`, the operation of shifting functors with the sum `(i + j)` in category theory using the `shiftFunctorAdd'` function is equivalent to the operation of shifting functors with `i` and `j` separately using the `shiftFunctorAdd` function. Here, `C` is a type that has a predefined category structure, and `A` is a type with a predefined addition operation and an element called zero. The `HasShift` instance implies that the `C` category has a shift operation parameterized by the additive monoid `A`.
More concisely: For any type `C` with a category structure, additive monoid `A`, and shift functor `shiftFunctorAdd` in category theory, the composition of `shiftFunctorAdd` with the addition operation in `A` is equivalent to the repeated application of `shiftFunctorAdd` with the additive monoid elements.
|
CategoryTheory.ShiftMkCore.zero_add_hom_app
theorem CategoryTheory.ShiftMkCore.zero_add_hom_app :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
(self : CategoryTheory.ShiftMkCore C A) (n : A) (X : C),
(self.add 0 n).hom.app X =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((self.F n).map (self.zero.inv.app X))
The theorem `CategoryTheory.ShiftMkCore.zero_add_hom_app` states that for any category `C`, any additive monoid `A`, any `CategoryTheory.ShiftMkCore` instance on `C` and `A`, any element `n` of the add monoid `A`, and any object `X` in the category `C`, the application of the morphism obtained from adding zero to `n` through the `add` function of the `ShiftMkCore` instance to `X` equals the composition of the morphism from `X` to itself obtained by the `eqToHom` function and the morphism obtained by applying the `map` function on the functor associated with `n` in `ShiftMkCore` to the morphism obtained by applying the inverse of `zero` to `X`. In other words, this theorem confirms the preservation of the additive monoid structure under the shift operation in a categorical setting.
More concisely: For any additive monoid `A` and object `X` in a category with a `CategoryTheory.ShiftMkCore` instance, applying the shift morphism obtained by adding zero to an element `n` in `A` to `X` is equivalent to composing the identity morphism on `X` with the morphism obtained by applying the functor associated with `n` to the identity morphism on `X` via the inverse of zero.
|
CategoryTheory.shiftEquiv'.proof_1
theorem CategoryTheory.shiftEquiv'.proof_1 : ∀ {A : Type u_1} [inst : AddGroup A] (i j : A), i + j = 0 → j + i = 0 := by
sorry
This theorem, `CategoryTheory.shiftEquiv'.proof_1`, states that for any type `A` that forms an additive group, given any two elements `i` and `j` of `A`, if the sum of `i` and `j` equals zero, then the sum of `j` and `i` also equals zero. In other words, if `i` and `j` are such that `i + j = 0`, then `j + i = 0` also holds. This is a commutativity property in the context of an additive group.
More concisely: In an additive group, if `i` and `j` are elements with `i + j = 0`, then `j + i = 0`.
|
CategoryTheory.ShiftMkCore.add_zero_hom_app
theorem CategoryTheory.ShiftMkCore.add_zero_hom_app :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
(self : CategoryTheory.ShiftMkCore C A) (n : A) (X : C),
(self.add n 0).hom.app X =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (self.zero.inv.app ((self.F n).obj X))
This theorem, named `CategoryTheory.ShiftMkCore.add_zero_hom_app`, establishes the compatibility of the `add` operation with the right addition of zero in the context of category theory. Specifically, it states that for any category `C` of type `u`, an additive monoid `A` of type `u_1`, an instance `self` of `ShiftMkCore` for `C` and `A`, an element `n` of `A`, and an object `X` of `C`, the application of the morphism associated with the sum of `n` and `0` to `X` equals the composition of the morphism induced by a certain equality and the application of the inverse of the zero morphism to the object obtained by applying functor `(self.F n)` to `X`.
More concisely: For any additive monoid `A` and object `X` in a category `C` with an instance of `ShiftMkCore`, the application of the morphism associated with `n + 0` to `X` equals the composition of the identity morphism on `X` with the inverse of the zero morphism at `(self.F n) X`.
|
CategoryTheory.shiftFunctorAdd'_assoc
theorem CategoryTheory.shiftFunctorAdd'_assoc :
∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
[inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ a₁₂ a₂₃ a₁₂₃ : A) (h₁₂ : a₁ + a₂ = a₁₂) (h₂₃ : a₂ + a₃ = a₂₃)
(h₁₂₃ : a₁ + a₂ + a₃ = a₁₂₃),
(CategoryTheory.shiftFunctorAdd' C a₁₂ a₃ a₁₂₃ ⋯).trans
((CategoryTheory.isoWhiskerRight (CategoryTheory.shiftFunctorAdd' C a₁ a₂ a₁₂ h₁₂)
(CategoryTheory.shiftFunctor C a₃)).trans
((CategoryTheory.shiftFunctor C a₁).associator (CategoryTheory.shiftFunctor C a₂)
(CategoryTheory.shiftFunctor C a₃))) =
(CategoryTheory.shiftFunctorAdd' C a₁ a₂₃ a₁₂₃ ⋯).trans
(CategoryTheory.isoWhiskerLeft (CategoryTheory.shiftFunctor C a₁)
(CategoryTheory.shiftFunctorAdd' C a₂ a₃ a₂₃ h₂₃))
The theorem `CategoryTheory.shiftFunctorAdd'_assoc` states that, for any category `C` with a shift structure indexed by an additive monoid `A`, given any three elements `a₁`, `a₂` and `a₃` of `A`, and `a₁₂`, `a₂₃`, `a₁₂₃` denoting their possible sums, if the sum of `a₁` and `a₂` equals `a₁₂`, the sum of `a₂` and `a₃` equals `a₂₃`, and the sum of `a₁`, `a₂`, and `a₃` equals `a₁₂₃`, then the composition of the shift of `a₁₂` and `a₃` by `a₁₂₃`, followed by the whisker right morphism of the shift of `a₁` and `a₂` by `a₁₂` and the shift functor of `a₃`, and finally the associator of the shift functors of `a₁`, `a₂` and `a₃`, is equal to the composition of the shift of `a₁` and `a₂₃` by `a₁₂₃` followed by the whisker left morphism of the shift functor of `a₁` and the shift of `a₂` and `a₃` by `a₂₃`. This essentially captures the associativity property of the shift operation in the category.
More concisely: For any additive monoid `A` in a category `C` with a shift structure, the associativity of shift operators holds: (shift `a₁₂` by `a₁₂₃` then whisker right of shift `a₁` and `a₂` by `a₁₂` and shift `a₃`, followed by associator of shifts `a₁`, `a₂`, and `a₃`) equals (shift `a₁` by `a₁₂₃` then whisker left of shift `a₁` and `a₂` and `a₃` by `a₂₃`).
|
CategoryTheory.shift_shiftFunctorCompIsoId_hom_app
theorem CategoryTheory.shift_shiftFunctorCompIsoId_hom_app :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
[inst_2 : CategoryTheory.HasShift C A] (n m : A) (h : n + m = 0) (X : C),
(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).hom.app X) =
(CategoryTheory.shiftFunctorCompIsoId C m n ⋯).hom.app ((CategoryTheory.shiftFunctor C n).obj X)
This theorem states that for any objects `C` of type `u`, `A` of type `u_1`, where `C` is a category, `A` is an additive group and a shift operation is defined on `C` with `A`, for any elements `n` and `m` of `A` such that `n + m` equals to zero and any object `X` of `C`, the morphism obtained by applying the map of the shift functor `CategoryTheory.shiftFunctor C n` to the application of the homeomorphism of `CategoryTheory.shiftFunctorCompIsoId C n m` to `X`, is identical to the morphism obtained by applying the homeomorphism of `CategoryTheory.shiftFunctorCompIsoId C m n` to the object obtained from `X` by the object function of the shift functor `CategoryTheory.shiftFunctor C n`.
In simpler terms, in the context of category theory, this theorem shows a specific property of the shift functor, and its interplay with another construct, the shift functor composition isomorphism, when used in a particular order defined by the elements `n` and `m` of the additive group `A`, given that they add up to zero.
More concisely: For any additive group `A` and category `C`, if `n` and `m` are elements of `A` with `n + m = 0`, then the composition of the shift functor `CategoryTheory.shiftFunctor C n` with the shift functor composition isomorphism `CategoryTheory.shiftFunctorCompIsoId C n m` is equal to the composition of the shift functor composition isomorphism `CategoryTheory.shiftFunctorCompIsoId C m n` with the shift functor `CategoryTheory.shiftFunctor C m`.
|
CategoryTheory.shiftFunctorComm_eq
theorem CategoryTheory.shiftFunctorComm_eq :
∀ (C : Type u) {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddCommMonoid A]
[inst_2 : CategoryTheory.HasShift C A] (i j k : A) (h : i + j = k),
CategoryTheory.shiftFunctorComm C i j =
(CategoryTheory.shiftFunctorAdd' C i j k h).symm.trans (CategoryTheory.shiftFunctorAdd' C j i k ⋯)
This theorem states that for any type `C` forming a category and a type `A` forming an additive commutative monoid, along with a given shift structure on `C` with respect to `A`, and for any three elements `i`, `j`, `k` of `A` such that `i + j = k`, the shift functor commutativity for `C` and `i`, `j` is equal to the composition of the symmetrisation of the shift functor addition for `C`, `i`, `j`, `k` and the hypothesis `h`, and the shift functor addition for `C`, `j`, `i`, `k`. This theorem essentially describes a relation between the shift functor commutativity and shift functor addition in the context of category theory.
More concisely: For any category `C` with type `A` forming an additive commutative monoid, and a given shift structure, the shift functor commutativity for any elements `i`, `j` of `A` with `i + j = k` equals the composition of the symmetrized shift functor addition and the shift functor addition for `C` with respect to `i`, `j`, `k`.
|
CategoryTheory.ShiftMkCore.shiftFunctorZero_eq
theorem CategoryTheory.ShiftMkCore.shiftFunctorZero_eq :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
(h : CategoryTheory.ShiftMkCore C A), CategoryTheory.shiftFunctorZero C A = h.zero
This theorem asserts that for any category `C` and any additive monoid `A`, given the structure `h` of "having shifts" (`CategoryTheory.ShiftMkCore`) on `C` with respect to `A`, the shift functor at zero (`CategoryTheory.shiftFunctorZero C A`) is equal to the zero morphism in the structure `h`. In other words, in the context of category theory, shifting by zero in a category that supports shift operations is the same as applying the zero morphism.
More concisely: For any category with shifts `C` and additive monoid `A`, the shift functor at zero is equal to the zero morphism in the shifts structure.
|
CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq
theorem CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
(h : CategoryTheory.ShiftMkCore C A) (a b : A), CategoryTheory.shiftFunctorAdd C a b = h.add a b
This theorem, `CategoryTheory.ShiftMkCore.shiftFunctorAdd_eq`, states that for any two elements `a` and `b` from an additive monoid `A`, and given a shift-making core structure `h` in a category `C`, the result of applying the shift functor addition operation `shiftFunctorAdd` on `C`, `a`, and `b` is equal to the result of applying the `add` operation of `h` on `a` and `b`. Essentially, it provides an equivalence between the shift functor addition operation and the addition operation defined in the shift-making core structure in the context of category theory.
More concisely: For any additive monoid `A` and shift-making core structure `h` in a category `C`, the shift functor addition `shiftFunctorAdd h a b` is equal to the `add` operation applied to `a` and `b` in `h`.
|
CategoryTheory.ShiftMkCore.assoc_hom_app
theorem CategoryTheory.ShiftMkCore.assoc_hom_app :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
(self : CategoryTheory.ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C),
CategoryTheory.CategoryStruct.comp ((self.add (m₁ + m₂) m₃).hom.app X)
((self.F m₃).map ((self.add m₁ m₂).hom.app X)) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp ((self.add m₁ (m₂ + m₃)).hom.app X)
((self.add m₂ m₃).hom.app ((self.F m₁).obj X)))
This theorem, `CategoryTheory.ShiftMkCore.assoc_hom_app`, is about a compatibility condition in a category theory context involving shifts. The theorem states that for any Category `C` and any additive monoid `A`, and for any three elements `m₁`, `m₂`, `m₃` from `A` and an object `X` from `C`, the composition of the morphism associated with the sum of `m₁` and `m₂` and `m₃` and the map induced by the functor `F` applied to `m₃` on the hom-app of the sum of `m₁` and `m₂` is equal to the composition of an equality morphism and the composition of the hom-app of the sum of `m₁` and the sum of `m₂` and `m₃` and the hom-app of the sum of `m₂` and `m₃` applied to the object resulting from applying the functor `F` to `m₁`. This asserts a form of associativity on these compositions of morphisms, reflecting some underlying algebraic structure.
More concisely: For any additive monoid A, functor F from a category C to itself, and objects X, m₁, m₂, and m₃ in C, the following diagram commutes:
F(m₁ + m₂) ∘ (hom-app X (m₁ + m₂)) ��jours (eq.refl _) ∘ (hom-app X m₁) ∘ (hom-app X m₂) ∘ (hom-app (F X) m₃)
|
CategoryTheory.shiftFunctorAdd'.proof_1
theorem CategoryTheory.shiftFunctorAdd'.proof_1 :
∀ (C : Type u_1) {A : Type u_3} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : AddMonoid A]
[inst_2 : CategoryTheory.HasShift C A] (i j k : A),
i + j = k → CategoryTheory.shiftFunctor C k = CategoryTheory.shiftFunctor C (i + j)
This theorem states that for any type `C` in the context of category theory, given a type `A` that forms an additive monoid, and assuming that `C` has a shift structure over `A`, then for any three elements `i`, `j`, and `k` of `A`, if `i + j` equals `k`, then the shift functor applied to `C` and `k` is the same as the shift functor applied to `C` and `i + j`. In other words, the shift functor preserves the additive monoid structure of `A`.
More concisely: Given an additive monoid `A` and a category `C` with a shift structure over `A`, the shift functor commutes with addition of elements in `A`, i.e., for all `i`, `j`, `k` in `A` with `i + j = k`, we have `S(C[i]) ≈ S(C[j]) ≈ S(C[k])`, where `≈` denotes isomorphic objects in `C`.
|
CategoryTheory.shift_shiftFunctorCompIsoId_inv_app
theorem CategoryTheory.shift_shiftFunctorCompIsoId_inv_app :
∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
[inst_2 : CategoryTheory.HasShift C A] (n m : A) (h : n + m = 0) (X : C),
(CategoryTheory.shiftFunctor C n).map ((CategoryTheory.shiftFunctorCompIsoId C n m h).inv.app X) =
(CategoryTheory.shiftFunctorCompIsoId C m n ⋯).inv.app ((CategoryTheory.shiftFunctor C n).obj X)
This theorem states that for any categories `C` and `A` where `A` is an additive group and `C` has shift, given two elements `n` and `m` of `A` such that their sum is zero and any object `X` of `C`, the mapping of the inverse application of the compositional isomorphism `CategoryTheory.shiftFunctorCompIsoId` with respect to `n` and `m` under the shift functor `CategoryTheory.shiftFunctor` with respect to `n` is the same as the inverse application of the compositional isomorphism `CategoryTheory.shiftFunctorCompIsoId` with respect to `m` and `n` on the result of the action of the shift functor `CategoryTheory.shiftFunctor` with respect to `n` on the object `X`. This theorem is a part of the properties of the shift functor in category theory, particularly, it demonstrates the compatibility of shift functor with the compositional isomorphism under certain conditions.
More concisely: For any additive categories `C` with shift and group `A`, the shift functor commutes with the compositional isomorphism under zero-sum elements of `A`, i.e., `(CategoryTheory.shiftFunctorCompIsoId X n).inverse.comp (CategoryTheory.shiftFunctor X n) = (CategoryTheory.shiftFunctorCompIsoId X m).inverse.comp (CategoryTheory.shiftFunctor X m)` when `n + m = 0`.
|