CategoryTheory.EnoughInjectives.of_adjunction
theorem CategoryTheory.EnoughInjectives.of_adjunction :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C},
(L ⊣ R) →
∀ [inst_2 : L.PreservesMonomorphisms] [inst_3 : L.ReflectsMonomorphisms]
[inst_4 : CategoryTheory.EnoughInjectives D], CategoryTheory.EnoughInjectives C
This theorem is about categories in mathematics, specifically in relation to category theory. The theorem asserts that if we have an adjunction between two categories C and D, with C and D being functors, and if the functor L preserves monomorphisms and reflects monomorphisms, and D has enough injectives, then C also has enough injectives. The term "enough injectives" in a category refers to the property that every object in the category is a subobject of an injective object. This theorem is also known as Lemma 3.8 in category theory.
More concisely: If functors C and D form an adjunction, with C preserving and reflecting monomorphisms, and D has enough injectives, then category C also has enough injectives.
|
CategoryTheory.EnoughInjectives.presentation
theorem CategoryTheory.EnoughInjectives.presentation :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [self : CategoryTheory.EnoughInjectives C] (X : C),
Nonempty (CategoryTheory.InjectivePresentation X)
The theorem `CategoryTheory.EnoughInjectives.presentation` states that, in a category that has enough injectives, every object has an injective presentation. More concretely, for every object `X` in such a category `C`, there exists an injective object `J` and a monomorphism from `X` to `J`. A monomorphism, in category theory, is an arrow (or morphism) that can be thought of as an injective function. Thus, this theorem is about the existence of a certain kind of structure (an injective presentation) within a category that satisfies a particular property (having enough injectives).
More concisely: In a category with enough injectives, every object has an injective object and a monomorphic arrow to it.
|
CategoryTheory.EnoughInjectives.of_equivalence
theorem CategoryTheory.EnoughInjectives.of_equivalence :
∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C]
[inst_1 : CategoryTheory.Category.{v₂, u₂} D] (e : CategoryTheory.Functor C D) [inst_2 : e.IsEquivalence]
[inst_3 : CategoryTheory.EnoughInjectives D], CategoryTheory.EnoughInjectives C
This theorem states that if there is an equivalence of categories between two categories C and D, and if D has enough injectives, then C also has enough injectives. Here, "enough injectives" refers to a property of a category such that for any object in the category, there is a monomorphism from that object to some injective object. An "equivalence of categories" is a relationship between two categories that allows us to translate concepts and properties from one category to the other in a way that preserves the essential structure of the categories. The theorem essentially says that if we can translate concepts and properties between two categories and one of them has enough injective objects, then the other one must also have enough injective objects.
More concisely: If there is an equivalence of categories between C and D and D has enough injectives, then C also has enough injectives.
|
CategoryTheory.Injective.factors
theorem CategoryTheory.Injective.factors :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : C} [self : CategoryTheory.Injective J] {X Y : C}
(g : X ⟶ J) (f : X ⟶ Y) [inst_1 : CategoryTheory.Mono f], ∃ h, CategoryTheory.CategoryStruct.comp f h = g
This theorem states that an object `J` in a category `C` is injective if and only if every morphism from any object `X` in `C` to `J` can be obtained by composing a monomorphism from `X` to some object `Y` in `C` with some morphism from `Y` to `J`. In other words, for every morphism `g : X ⟶ J` and every monomorphism `f : X ⟶ Y`, there exists a morphism `h` such that the composition of `f` and `h` equals `g`.
More concisely: An object `J` in a category `C` is injective if and only if every morphism to `J` factorizes through some monomorphism in `C`.
|
CategoryTheory.InjectivePresentation.mono
theorem CategoryTheory.InjectivePresentation.mono :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.InjectivePresentation X),
CategoryTheory.Mono self.f
This theorem states that for any category `C` and any object `X` within that category, if `X` has an injective presentation, then the morphism `f` from `X` to some injective object `J` is a monomorphism. In category theory, a monomorphism is a morphism (or arrow) that is left-cancellable, and an injective presentation of an object involves a monomorphism to some injective object. In simpler terms, if you have a one-way function from `X` to an injective object `J`, this function is a monomorphism.
More concisely: If an object `X` in a category `C` has an injective presentation, then any morphem `f` from `X` to an injective object is a monomorphism.
|
CategoryTheory.Injective.comp_factorThru
theorem CategoryTheory.Injective.comp_factorThru :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J X Y : C} [inst_1 : CategoryTheory.Injective J]
(g : X ⟶ J) (f : X ⟶ Y) [inst_2 : CategoryTheory.Mono f],
CategoryTheory.CategoryStruct.comp f (CategoryTheory.Injective.factorThru g f) = g
The theorem `CategoryTheory.Injective.comp_factorThru` states that in any category `C`, for objects `J`, `X`, and `Y` such that `J` is injective, given a morphism `g` from `X` to `J` and a monomorphism `f` from `X` to `Y`, the factorization of `g` through `f` (represented by `CategoryTheory.Injective.factorThru g f`) followed by `f` (represented by `CategoryTheory.CategoryStruct.comp f (CategoryTheory.Injective.factorThru g f)`) is equal to `g`. In other words, the composition of `f` and the factorisation of `g` through `f` yields `g`, affirming that `g` can indeed be factored through the monomorphism `f`.
More concisely: In a category with injective objects, given a morphism and a monomorphism between their sources, the composition of the morphism with the factorization of the morphism through the monomorphism equals the morphism itself.
|
CategoryTheory.InjectivePresentation.injective
theorem CategoryTheory.InjectivePresentation.injective :
∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (self : CategoryTheory.InjectivePresentation X),
CategoryTheory.Injective self.J
This theorem states that for any type `C` that forms a category, and any object `X` in that category, if `X` has an injective presentation, then the object `J` in that injective presentation is injective. In other words, if there is a monomorphism (an injective morphism) from `X` to `J`, then `J` is injective. This is typically used in category theory, a field of mathematics that deals with abstract algebraic structures and their relationships.
More concisely: If `X` is an object in a category `C` with an injective presentation `X ↔ J`, then `J` is an injective object in `C`.
|