Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-05-03 14:11 7da83031

View on Github →

feat(category_theory/preadditive): Schur's lemma (#7366) 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.

Estimated changes

Modified src/category_theory/endomorphism.lean

added def category_theory.End.as_hom

added def category_theory.End.of

added theorem category_theory.is_unit_iff_is_iso

Modified src/category_theory/linear/default.lean

Modified src/category_theory/preadditive/default.lean

Modified src/category_theory/preadditive/schur.lean

added theorem category_theory.endomorphism_simple_eq_smul_id

added theorem category_theory.finrank_endomorphism_eq_one

added theorem category_theory.finrank_endomorphism_simple_eq_one

added theorem category_theory.finrank_hom_simple_simple_eq_one_iff

added theorem category_theory.finrank_hom_simple_simple_eq_zero_iff

added theorem category_theory.finrank_hom_simple_simple_eq_zero_of_not_iso

added theorem category_theory.finrank_hom_simple_simple_le_one

deleted def category_theory.is_iso_equiv_nonzero

added theorem category_theory.is_iso_iff_nonzero

modified theorem category_theory.is_iso_of_hom_simple

Modified src/category_theory/simple.lean

Modified src/linear_algebra/finite_dimensional.lean

added theorem finrank_eq_one_iff_of_nonzero'