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 <scott.morrison@gmail.com>

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,26 +136,41 @@ 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.
 
 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)],