CategoryTheory.Functor.congr_obj
theorem CategoryTheory.Functor.congr_obj :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D},
F = G → ∀ (X : C), F.obj X = G.obj X
This theorem states that for any two functors `F` and `G` from a category `C` to a category `D`, if `F` equals `G`, then the object `F.obj X` is equal to the object `G.obj X` for every object `X` in the category `C`. In other words, two equivalent functors map the same object in the domain category to the same object in the codomain category.
More concisely: For any functors F and G from a category C to a category D, if F is equal to G, then for all objects X in C, F.obj X = G.obj X.
|
CategoryTheory.congrArg_mpr_hom_right
theorem CategoryTheory.congrArg_mpr_hom_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y),
⋯.mpr p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
This theorem, `CategoryTheory.congrArg_mpr_hom_right`, states that in the context of a category `C` with objects `X`, `Y`, and `Z`, if we have a morphism `p` from `X` to `Y` and an equality `q` stating that `Z` is equal to `Y`, then an identity morphism on the target object `Y` of `p` can be replaced by a composition of `p` with `eqToHom` applied to `q`. However, it might be more advisable to introduce any necessary `eqToHom` morphisms manually rather than relying on this theorem to do so.
More concisely: In a category, given a morphism `p` from `X` to `Y` and an equality `q : Y ≡ Z`, the identity morphism on `Y` can be replaced by `p ∙ eqToHom q`.
|
CategoryTheory.eqToHom_refl
theorem CategoryTheory.eqToHom_refl :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C) (p : X = X),
CategoryTheory.eqToHom p = CategoryTheory.CategoryStruct.id X
This theorem states that for any category `C` and any object `X` in that category, the morphism obtained by applying the function `CategoryTheory.eqToHom` to the reflexive equality `p` (i.e., `X = X`) is equal to the identity morphism on `X`. In other words, in any given category, the morphism created by asserting the identity of an object with itself is indeed the identity morphism for that object.
More concisely: For any category `C` and object `X` in `C`, the morphism `CategoryTheory.eqToHom X X` equals the identity morphism `id X`.
|
CategoryTheory.congrArg_cast_hom_left
theorem CategoryTheory.congrArg_cast_hom_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z),
cast ⋯ q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
The theorem `CategoryTheory.congrArg_cast_hom_left` states that for any category `C` and objects `X`, `Y`, and `Z` within `C`, given an equality `p` between `X` and `Y` and a morphism `q` from `Y` to `Z`, the cast morphism of `q` is equal to the composition of the morphism obtained from the equality `p` and the morphism `q`. In other words, casting does not change the behavior of a morphism under composition with a morphism derived from an object equality.
More concisely: For any category C, given morphisms p : X ≈ Y and q : Y -> Z in C, the cast morphism of q along p equals the composition of p and q. In other words, p >.** q = q.cast (p : X -> Y).
|
CategoryTheory.congrArg_mpr_hom_left
theorem CategoryTheory.congrArg_mpr_hom_left :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y ⟶ Z),
⋯.mpr q = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) q
This theorem, `CategoryTheory.congrArg_mpr_hom_left`, states that in any category `C`, for any objects `X`, `Y`, and `Z`, given an equality `p : X = Y` and a morphism `q : Y ⟶ Z`, we can replace any term that is the morphism `q` applied to some object (obtained through equational rewriting on the source object of the morphism) with a composition of the morphism derived from the equality `p` (`CategoryTheory.eqToHom p`) and the morphism `q`. The theorem suggests it might be better to manually introduce any necessary morphisms from equalities rather than relying on this result.
More concisely: In any category, given an equality between objects and a morphism, the morphism applied to the equal object can be replaced by the composition of the morphism derived from the equality and the given morphism.
|
CategoryTheory.eqToHom_trans
theorem CategoryTheory.eqToHom_trans :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z),
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.eqToHom q) =
CategoryTheory.eqToHom ⋯
The theorem `CategoryTheory.eqToHom_trans` states that for any category `C` and for any three objects `X`, `Y`, and `Z` in `C`, if we have two equalities `p: X = Y` and `q: Y = Z`, then the composition of the morphisms obtained from these equalities via the `eqToHom` function, i.e., `CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p) (CategoryTheory.eqToHom q)`, is equal to the morphism obtained from the transitivity of `p` and `q` using the `eqToHom` function. In other words, this theorem is a statement about the compatibility of the `eqToHom` function with the transitivity of equalities in a category.
More concisely: For any category `C` and objects `X`, `Y`, and `Z` with equalities `p: X = Y` and `q: Y = Z`, the composition of morphisms `CategoryTheory.eqToHom p` and `CategoryTheory.eqToHom q` is equal to `CategoryTheory.eqToHom (p &&& q)`, where `&&&` represents the function composition in Lean.
|
CategoryTheory.eqToHom_op
theorem CategoryTheory.eqToHom_op :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (h : X = Y),
(CategoryTheory.eqToHom h).op = CategoryTheory.eqToHom ⋯
The theorem `CategoryTheory.eqToHom_op` states that for any category 'C' and any two objects 'X' and 'Y' in 'C' such that 'X' equals 'Y' (denoted by 'h : X = Y'), the opposite morphism of the morphism from 'X' to 'Y' obtained through the function `CategoryTheory.eqToHom` using the equality 'h', is equal to the morphism obtained by applying `CategoryTheory.eqToHom` to some equality (suppressed for brevity). This means that the operation of taking the opposite does not change the morphism given by the equality between objects in the category.
More concisely: For any category 'C' and objects 'X' and 'Y' with 'X = Y', the opposite morphisms of `CategoryTheory.eqToHom X Y` are equal.
|
CategoryTheory.eqToHom_unop
theorem CategoryTheory.eqToHom_unop :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (h : X = Y),
(CategoryTheory.eqToHom h).unop = CategoryTheory.eqToHom ⋯
The theorem `CategoryTheory.eqToHom_unop` states that for any category `C` and any two objects `X` and `Y` in the opposite category `Cᵒᵖ`, given an equality `h : X = Y`, the unopposite of the morphism from `X` to `Y` in `Cᵒᵖ` obtained through `CategoryTheory.eqToHom h` is equal to the morphism from `X` to `Y` in the category `C` obtained by applying `CategoryTheory.eqToHom` to this equality after applying an unspecified operation. Essentially, the theorem connects the morphisms obtained from equalities in a category and its opposite.
More concisely: For any category `C` and objects `X` and `Y` in `Cᵒᵖ`, the unopposite morphism from `X` to `Y` in `Cᵒᵖ` obtained from an equality `h : X = Y` is equal to the morphism from `X` to `Y` in `C` obtained by applying `CategoryTheory.eqToHom` to `h`.
|
CategoryTheory.Functor.ext
theorem CategoryTheory.Functor.ext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D}
(h_obj : ∀ (X : C), F.obj X = G.obj X),
autoParam
(∀ (X Y : C) (f : X ⟶ Y),
F.map f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
(CategoryTheory.CategoryStruct.comp (G.map f) (CategoryTheory.eqToHom ⋯)))
_auto✝ →
F = G
This theorem, `CategoryTheory.Functor.ext`, states that for two functors `F` and `G` from a category `C` to a category `D`, if for all objects `X` in `C`, `F.obj X` equals `G.obj X`, and if for all objects `X`, `Y` in `C` and morphism `f` from `X` to `Y`, the mapping of `f` by `F` equals the composition of the morphism induced by the equality between `F.obj X` and `G.obj X`, the mapping of `f` by `G`, and the morphism induced by the equality between `F.obj Y` and `G.obj Y`, then the two functors `F` and `G` are equal. The second condition is implicitly provided by an `autoParam`, a mechanism that provides default arguments during elaboration. It's important to note that this isn't an extensionality lemma, because in most cases, proving equality between functors is not desirable or necessary.
More concisely: If functors `F` and `G` from category `C` to category `D` have equal objects and morphisms induced by morphisms between objects, then `F` and `G` are equal.
|
CategoryTheory.eqToHom_iso_inv_naturality
theorem CategoryTheory.eqToHom_iso_inv_naturality :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b)
{j j' : β} (w : j = j'),
CategoryTheory.CategoryStruct.comp (z j).inv (CategoryTheory.eqToHom ⋯) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').inv
This theorem, named `CategoryTheory.eqToHom_iso_inv_naturality`, asserts that for any category `C` and any families `f` and `g` from a sort `β` to `C`, if there exists a family of isomorphisms `z` between `f` and `g`, then for any two elements `j` and `j'` in `β` with equality `j = j'`, the composition of the inverse of the isomorphism at `j` and the morphism produced from the equality is the same as the composition of the morphism produced from the equality and the inverse of the isomorphism at `j'`. This property can be understood as a naturality condition for the "equality-to-morphism" function in the context of isomorphisms.
More concisely: For any category `C` and families `f` and `g` from a sort `β` to `C`, if `z` is a family of isomorphisms from `f` to `g`, then for all `j, j' in β` with `j = j'`, the diagram `(z.inv j) * (id j) = (id j') * (z.inv j')` commutes.
|
CategoryTheory.eqToHom_map
theorem CategoryTheory.eqToHom_map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (p : X = Y),
F.map (CategoryTheory.eqToHom p) = CategoryTheory.eqToHom ⋯
The theorem `CategoryTheory.eqToHom_map` states that for any categories `C` and `D`, and any functor `F` from `C` to `D`, if `X` and `Y` are objects in `C` such that `X = Y`, then mapping the morphism that corresponds to this equality (obtained through `CategoryTheory.eqToHom`) under the functor `F` is equal to the morphism in `D` that corresponds to the equality `F(X) = F(Y)`. In other words, the functor `F` preserves the morphisms that are induced by object equalities. This theorem is not always suitable to be a simplification lemma, as it might prevent us from using results that interact with `F`, such as the naturality of a natural transformation.
More concisely: For any functor F between categories C and D, if X and Y are equal objects in C, then F(Equality morphism from X to Y) = Equality morphism from F(X) to F(Y) in D.
|
CategoryTheory.Functor.conj_eqToHom_iff_heq
theorem CategoryTheory.Functor.conj_eqToHom_iff_heq :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} (f : W ⟶ X) (g : Y ⟶ Z) (h : W = Y)
(h' : X = Z),
f =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom h)
(CategoryTheory.CategoryStruct.comp g (CategoryTheory.eqToHom ⋯)) ↔
HEq f g
This theorem states that in any category `C`, for any four objects `W`, `X`, `Y`, `Z` in `C` and for any two morphisms `f: W ⟶ X` and `g: Y ⟶ Z`, `f` is equal to the composition of the morphism from `eqToHom h` and the composition of `g` with `eqToHom h'` if and only if `f` is heterogeneously equal to `g`. The morphism `eqToHom h` is obtained from the equality `h: W = Y` and `eqToHom h'` is from `h': X = Z`. The term "heterogeneously equal" refers to a kind of equality (`HEq`) in dependent type theory where the types of the things being compared may themselves not be equal.
More concisely: For any category C and objects W, X, Y, Z, morphisms f : W → X and g : Y → Z, and equalities h : W = Y and h' : X = Z, f is equal to the composition of eqToHom h and the composition of g with eqToHom h' if and only if f is heterogeneously equal to g.
|
CategoryTheory.eqToHom_trans_assoc
theorem CategoryTheory.eqToHom_trans_assoc :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X = Y) (q : Y = Z) {Z_1 : C}
(h : Z ⟶ Z_1),
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom p)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom q) h) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h
This theorem, `CategoryTheory.eqToHom_trans_assoc`, asserts that in any category `C`, given objects `X`, `Y`, `Z` and `Z_1`, and equalities `p : X = Y` and `q : Y = Z`, the composition of the morphism induced by `p` and the composition of the morphism induced by `q` and a morphism `h : Z ⟶ Z_1` is equal to a composition of a morphism and `h`, where the morphism is induced by chaining equalities `p` and `q`. In other words, this theorem demonstrates the associative property of morphism composition with regards to equality-induced morphisms in category theory.
More concisely: In any category, given equalities `p : X = Y` and `q : Y = Z` between objects, the induced morphisms satisfy `h . (p ∘ q) = (h ∘ p) ∘ q`.
|
CategoryTheory.eqToHom_app
theorem CategoryTheory.eqToHom_app :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D} (h : F = G) (X : C),
(CategoryTheory.eqToHom h).app X = CategoryTheory.eqToHom ⋯
The theorem `CategoryTheory.eqToHom_app` states that for any two categories `C` and `D` with functors `F` and `G` such that `F` equals `G`, and any object `X` in `C`, the application of the morphism generated from equality `F = G` to `X` is the same as the morphism generated by the equality at some suppressed context. In other words, this theorem relates the application of a functor equality to an object with the morphism generated by the equality in a certain context.
More concisely: For any categories C, D, functors F = G, and object X in C, the morphism generated from the equality F = G applied to X is equal to the morphism generated by the equality at some suppressed context.
|
CategoryTheory.eqToIso_map
theorem CategoryTheory.eqToIso_map :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X Y : C} (p : X = Y),
F.mapIso (CategoryTheory.eqToIso p) = CategoryTheory.eqToIso ⋯
The theorem `CategoryTheory.eqToIso_map` states that for any categories `C` and `D`, and a functor `F` from `C` to `D`, if there is an equality `p` between two objects `X` and `Y` in `C`, then the isomorphism induced by `F` mapping the isomorphism from `X` to `Y` (which is derived from equality `p`) is the same as the isomorphism derived from the mapped equality under the functor `F`. This theorem links the concept of equality and isomorphism in the context of category theory, highlighting that functors preserve isomorphisms.
More concisely: For any categories `C` and `D`, functor `F` from `C` to `D`, and equalities `p : X = Y` in `C`, the induced isomorphisms from `p` and `F(p)` agree: `CategoryTheory.eqToIso_map F p = F.map (CategoryTheory.eqToIso p)`.
|
CategoryTheory.eqToHom_naturality
theorem CategoryTheory.eqToHom_naturality :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ⟶ g b)
{j j' : β} (w : j = j'),
CategoryTheory.CategoryStruct.comp (z j) (CategoryTheory.eqToHom ⋯) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j')
This theorem states that in a category `C`, for any indexed family of morphisms `z : (b : β) → f b ⟶ g b` from `f b` to `g b` (for each `b` in `β`), the composition of the morphism `z j` and an `eqToHom` morphism associated with an equality `w : j = j'` is equal to the composition of an `eqToHom` morphism and the morphism `z j'`. This can be seen as a property of `eqToHom` being "natural" with respect to composition, meaning it can be "pushed" through the family of morphisms `z`.
More concisely: For any indexed family of morphisms `z : (b : β) → f b → g b` in a category `C`, and for any equalities `w : j = j'` in `β`, the diagram commutes: `z j ∘ eqToHom w = eqToHom w ∘ z j'`.
|
CategoryTheory.congrArg_cast_hom_right
theorem CategoryTheory.congrArg_cast_hom_right :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (p : X ⟶ Y) (q : Z = Y),
cast ⋯ p = CategoryTheory.CategoryStruct.comp p (CategoryTheory.eqToHom ⋯)
This theorem, `CategoryTheory.congrArg_cast_hom_right`, states that in any category `C`, for any three objects `X`, `Y`, and `Z` and a morphism `p` from `X` to `Y` and an equality `q` asserting that `Z` is identical to `Y`, the cast of morphism `p` (which might be required due to type theory issues) is equivalent to the composition of morphism `p` and the homomorphism derived from the equality `q`. The homomorphism derived from the equality `q` is obtained using the `CategoryTheory.eqToHom` function. This theorem essentially relates the cast operation with the composition of morphisms in a categorical setting.
More concisely: In any category, the cast of a morphism is equal to the composition of the morphism with the homomorphism derived from its equality to another morphism.
|
CategoryTheory.Functor.hext
theorem CategoryTheory.Functor.hext :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {F G : CategoryTheory.Functor C D},
(∀ (X : C), F.obj X = G.obj X) → (∀ (X Y : C) (f : X ⟶ Y), HEq (F.map f) (G.map f)) → F = G
This theorem, `CategoryTheory.Functor.hext`, establishes that two functors, F and G, from a category C to a category D are equal if and only if two conditions are met. First, for every object X in category C, the image of X under functor F is equal to the image of X under functor G. Second, for every pair of objects X and Y in category C and every morphism f from X to Y, the image of f under functor F is heterogeneously equal to the image of f under functor G. Here, heterogeneous equality (HEq) allows for equality between elements of potentially different types, necessary because category theory often deals with objects and morphisms of different types.
More concisely: Two functors F and G from a category C to a category D are equal if and only if they map each object and morphism in C heterogeneously equal.
|
CategoryTheory.eqToHom_iso_hom_naturality
theorem CategoryTheory.eqToHom_iso_hom_naturality :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {β : Sort u_1} {f g : β → C} (z : (b : β) → f b ≅ g b)
{j j' : β} (w : j = j'),
CategoryTheory.CategoryStruct.comp (z j).hom (CategoryTheory.eqToHom ⋯) =
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (z j').hom
This theorem, named `CategoryTheory.eqToHom_iso_hom_naturality` in Lean 4, addresses the concept of natural transformations in category theory. It states that for any category `C` and two families of objects `f` and `g` indexed over a type `β`, given natural isomorphisms `z` between `f` and `g`, and for any two indexes `j` and `j'` with an equality `w` between them, the composition of the isomorphism at `j` and the morphism induced by the equality is equal to the composition of the morphism induced by the equality and the isomorphism at `j'`. In other words, it ensures that the process of moving within the category respects the structure of the category and the isomorphisms between objects.
More concisely: Given any category C, families of objects f and g indexed over a type β, and natural isomorphisms z between f and g, if w is an equality between indexes j and j', then z\_j ∘ h\_w = h\_w ∘ z\_j', where h\_w is the induced morphism by w.
|