CategoryTheory.nat_trans_from_is_connected
theorem CategoryTheory.nat_trans_from_is_connected :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂}
[inst_1 : CategoryTheory.Category.{u₁, u₂} C] [inst_2 : CategoryTheory.IsPreconnected J] {X Y : C}
(α : (CategoryTheory.Functor.const J).obj X ⟶ (CategoryTheory.Functor.const J).obj Y) (j j' : J),
α.app j = α.app j'
The theorem `CategoryTheory.nat_trans_from_is_connected` states that for any two objects `X` and `Y` in a category `C` and any natural transformation `α` from the constant functor at `X` to the constant functor at `Y`, if the index category `J` is preconnected (a weaker version of being connected), then the morphism that the natural transformation `α` assigns to any two objects in `J` is the same. In other words, the natural transformation is constant. This property of connected categories is crucial for establishing properties about limits.
More concisely: If `C` is a preconnected category, any natural transformation from the constant functor at `X` to the constant functor at `Y` in `C` is constant.
|
CategoryTheory.IsPreconnected.iso_constant
theorem CategoryTheory.IsPreconnected.iso_constant :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [self : CategoryTheory.IsPreconnected J] {α : Type u₁}
(F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j : J),
Nonempty (F ≅ (CategoryTheory.Functor.const J).obj (F.obj j))
This theorem states that for any possibly empty category `J`, if every functor to a discrete category is constant, then for any functor `F` from `J` to a discrete category `α` and for any object `j` in `J`, there exists an isomorphism between `F` and the constant functor on `J` with value `F.obj j`. In other words, in a preconnected category, any functor to a discrete category must be constant at some object.
More concisely: In any preconnected category `J`, if every functor from `J` to a discrete category is constant, then for any functor `F` from `J` to a discrete category `α`, there exists an isomorphism between `F` and the constant functor on `J` with value `F.obj j` for some object `j` in `J`.
|
CategoryTheory.isConnected_of_zigzag
theorem CategoryTheory.isConnected_of_zigzag :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : Nonempty J],
(∀ (j₁ j₂ : J), ∃ l, List.Chain CategoryTheory.Zag j₁ l ∧ (j₁ :: l).getLast ⋯ = j₂) →
CategoryTheory.IsConnected J
The theorem `CategoryTheory.isConnected_of_zigzag` states that if in a nonempty category `J`, any two objects are connected by a sequence of morphisms (which can be potentially reversed), then the category `J` is said to be connected. Here, `CategoryTheory.Zag` is a relation that indicates there exists a morphism between two objects either in the standard or reversed direction. The existence of a chain of such relations linking any two objects in the category implies the connectedness of the category. This theorem is the converse of `exists_zigzag'`.
More concisely: In a nonempty category, if every pair of objects can be connected by a zigzag sequence of morphisms (which may be reversed), then the category is connected.
|
CategoryTheory.zigzag_isConnected
theorem CategoryTheory.zigzag_isConnected :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : Nonempty J],
(∀ (j₁ j₂ : J), CategoryTheory.Zigzag j₁ j₂) → CategoryTheory.IsConnected J
This theorem states that if in a nonempty category, any two objects are related by the `Zigzag` relationship (meaning there is a chain of morphisms from one object to the other, and the chain can include backward morphisms), then the category is considered connected. In essence, the `Zigzag` relationship serves as a criterion for the connectedness of the category.
More concisely: In a nonempty category, if any two objects are related by a zigzag of morphisms, then the category is connected.
|
CategoryTheory.isPreconnected_of_equivalent
theorem CategoryTheory.isPreconnected_of_equivalent :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] [inst_2 : CategoryTheory.IsPreconnected J],
(J ≌ K) → CategoryTheory.IsPreconnected K
The theorem states that if two Types `J` and `K` are equivalent in the context of Category Theory, and if `J` is preconnected, then `K` is also preconnected. This theorem relates to the concept of preconnectedness (an object is preconnected if any two of its morphisms to another object can be connected through a zigzag of morphisms) in Category Theory and establishes its invariant property under equivalence of categories.
More concisely: If `J` and `K` are equivalent categories with `J` being preconnected, then `K` is also preconnected.
|
CategoryTheory.induct_on_objects
theorem CategoryTheory.induct_on_objects :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.IsPreconnected J] (p : Set J)
{j₀ : J}, j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p
This theorem describes an inductive-like property for objects in a connected category. It states that, for any given category `J`, which is pre-connected, and any given set `p` of objects in `J`, if `p` is nonempty (i.e. it contains an object `j₀`) and `p` is closed under the morphisms of `J` (meaning that if `j₁` is an element in `p` and there is a morphism from `j₁` to `j₂`, then `j₂` is also in `p`), then all objects in `J` belong to `p`. Essentially, this theorem states that if a set contains one object and is invariant under morphisms, it must contain all objects of the pre-connected category. The converse scenario is detailed in `IsConnected.of_induct`.
More concisely: In a pre-connected category `J`, any nonempty set `p` of objects that is closed under morphisms contains all objects in `J`.
|
CategoryTheory.IsConnected.of_any_functor_const_on_obj
theorem CategoryTheory.IsConnected.of_any_functor_const_on_obj :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : Nonempty J],
(∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j') →
CategoryTheory.IsConnected J
This theorem states that if for any functor `F` from a category `J` to a discrete category `α`, the functor's object mappings are constant (meaning for any two objects `j` and `j'` in `J`, `F.obj j = F.obj j'`), then `J` is a connected category. This theorem is the converse of the `any_functor_const_on_obj` theorem. It thereby provides a condition for the connectedness of a category in the context of category theory.
More concisely: If a functor from a category to a discrete category maps all objects constantly, then the category is connected.
|
CategoryTheory.isConnected_zigzag
theorem CategoryTheory.isConnected_zigzag :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.IsPreconnected J] (j₁ j₂ : J),
CategoryTheory.Zigzag j₁ j₂
This theorem, referred to as "Alias of `CategoryTheory.isPreconnected_zigzag`", states that in a connected category, there is a `Zigzag` relation between any two objects. In the context of category theory, a `Zigzag` relation means that there exists a chain of morphisms from one object to another, allowing for both forward and backward morphisms. This theorem holds for all objects `j₁` and `j₂` in a preconnected category `J`.
More concisely: In a connected category, for all objects $j\_1, j\_2$, there exists a zigzag of morphisms from $j\_1$ to $j\_2$.
|
CategoryTheory.zigzag_obj_of_zigzag
theorem CategoryTheory.zigzag_obj_of_zigzag :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K] (F : CategoryTheory.Functor J K) {j₁ j₂ : J},
CategoryTheory.Zigzag j₁ j₂ → CategoryTheory.Zigzag (F.obj j₁) (F.obj j₂)
The theorem `CategoryTheory.zigzag_obj_of_zigzag` states that given a category `J` and a functor `F` mapping from `J` to another category `K`, if there exists a 'zigzag' path (a sequence of morphisms that can go forwards and backwards) between two objects `j₁` and `j₂` in `J`, then there will also exist a 'zigzag' path between the images of these objects, `F.obj j₁` and `F.obj j₂`, in the category `K`.
More concisely: If there exists a zigzag sequence of morphisms between objects `j₁` and `j₂` in a category `J`, then there exists a corresponding zigzag sequence of morphisms between `F.obj j₁` and `F.obj j₂` in the category `K`.
|
CategoryTheory.constant_of_preserves_morphisms
theorem CategoryTheory.constant_of_preserves_morphisms :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.IsPreconnected J] {α : Type u₂}
(F : J → α), (∀ (j₁ j₂ : J), (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j'
This theorem states that if `J` is a preconnected category, then for any function `F` from `J` to an arbitrary type `α`, if every morphism from `j₁` to `j₂` in `J` implies that `F j₁` equals `F j₂`, then `F` is a constant function. In other words, if `F` preserves the structure of morphisms in `J`, then `F` maps every object in `J` to the same value in `α`. This is a kind of local-to-global property: local conditions (preservation of morphisms) imply a global condition (constancy of `F`). The converse is shown in `IsConnected.of_constant_of_preserves_morphisms`.
More concisely: If `J` is a preconnected category and for any morphisms `j₁` and `j₂` in `J`, `F j₁ = F j₂` whenever there is a morphism from `j₁` to `j₂`, then `F` is a constant function on `J`.
|
CategoryTheory.any_functor_const_on_obj
theorem CategoryTheory.any_functor_const_on_obj :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.IsPreconnected J] {α : Type u₂}
(F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j'
This theorem states that for any type `J` that forms a category and is preconnected, a functor `F` that maps from `J` to a discrete category of type `α` will always map any two objects `j` and `j'` from `J` to the same object in the discrete category. In other words, if `J` is a connected category, any functor to a discrete category is constant on its objects. The converse of this theorem is provided in `IsConnected.of_any_functor_const_on_obj`.
More concisely: For any preconnected category J and constant functor F from J to a discrete category, objects in J map to the same object in the discrete category.
|
CategoryTheory.IsConnected.of_induct
theorem CategoryTheory.IsConnected.of_induct :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : Nonempty J] {j₀ : J},
(∀ (p : Set J), j₀ ∈ p → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : J), j ∈ p) →
CategoryTheory.IsConnected J
This theorem states that given a type `J` that forms a category and is nonempty, and an element `j₀` of `J`, if for any set `p` of `J` containing `j₀`, the property holds that if there exists a morphism from `j₁` to `j₂` in the category, then `j₁` is in `p` if and only if `j₂` is in `p`, and every element of `J` is in `p`, then `J` is connected in the category theory sense.
In essence, it's saying that if any maximal connected component containing a certain element `j₀` is the entire set `J`, then `J` is considered to be connected. This is a reverse statement of the `induct_on_objects` theorem.
More concisely: If a nonempty type `J` forming a category with element `j₀` satisfies the property that every element in `J` is in any set containing `j₀` that contains a morphism between any two elements if and only if they are both in that set, then `J` is connected.
|
CategoryTheory.isPreconnected_induction
theorem CategoryTheory.isPreconnected_induction :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.IsPreconnected J]
(Z : J → Sort u_1),
({j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₁ → Z j₂) →
({j₁ j₂ : J} → (j₁ ⟶ j₂) → Z j₂ → Z j₁) → ∀ {j₀ : J}, Z j₀ → ∀ (j : J), Nonempty (Z j)
This theorem is another induction principle specifically for the type `IsPreconnected J` in category theory. Given a type family `Z : J → Sort*` and a rule for transporting in both directions along a morphism in `J`, it states that we can transport an element `x : Z j₀` to a point in `Z j` for any `j` in `J`. This is applicable in any category `J` that has a `Category` structure and is preconnected.
More concisely: Given a preconnected category J with a transport rule for a type family Z : J -> Sort*, there exists an element x in Z j for any j in J and any x0 in Z j0.
|
CategoryTheory.isConnected_of_equivalent
theorem CategoryTheory.isConnected_of_equivalent :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂}
[inst_1 : CategoryTheory.Category.{v₂, u₂} K],
(J ≌ K) → ∀ [inst : CategoryTheory.IsConnected J], CategoryTheory.IsConnected K
The theorem states that in the context of category theory, if we have two types `J` and `K` which are categories, then if `J` and `K` are equivalent (`J ≌ K`), and if `J` is a connected category, then `K` is also a connected category.
In other words, the property of being a connected category is preserved under equivalence of categories.
More concisely: If two connected categories `J` and `K` are equivalent, then `K` is also a connected category.
|
CategoryTheory.zigzag_isPreconnected
theorem CategoryTheory.zigzag_isPreconnected :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J],
(∀ (j₁ j₂ : J), CategoryTheory.Zigzag j₁ j₂) → CategoryTheory.IsPreconnected J
This theorem states that for any type `J` that forms a category, if for every pair of objects `j₁` and `j₂` in `J`, there exists a zigzag chain of morphisms connecting `j₁` and `j₂` (that is, a sequence of morphisms where backward morphisms are allowed), then `J` is preconnected. In the context of category theory, a category is said to be preconnected if any two objects in the category can be connected by a sequence of morphisms.
More concisely: A type `J` forming a category is preconnected if for every pair of objects `j₁` and `j₂` in `J`, there exists a zigzag sequence of morphisms from `j₁` to `j₂`.
|
CategoryTheory.equiv_relation
theorem CategoryTheory.equiv_relation :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : CategoryTheory.IsPreconnected J]
(r : J → J → Prop), Equivalence r → (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → r j₁ j₂) → ∀ (j₁ j₂ : J), r j₁ j₂
This theorem states that given any type `J` which forms a category and is preconnected, for any equivalence relation `r` on `J`, if the relation `r` holds for all pairs `(j₁, j₂)` such that there is a morphism from `j₁` to `j₂` in the category, then the relation `r` holds for all pairs `(j₁, j₂)` in `J`. In other words, if an equivalence relation is valid for all pairs of objects in a connected category that are connected by a morphism, then that equivalence relation holds for all pairs of objects in the category.
More concisely: In a preconnected category `J` with an equivalence relation `r`, if `r` holds for all pairs of objects connected by a morphism, then `r` holds for all pairs of objects in `J`.
|
CategoryTheory.IsConnected.of_constant_of_preserves_morphisms
theorem CategoryTheory.IsConnected.of_constant_of_preserves_morphisms :
∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [inst_1 : Nonempty J],
(∀ {α : Type u₁} (F : J → α), (∀ {j₁ j₂ : J}, (j₁ ⟶ j₂) → F j₁ = F j₂) → ∀ (j j' : J), F j = F j') →
CategoryTheory.IsConnected J
The theorem `CategoryTheory.IsConnected.of_constant_of_preserves_morphisms` states that, for any type `J` that is both a category and nonempty, if any function `F : J → α` is constant for any `j₁, j₂` whenever there is a morphism `j₁ ⟶ j₂`, then the function `F` is constant for all `j` and `j'` in `J`. This implies that `J` is a connected category. This is a kind of local-to-global property, and it's the converse of the theorem `constant_of_preserves_morphisms`.
More concisely: If every constant function on a nonempty connected category preserves morphisms, then the category is actually connected.
|