CategoryTheory.finrank_hom_simple_simple_le_one
theorem CategoryTheory.finrank_hom_simple_simple_le_one :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(𝕜 : Type u_2) [inst_2 : Field 𝕜] [inst_3 : IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C]
[inst_5 : CategoryTheory.Limits.HasKernels C] (X Y : C) [inst_6 : FiniteDimensional 𝕜 (X ⟶ X)]
[inst_7 : CategoryTheory.Simple X] [inst_8 : CategoryTheory.Simple Y], FiniteDimensional.finrank 𝕜 (X ⟶ Y) ≤ 1
**Schur's Lemma** for `𝕜`-linear categories: In the context of a category `C` which is preadditive, has kernels, and is `𝕜`-linear where `𝕜` is a field that is algebraically closed, if objects `X` and `Y` in `C` are each simple (i.e., they have no non-zero proper subobjects), and the hom space (set of morphisms) from `X` to `X` is a finite-dimensional `𝕜`-vector space, then the dimension of the hom space from `X` to `Y` over `𝕜` is either 0 or 1. The specific dimension can be determined given the information whether `X` and `Y` are isomorphic, which is a refinement provided by other theorems `finrank_hom_simple_simple_eq_one_iff` and `finrank_hom_simple_simple_eq_zero_iff`.
More concisely: In a preadditive, `𝕜`-linear, algebraically closed field category `C` with kernels, if `X` and `Y` are simple objects with finite-dimensional `𝕜`-vector space of homomorphisms, then the dimension is either 0 or 1 and equals 1 if and only if `X` and `Y` are isomorphic.
|
CategoryTheory.finrank_endomorphism_simple_eq_one
theorem CategoryTheory.finrank_endomorphism_simple_eq_one :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(𝕜 : Type u_2) [inst_2 : Field 𝕜] [inst_3 : IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C]
[inst_5 : CategoryTheory.Limits.HasKernels C] (X : C) [inst_6 : CategoryTheory.Simple X]
[inst_7 : FiniteDimensional 𝕜 (X ⟶ X)], FiniteDimensional.finrank 𝕜 (X ⟶ X) = 1
**Schur's Lemma** for endomorphisms in `𝕜`-linear categories states that for any category `C` accompanied by some conditions (being a category, being preadditive, having a field `𝕜`, the field `𝕜` being algebraically closed, the category `C` being `𝕜`-linear, and having kernels) and any object `X` in that category, where `X` is simple and the vector space of morphisms from `X` to `X` is finite-dimensional, the rank (or dimension in the finite case) of the endomorphism space (set of all morphisms from `X` to itself) is equal to one.
In other words, in a context where morphisms have a structure of `𝕜`-vector space and `𝕜` is a field, if we consider a simple object `X` whose self-morphisms form a finite-dimensional vector space, then this vector space has dimension one. This is a key result in representation theory and reflects the 'irreducibility' of simple objects.
More concisely: In a preadditive, finite-dimensional, algebraically closed `𝕜`-linear category with kernels, the endomorphism space of a simple object is a one-dimensional `𝕜`-vector space.
|
CategoryTheory.finrank_endomorphism_eq_one
theorem CategoryTheory.finrank_endomorphism_eq_one :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(𝕜 : Type u_2) [inst_2 : Field 𝕜] [inst_3 : IsAlgClosed 𝕜] [inst_4 : CategoryTheory.Linear 𝕜 C] {X : C},
(∀ (f : X ⟶ X), CategoryTheory.IsIso f ↔ f ≠ 0) →
∀ [I : FiniteDimensional 𝕜 (X ⟶ X)], FiniteDimensional.finrank 𝕜 (X ⟶ X) = 1
This theorem, known as an auxiliary lemma for Schur's lemma, states that for any category `C` that is preadditive and has a linear structure over a field `𝕜`, and for any object `X` in `C`, if the endomorphism space `X ⟶ X` is finite-dimensional and every non-zero endomorphism is invertible, then the rank (or dimension) of the endomorphism space `X ⟶ X` is 1. This theorem has implications in the context of representation theory and linear algebra.
More concisely: In a preadditive, linearly structured category over a field with finite-dimensional and invertible endomorphisms for every non-zero endomorphism of an object, the rank of the endomorphism space of that object is equal to 1.
|
CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso
theorem CategoryTheory.finrank_hom_simple_simple_eq_zero_of_not_iso :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
(𝕜 : Type u_2) [inst_2 : DivisionRing 𝕜] [inst_3 : CategoryTheory.Limits.HasKernels C]
[inst_4 : CategoryTheory.Linear 𝕜 C] {X Y : C} [inst_5 : CategoryTheory.Simple X]
[inst_6 : CategoryTheory.Simple Y], ((X ≅ Y) → False) → FiniteDimensional.finrank 𝕜 (X ⟶ Y) = 0
This theorem is a part of Schur's lemma for 𝕜-linear categories. It states that, given a division ring 𝕜 and a 𝕜-linear category C which has kernels and two objects X and Y that are simple, the hom space (set of morphisms) from X to Y is 0-dimensional if X and Y are not isomorphic. In other words, there are no non-zero 𝕜-linear maps between two distinct simple objects in the category.
More concisely: In a 𝕜-linear category with kernels, the hom set between two distinct simple objects is empty.
|
CategoryTheory.isIso_of_hom_simple
theorem CategoryTheory.isIso_of_hom_simple :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasKernels C] {X Y : C} [inst_3 : CategoryTheory.Simple X]
[inst_4 : CategoryTheory.Simple Y] {f : X ⟶ Y}, f ≠ 0 → CategoryTheory.IsIso f
This theorem is a part of Schur's lemma, as applied in any preadditive category that has kernels. It states that any non-zero morphism `f` between two simple objects `X` and `Y` is an isomorphism. Here, `C` is the category, and `X` and `Y` are objects in `C` that are assumed to be simple. The condition `f ≠ 0` asserts that `f` is a non-zero morphism from `X` to `Y`. The theorem then concludes that `f` is an isomorphism in the category `C`.
More concisely: In any preadditive category with kernels, a non-zero morphism between two simple objects is an isomorphism.
|
CategoryTheory.isIso_iff_nonzero
theorem CategoryTheory.isIso_iff_nonzero :
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
[inst_2 : CategoryTheory.Limits.HasKernels C] {X Y : C} [inst_3 : CategoryTheory.Simple X]
[inst_4 : CategoryTheory.Simple Y] (f : X ⟶ Y), CategoryTheory.IsIso f ↔ f ≠ 0
This theorem states that in the context of preadditive categories with kernels, for any morphism `f` between two simple objects `X` and `Y`, `f` is an isomorphism if and only if `f` is not equal to zero. This is a corollary of Schur's lemma for preadditive categories, which states that any morphism between simple objects is exclusively either an isomorphism or zero.
More concisely: In a preadditive category with kernels, a morphism between simple objects is an isomorphism if and only if it is non-zero.
|