From 9d3db5347e8c637ca8c0247bea649ec9fa500d64 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 2 May 2022 13:45:08 +0000 Subject: [PATCH] feat(category_theory/preadditive): End X is a division_ring or field when X is simple (#13849) Consequences of Schur's lemma Co-authored-by: Scott Morrison --- src/category_theory/preadditive/schur.lean | 66 ++++++++++++++++------ 1 file changed, 48 insertions(+), 18 deletions(-) diff --git a/src/category_theory/preadditive/schur.lean b/src/category_theory/preadditive/schur.lean index 931c218419558..22566b9338844 100644 --- a/src/category_theory/preadditive/schur.lean +++ b/src/category_theory/preadditive/schur.lean @@ -19,19 +19,13 @@ Second, we prove Schur's lemma for `𝕜`-linear categories with finite dimensio 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. -/ namespace category_theory open category_theory.limits -universes v u -variables {C : Type u} [category.{v} C] +variables {C : Type*} [category C] variables [preadditive C] /-- @@ -49,8 +43,8 @@ end As a corollary of Schur's lemma for preadditive categories, any morphism between simple objects is (exclusively) either an isomorphism or zero. -/ -lemma is_iso_iff_nonzero [has_kernels C] {X Y : C} [simple.{v} X] [simple.{v} Y] (f : X ⟶ Y) : - is_iso.{v} f ↔ f ≠ 0 := +lemma is_iso_iff_nonzero [has_kernels C] {X Y : C} [simple X] [simple Y] (f : X ⟶ Y) : + is_iso f ↔ f ≠ 0 := ⟨λ I, begin introI h, @@ -59,16 +53,34 @@ lemma is_iso_iff_nonzero [has_kernels C] {X Y : C} [simple.{v} X] [simple.{v} Y] end, λ w, is_iso_of_hom_simple w⟩ +/-- +In any preadditive category with kernels, +the endomorphisms of a simple object form a division ring. +-/ +noncomputable +instance [has_kernels C] {X : C} [simple X] : division_ring (End X) := +by classical; exact +{ inv := λ f, if h : f = 0 then 0 else by { haveI := is_iso_of_hom_simple h, exact inv f, }, + exists_pair_ne := ⟨𝟙 X, 0, id_nonzero _⟩, + inv_zero := dif_pos rfl, + mul_inv_cancel := λ f h, begin + haveI := is_iso_of_hom_simple h, + convert is_iso.inv_hom_id f, + exact dif_neg h, + end, + ..(infer_instance : ring (End X)) } + open finite_dimensional -variables (𝕜 : Type*) [field 𝕜] +section +variables (𝕜 : Type*) [division_ring 𝕜] /-- Part of **Schur's lemma** for `𝕜`-linear categories: the hom space between two non-isomorphic simple objects is 0-dimensional. -/ lemma finrank_hom_simple_simple_eq_zero_of_not_iso - [has_kernels C] [linear 𝕜 C] {X Y : C} [simple.{v} X] [simple.{v} Y] + [has_kernels C] [linear 𝕜 C] {X Y : C} [simple X] [simple Y] (h : (X ≅ Y) → false): finrank 𝕜 (X ⟶ Y) = 0 := begin @@ -80,6 +92,9 @@ begin exact finrank_zero_of_subsingleton, end +end + +variables (𝕜 : Type*) [field 𝕜] variables [is_alg_closed 𝕜] [linear 𝕜 C] -- In the proof below we have some difficulty using `I : finite_dimensional 𝕜 (X ⟶ X)` @@ -121,15 +136,30 @@ variables [has_kernels C] **Schur's lemma** for endomorphisms in `𝕜`-linear categories. -/ lemma finrank_endomorphism_simple_eq_one - (X : C) [simple.{v} X] [I : finite_dimensional 𝕜 (X ⟶ X)] : + (X : C) [simple X] [I : finite_dimensional 𝕜 (X ⟶ X)] : finrank 𝕜 (X ⟶ X) = 1 := finrank_endomorphism_eq_one 𝕜 is_iso_iff_nonzero lemma endomorphism_simple_eq_smul_id - {X : C} [simple.{v} X] [I : finite_dimensional 𝕜 (X ⟶ X)] (f : X ⟶ X) : + {X : C} [simple X] [I : finite_dimensional 𝕜 (X ⟶ X)] (f : X ⟶ X) : ∃ c : 𝕜, c • 𝟙 X = f := (finrank_eq_one_iff_of_nonzero' (𝟙 X) (id_nonzero X)).mp (finrank_endomorphism_simple_eq_one 𝕜 X) f +/-- +Endomorphisms of a simple object form a field if they are finite dimensional. +This can't be an instance as `𝕜` would be undetermined. +-/ +noncomputable +def field_End_of_finite_dimensional (X : C) [simple X] [I : finite_dimensional 𝕜 (X ⟶ X)] : + field (End X) := +by classical; exact +{ mul_comm := λ f g, begin + obtain ⟨c, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 f, + obtain ⟨d, rfl⟩ := endomorphism_simple_eq_smul_id 𝕜 g, + simp [←mul_smul, mul_comm c d], + end, + ..(infer_instance : division_ring (End X)) } + /-- **Schur's lemma** for `𝕜`-linear categories: if hom spaces are finite dimensional, then the hom space between simples is at most 1-dimensional. @@ -137,10 +167,10 @@ if hom spaces are finite dimensional, then the hom space between simples is at m 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. -/ --- We don't really need `[∀ X Y : C, finite_dimensional 𝕜 (X ⟶ Y)]` here, --- just at least one of `[finite_dimensional 𝕜 (X ⟶ X)]` or `[finite_dimensional 𝕜 (Y ⟶ Y)]`. +-- There is a symmetric argument that uses `[finite_dimensional 𝕜 (Y ⟶ Y)]` instead, +-- but we don't bother proving that here. lemma finrank_hom_simple_simple_le_one - (X Y : C) [∀ X Y : C, finite_dimensional 𝕜 (X ⟶ Y)] [simple.{v} X] [simple.{v} Y] : + (X Y : C) [finite_dimensional 𝕜 (X ⟶ X)] [simple X] [simple Y] : finrank 𝕜 (X ⟶ Y) ≤ 1 := begin cases subsingleton_or_nontrivial (X ⟶ Y) with h, @@ -156,7 +186,7 @@ begin end lemma finrank_hom_simple_simple_eq_one_iff - (X Y : C) [∀ X Y : C, finite_dimensional 𝕜 (X ⟶ Y)] [simple.{v} X] [simple.{v} Y] : + (X Y : C) [finite_dimensional 𝕜 (X ⟶ X)] [finite_dimensional 𝕜 (X ⟶ Y)] [simple X] [simple Y] : finrank 𝕜 (X ⟶ Y) = 1 ↔ nonempty (X ≅ Y) := begin fsplit, @@ -173,7 +203,7 @@ begin end lemma finrank_hom_simple_simple_eq_zero_iff - (X Y : C) [∀ X Y : C, finite_dimensional 𝕜 (X ⟶ Y)] [simple.{v} X] [simple.{v} Y] : + (X Y : C) [finite_dimensional 𝕜 (X ⟶ X)] [finite_dimensional 𝕜 (X ⟶ Y)] [simple X] [simple Y] : finrank 𝕜 (X ⟶ Y) = 0 ↔ is_empty (X ≅ Y) := begin rw [← not_nonempty_iff, ← not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y)],