CategoryTheory.zero_not_simple
theorem CategoryTheory.zero_not_simple :
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst : CategoryTheory.Simple 0], False
This theorem establishes that in the context of category theory, the zero object cannot be considered 'simple'. Specifically, for any category `C` that has zero morphisms and a zero object, if we assume that this zero object is 'simple', then we arrive at a contradiction. The term 'simple' here refers to a concept in category theory where an object is considered simple if it has no non-trivial proper quotients. The theorem essentially asserts that there's no way to consider the zero object 'simple' under these conditions.
More concisely: In any category with zero morphisms and a zero object, the zero object cannot be simple.
|
CategoryTheory.isIso_of_mono_of_nonzero
theorem CategoryTheory.isIso_of_mono_of_nonzero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} [inst_2 : CategoryTheory.Simple Y] {f : X ⟶ Y} [inst_3 : CategoryTheory.Mono f],
f ≠ 0 → CategoryTheory.IsIso f
This theorem is a statement in the field of category theory, and it asserts the following: Given a category `C` with zero morphisms and an object `Y` in `C` that is simple, if `f` is a monomorphism (an injective morphism) from another object `X` to `Y` and `f` is not the zero morphism, then `f` is an isomorphism (a bijective morphism).
More concisely: In a category with zero morphisms, if `f` is a non-zero monomorphism from object `X` to simple object `Y`, then `f` is an isomorphism.
|
CategoryTheory.simple_of_isSimpleOrder_subobject
theorem CategoryTheory.simple_of_isSimpleOrder_subobject :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C) [inst_3 : IsSimpleOrder (CategoryTheory.Subobject X)],
CategoryTheory.Simple X
This theorem states that if a category `X` has a subobject lattice that consists of a bottom element and a top element, then `X` is simple. In more detail, given a category `C` with zero morphisms and a zero object, if `X` is an object in `C` and the subobjects of `X` form a simple order (meaning there are only two distinct elements: a least element and a greatest element), then `X` is a simple object in `C`. In category theory, a simple object is one that has no non-trivial subobjects.
More concisely: If a category with zero morphisms and a zero object has an object `X` with a subobject lattice consisting only of a bottom and top element, then `X` is a simple object in the category.
|
CategoryTheory.indecomposable_of_simple
theorem CategoryTheory.indecomposable_of_simple :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (X : C) [inst_3 : CategoryTheory.Simple X],
CategoryTheory.Indecomposable X
The theorem `CategoryTheory.indecomposable_of_simple` states that any simple object in a preadditive category is indecomposable. In more detail, consider a preadditive category with binary biproducts. If an object `X` in this category is simple, meaning it has no proper non-zero subobjects, then `X` is indecomposable. That is, it cannot be written as the biproduct of two non-zero objects. In other words, if `X` is isomorphic to the biproduct of two objects `Y` and `Z`, then either `Y` or `Z` must be zero.
More concisely: In a preadditive category with binary biproducts, a simple object is indecomposable and cannot be written as the biproduct of two non-zero objects.
|
CategoryTheory.subobject_simple_iff_isAtom
theorem CategoryTheory.subobject_simple_iff_isAtom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} (Y : CategoryTheory.Subobject X),
CategoryTheory.Simple (CategoryTheory.Subobject.underlying.obj Y) ↔ IsAtom Y
This theorem states that for any category 'C' with zero morphisms and a zero object, and for any object 'X' in 'C', a subobject 'Y' of 'X' is simple if and only if 'Y' is an atom in the lattice of subobjects of 'X'. Here, a subobject is considered simple if it has no non-trivial quotient objects, and an atom in the subobject lattice is an element with no other elements between it and the bottom element, excluding the bottom element itself.
More concisely: A subobject of an object in a category with zero morphisms and a zero object is simple if and only if it is an atom in the lattice of subobjects.
|
CategoryTheory.simple_iff_subobject_isSimpleOrder
theorem CategoryTheory.simple_iff_subobject_isSimpleOrder :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasZeroObject C] (X : C),
CategoryTheory.Simple X ↔ IsSimpleOrder (CategoryTheory.Subobject X)
The theorem `CategoryTheory.simple_iff_subobject_isSimpleOrder` states that in a category `C` with zero morphisms and a zero object, an object `X` is simple if and only if the lattice of subobjects of `X` is a simple order, which means it only contains a bottom element and a top element. The subobjects of `X` are defined as isomorphism classes of monomorphisms into `X`.
More concisely: In a category with zero morphisms and a zero object, an object is simple if and only if its lattice of subobjects is a two-element lattice.
|
CategoryTheory.simple_of_cosimple
theorem CategoryTheory.simple_of_cosimple :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C),
(∀ {Z : C} (f : X ⟶ Z) [inst_2 : CategoryTheory.Epi f], CategoryTheory.IsIso f ↔ f ≠ 0) →
CategoryTheory.Simple X
In the context of an abelian category, this theorem states that if a certain object meets the dual definition of a simple object, then it is indeed a simple object. Specifically, for any object X in the category, if for every morphism from X to another object Z (where the morphism is an epimorphism), the morphism is an isomorphism if and only if the morphism is not equal to zero, then X is a simple object. An abelian category is a type of category in mathematics that contains "abelian groups" and allows morphisms between them.
More concisely: In an abelian category, an object X is simple if and only if every epimorphism from X to another object is an isomorphism when non-zero.
|
CategoryTheory.id_nonzero
theorem CategoryTheory.id_nonzero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X : C)
[inst_2 : CategoryTheory.Simple X], CategoryTheory.CategoryStruct.id X ≠ 0
This theorem, `CategoryTheory.id_nonzero`, states that for any category `C` that has zero morphisms and any object `X` in `C` which is simple (i.e., has no non-trivial direct summands), the identity morphism on `X` is not a zero morphism. In other words, the identity morphism on a simple object in a category with zero morphisms is always nonzero.
More concisely: In any category with zero morphisms, the identity morphism of a simple object is non-zero.
|
CategoryTheory.isIso_of_epi_of_nonzero
theorem CategoryTheory.isIso_of_epi_of_nonzero :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y : C}
[inst_2 : CategoryTheory.Simple X] {f : X ⟶ Y} [inst_3 : CategoryTheory.Epi f], f ≠ 0 → CategoryTheory.IsIso f
This theorem states that in an Abelian category, if there exists a nonzero epimorphism (a morphism whose image is its target) from a simple object (an object with no proper, nontrivial subobjects) to any other object, then this epimorphism is an isomorphism (a morphism with an inverse).
More concisely: In an Abelian category, a simple object is isomorphic to any epimorphic image of it.
|
CategoryTheory.Simple.of_iso
theorem CategoryTheory.Simple.of_iso :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
{X Y : C} [inst_2 : CategoryTheory.Simple Y], (X ≅ Y) → CategoryTheory.Simple X
This theorem states that for any category `C` that has zero morphisms, if `Y` is a simple object in `C` and `X` is isomorphic to `Y`, then `X` is also a simple object. Here, "simple object" is a concept from category theory which essentially means that the object has no non-trivial direct summands. In other words, the theorem tells us that the property of being a simple object is preserved under isomorphism in a category with zero morphisms.
More concisely: In a category with zero morphisms, if two objects are isomorphic, then each is a simple object.
|
CategoryTheory.epi_of_nonzero_to_simple
theorem CategoryTheory.epi_of_nonzero_to_simple :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
[inst_2 : CategoryTheory.Limits.HasEqualizers C] {X Y : C} [inst_3 : CategoryTheory.Simple Y] {f : X ⟶ Y}
[inst_4 : CategoryTheory.Limits.HasImage f], f ≠ 0 → CategoryTheory.Epi f
This theorem states that for a given category `C` with zero morphisms and equalizers, when we have a nonzero morphism `f` from an object `X` to a simple object `Y` in `C` (assuming that `f` has an image), this morphism `f` is an epimorphism. In other words, in the context of category theory, if we have a morphism that is not the zero morphism and it originates from a simple object, then it will be an "onto" mapping, meaning that it will map to every element in the codomain.
More concisely: In a category with zero morphisms and equalizers, every non-zero morphism from a simple object is an epimorphism.
|