mathlib documentation

category_theory.preadditive.schur

Schur's lemma #

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.

Future work #

It might be nice to provide a division_ring instance on End X when X is simple. This is an easy consequence of the results here, but may take some care setting up usable instances.

The part of Schur's lemma that holds in any preadditive category with kernels: that a nonzero morphism between simple objects is an isomorphism.

As a corollary of Schur's lemma for preadditive categories, any morphism between simple objects is (exclusively) either an isomorphism or zero.

Part of Schur's lemma for π•œ-linear categories: the hom space between two non-isomorphic simple objects is 0-dimensional.

theorem distrib_mul_action.ext {M : Type u_9} {A : Type u_10} {_inst_1 : monoid M} {_inst_2 : add_monoid A} (x y : distrib_mul_action M A) (h : distrib_mul_action.to_mul_action = distrib_mul_action.to_mul_action) :
x = y
theorem module.ext {R : Type u} {M : Type v} {_inst_1 : semiring R} {_inst_2 : add_comm_monoid M} (x y : module R M) (h : module.to_distrib_mul_action = module.to_distrib_mul_action) :
x = y
theorem distrib_mul_action.ext_iff {M : Type u_9} {A : Type u_10} {_inst_1 : monoid M} {_inst_2 : add_monoid A} (x y : distrib_mul_action M A) :
theorem mul_action.ext {Ξ± : Type u_9} {Ξ² : Type u_10} {_inst_1 : monoid Ξ±} (x y : mul_action Ξ± Ξ²) (h : mul_action.to_has_scalar = mul_action.to_has_scalar) :
x = y
theorem mul_action.ext_iff {Ξ± : Type u_9} {Ξ² : Type u_10} {_inst_1 : monoid Ξ±} (x y : mul_action Ξ± Ξ²) :
theorem has_scalar.ext {M : Type u_9} {Ξ± : Type u_10} (x y : has_scalar M Ξ±) (h : has_scalar.smul = has_scalar.smul) :
x = y
theorem module.ext_iff {R : Type u} {M : Type v} {_inst_1 : semiring R} {_inst_2 : add_comm_monoid M} (x y : module R M) :
theorem has_scalar.ext_iff {M : Type u_9} {Ξ± : Type u_10} (x y : has_scalar M Ξ±) :
theorem category_theory.finrank_endomorphism_eq_one {C : Type u} [category_theory.category C] [category_theory.preadditive C] (π•œ : Type u_1) [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)] :

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.

Schur's lemma for endomorphisms in π•œ-linear categories.

theorem category_theory.endomorphism_simple_eq_smul_id {C : Type u} [category_theory.category C] [category_theory.preadditive C] (π•œ : Type u_1) [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) :
βˆƒ (c : π•œ), c β€’ πŸ™ X = f

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.