Schur's lemma #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. We first prove the part of Schur's Lemma that holds in any preadditive category with kernels, that any nonzero morphism between simple objects is an isomorphism.
Second, we prove Schur's lemma for π-linear categories with finite dimensional hom spaces,
over an algebraically closed field π:
the hom space X βΆ Y between simple objects X and Y is at most one dimensional,
and is 1-dimensional iff X and Y are isomorphic.
theorem
category_theory.mono_of_nonzero_from_simple
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_kernels C]
{X Y : C}
[category_theory.simple X]
{f : X βΆ Y}
(w : f β 0) :
theorem
category_theory.is_iso_of_hom_simple
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_kernels C]
{X Y : C}
[category_theory.simple X]
[category_theory.simple Y]
{f : X βΆ Y}
(w : f β 0) :
The part of Schur's lemma that holds in any preadditive category with kernels: that a nonzero morphism between simple objects is an isomorphism.
theorem
category_theory.is_iso_iff_nonzero
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_kernels C]
{X Y : C}
[category_theory.simple X]
[category_theory.simple Y]
(f : X βΆ Y) :
category_theory.is_iso f β f β 0
As a corollary of Schur's lemma for preadditive categories, any morphism between simple objects is (exclusively) either an isomorphism or zero.
@[protected, instance]
noncomputable
def
category_theory.End.division_ring
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.limits.has_kernels C]
{X : C}
[category_theory.simple X] :
In any preadditive category with kernels, the endomorphisms of a simple object form a division ring.
Equations
- category_theory.End.division_ring = {add := ring.add infer_instance, add_assoc := _, zero := ring.zero infer_instance, zero_add := _, add_zero := _, nsmul := ring.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg infer_instance, sub := ring.sub infer_instance, sub_eq_add_neg := _, zsmul := ring.zsmul infer_instance, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast infer_instance, nat_cast := ring.nat_cast infer_instance, one := ring.one infer_instance, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul infer_instance, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow infer_instance, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := Ξ» (f : category_theory.End X), dite (f = 0) (Ξ» (h : f = 0), 0) (Ξ» (h : Β¬f = 0), category_theory.inv f), div := div_inv_monoid.div._default ring.mul category_theory.End.division_ring._proof_23 ring.one category_theory.End.division_ring._proof_24 category_theory.End.division_ring._proof_25 ring.npow category_theory.End.division_ring._proof_26 category_theory.End.division_ring._proof_27 (Ξ» (f : category_theory.End X), dite (f = 0) (Ξ» (h : f = 0), 0) (Ξ» (h : Β¬f = 0), category_theory.inv f)), div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default ring.mul category_theory.End.division_ring._proof_29 ring.one category_theory.End.division_ring._proof_30 category_theory.End.division_ring._proof_31 ring.npow category_theory.End.division_ring._proof_32 category_theory.End.division_ring._proof_33 (Ξ» (f : category_theory.End X), dite (f = 0) (Ξ» (h : f = 0), 0) (Ξ» (h : Β¬f = 0), category_theory.inv f)), zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv (category_theory.End X)), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul (category_theory.End X)), qsmul_eq_mul' := _}
theorem
category_theory.finrank_hom_simple_simple_eq_zero_of_not_iso
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[division_ring π]
[category_theory.limits.has_kernels C]
[category_theory.linear π C]
{X Y : C}
[category_theory.simple X]
[category_theory.simple Y]
(h : (X β
Y) β false) :
finite_dimensional.finrank π (X βΆ Y) = 0
Part of Schur's lemma for π-linear categories:
the hom space between two non-isomorphic simple objects is 0-dimensional.
theorem
category_theory.finrank_endomorphism_eq_one
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
{X : C}
(is_iso_iff_nonzero : β (f : X βΆ X), category_theory.is_iso f β f β 0)
[I : finite_dimensional π (X βΆ X)] :
finite_dimensional.finrank π (X βΆ X) = 1
An auxiliary lemma for Schur's lemma.
If X βΆ X is finite dimensional, and every nonzero endomorphism is invertible,
then X βΆ X is 1-dimensional.
theorem
category_theory.finrank_endomorphism_simple_eq_one
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
[category_theory.limits.has_kernels C]
(X : C)
[category_theory.simple X]
[I : finite_dimensional π (X βΆ X)] :
finite_dimensional.finrank π (X βΆ X) = 1
Schur's lemma for endomorphisms in π-linear categories.
theorem
category_theory.endomorphism_simple_eq_smul_id
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
[category_theory.limits.has_kernels C]
{X : C}
[category_theory.simple X]
[I : finite_dimensional π (X βΆ X)]
(f : X βΆ X) :
noncomputable
def
category_theory.field_End_of_finite_dimensional
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
[category_theory.limits.has_kernels C]
(X : C)
[category_theory.simple X]
[I : finite_dimensional π (X βΆ X)] :
Endomorphisms of a simple object form a field if they are finite dimensional.
This can't be an instance as π would be undetermined.
Equations
- category_theory.field_End_of_finite_dimensional π X = {add := division_ring.add infer_instance, add_assoc := _, zero := division_ring.zero infer_instance, zero_add := _, add_zero := _, nsmul := division_ring.nsmul infer_instance, nsmul_zero' := _, nsmul_succ' := _, neg := division_ring.neg infer_instance, sub := division_ring.sub infer_instance, sub_eq_add_neg := _, zsmul := division_ring.zsmul infer_instance, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := division_ring.int_cast infer_instance, nat_cast := division_ring.nat_cast infer_instance, one := division_ring.one infer_instance, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := division_ring.mul infer_instance, mul_assoc := _, one_mul := _, mul_one := _, npow := division_ring.npow infer_instance, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, mul_comm := _, inv := division_ring.inv infer_instance, div := division_ring.div infer_instance, div_eq_mul_inv := _, zpow := division_ring.zpow infer_instance, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := division_ring.rat_cast infer_instance, mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := division_ring.qsmul infer_instance, qsmul_eq_mul' := _}
theorem
category_theory.finrank_hom_simple_simple_le_one
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
[category_theory.limits.has_kernels C]
(X Y : C)
[finite_dimensional π (X βΆ X)]
[category_theory.simple X]
[category_theory.simple Y] :
finite_dimensional.finrank π (X βΆ Y) β€ 1
Schur's lemma for π-linear categories:
if hom spaces are finite dimensional, then the hom space between simples is at most 1-dimensional.
See finrank_hom_simple_simple_eq_one_iff and finrank_hom_simple_simple_eq_zero_iff below
for the refinements when we know whether or not the simples are isomorphic.
theorem
category_theory.finrank_hom_simple_simple_eq_one_iff
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
[category_theory.limits.has_kernels C]
(X Y : C)
[finite_dimensional π (X βΆ X)]
[finite_dimensional π (X βΆ Y)]
[category_theory.simple X]
[category_theory.simple Y] :
theorem
category_theory.finrank_hom_simple_simple_eq_zero_iff
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
[category_theory.limits.has_kernels C]
(X Y : C)
[finite_dimensional π (X βΆ X)]
[finite_dimensional π (X βΆ Y)]
[category_theory.simple X]
[category_theory.simple Y] :
theorem
category_theory.finrank_hom_simple_simple
{C : Type u_1}
[category_theory.category C]
[category_theory.preadditive C]
(π : Type u_3)
[field π]
[is_alg_closed π]
[category_theory.linear π C]
[category_theory.limits.has_kernels C]
(X Y : C)
[β (X Y : C), finite_dimensional π (X βΆ Y)]
[category_theory.simple X]
[category_theory.simple Y] :