[Merged by Bors] - feat(category_theory/preadditive): Schur's lemma

src/category_theory/endomorphism.lean

@@ -30,6 +30,12 @@ instance has_mul : has_mul (End X) := ⟨λ x y, y ≫ x⟩
 
 variable {X}
 
+/-- Assist the typechecker by expressing a morphism `X ⟶ X` as a term of `End X`. -/
+def of (f : X ⟶ X) : End X := f
+
+/-- Assist the typechecker by expressing an endomorphism `f : End X` as a term of `X ⟶ X`. -/
+def as_hom (f : End X) : X ⟶ X := f
+
 @[simp] lemma one_def : (1 : End X) = 𝟙 X := rfl
 
 @[simp] lemma mul_def (xs ys : End X) : xs * ys = ys ≫ xs := rfl
@@ -49,6 +55,13 @@ instance group {C : Type u} [groupoid.{v} C] (X : C) : group (End X) :=
 
 end End
 
+lemma is_unit_iff_is_iso {C : Type u} [category.{v} C] {X : C} (f : End X) :
+  is_unit (f : End X) ↔ is_iso f :=
+⟨λ h, { out := ⟨h.unit.inv,
+  ⟨by { convert h.unit.inv_val, exact h.unit_spec.symm, },
+    by { convert h.unit.val_inv, exact h.unit_spec.symm, }⟩⟩ },
+  λ h, by exactI ⟨⟨f, inv f, by simp, by simp⟩, rfl⟩⟩
+
 variables {C : Type u} [category.{v} C] (X : C)
 
 /--

src/category_theory/linear/default.lean

@@ -7,6 +7,7 @@ import category_theory.preadditive
 import algebra.module.linear_map
 import algebra.invertible
 import linear_algebra.basic
+import algebra.algebra.basic
 
 /-!
 # Linear categories
@@ -58,6 +59,17 @@ namespace category_theory.linear
 
 variables {C : Type u} [category.{v} C] [preadditive C]
 
+section End
+
+variables {R : Type w} [comm_ring R] [linear R C]
+
+instance (X : C) : module R (End X) := by { dsimp [End], apply_instance, }
+
+instance (X : C) : algebra R (End X) :=
+algebra.of_module (λ r f g, comp_smul _ _ _ _ _ _) (λ r f g, smul_comp _ _ _ _ _ _)
+
+end End
+
 section
 variables {R : Type w} [ring R] [linear R C]
 

src/category_theory/preadditive/default.lean

@@ -6,6 +6,7 @@ Authors: Markus Himmel
 import algebra.group.hom
 import category_theory.limits.shapes.kernels
 import algebra.big_operators.basic
+import category_theory.endomorphism
 
 /-!
 # Preadditive categories
@@ -85,6 +86,14 @@ instance induced_category.category : preadditive.{v} (induced_category C F) :=
 
 end induced_category
 
+instance (X : C) : add_comm_group (End X) := by { dsimp [End], apply_instance, }
+
+instance (X : C) : ring (End X) :=
+{ left_distrib := λ f g h, preadditive.add_comp X X X g h f,
+  right_distrib := λ f g h, preadditive.comp_add X X X h f g,
+  ..(infer_instance : add_comm_group (End X)),
+  ..(infer_instance : monoid (End X)) }
+
 /-- Composition by a fixed left argument as a group homomorphism -/
 def left_comp {P Q : C} (R : C) (f : P ⟶ Q) : (Q ⟶ R) →+ (P ⟶ R) :=
 mk' (λ g, f ≫ g) $ λ g g', by simp

src/category_theory/preadditive/schur.lean

@@ -4,26 +4,25 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison
 -/
 import category_theory.simple
-import category_theory.preadditive
+import category_theory.linear
+import category_theory.endomorphism
+import field_theory.algebraic_closure
 
 /-!
 # Schur's lemma
-We prove the part of Schur's Lemma that holds in any preadditive category with kernels,
+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.
 
-## TODO
-If the category is enriched over finite dimensional vector spaces
-over an algebraically closed field, then we can further prove that
-`dim (X ⟶ Y) ≤ 1`.
-
-(Probably easiest to prove this for endomorphisms first:
-some polynomial `p` in `f : X ⟶ X` vanishes by finite dimensionality,
-that polynomial factors linearly,
-and at least one factor must be non-invertible, hence zero,
-so `f` is a scalar multiple of the identity.
-Then for any two nonzero `f g : X ⟶ Y`,
-observe `f ≫ g⁻¹` is a multiple of the identity.)
+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.
 -/
 
 namespace category_theory
@@ -32,33 +31,158 @@ open category_theory.limits
 
 universes v u
 variables {C : Type u} [category.{v} C]
-variables [preadditive C] [has_kernels C]
+variables [preadditive C]
 
 /--
-Schur's Lemma (for a general preadditive category),
+The part of Schur's lemma that holds in any preadditive category with kernels:
 that a nonzero morphism between simple objects is an isomorphism.
 -/
-lemma is_iso_of_hom_simple {X Y : C} [simple X] [simple Y] {f : X ⟶ Y} (w : f ≠ 0) :
+lemma is_iso_of_hom_simple [has_kernels C] {X Y : C} [simple X] [simple Y] {f : X ⟶ Y} (w : f ≠ 0) :
   is_iso f :=
 begin
   haveI : mono f := preadditive.mono_of_kernel_zero (kernel_zero_of_nonzero_from_simple w),
   exact is_iso_of_mono_of_nonzero w
 end
 
 /--
-As a corollary of Schur's lemma,
+As a corollary of Schur's lemma for preadditive categories,
 any morphism between simple objects is (exclusively) either an isomorphism or zero.
 -/
-def is_iso_equiv_nonzero {X Y : C} [simple.{v} X] [simple.{v} Y] {f : X ⟶ Y} :
-  is_iso.{v} f ≃ (f ≠ 0) :=
-{ to_fun := λ I,
+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 :=
+⟨λ I,
   begin
     introI h,
     apply id_nonzero X,
     simp only [←is_iso.hom_inv_id f, h, zero_comp],
   end,
-  inv_fun := λ w, is_iso_of_hom_simple w,
-  left_inv := λ I, subsingleton.elim _ _,
-  right_inv := λ w, rfl }
+  λ w, is_iso_of_hom_simple w⟩
+
+open finite_dimensional
+
+variables (𝕜 : Type*) [field 𝕜]
+
+/--
+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]
+  (h : (X ≅ Y) → false):
+  finrank 𝕜 (X ⟶ Y) = 0 :=
+begin
+  haveI := subsingleton_of_forall_eq (0 : X ⟶ Y) (λ f, begin
+    have p := not_congr (is_iso_iff_nonzero f),
+    simp only [not_not, ne.def] at p,
+    refine p.mp (λ _, by exactI h (as_iso f)),
+  end),
+  exact finrank_zero_of_subsingleton,
+end
+
+variables [is_alg_closed 𝕜] [linear 𝕜 C]
+
+-- In the proof below we have some difficulty using `I : finite_dimensional 𝕜 (X ⟶ X)`
+-- where we need a `finite_dimensional 𝕜 (End X)`.
+-- These are definitionally equal, but without eta reduction Lean can't see this.
+-- To get around this, we use `convert I`,
+-- then check the various instances agree field-by-field,
+-- using `ext` equipped with the following extra lemmas:
+local attribute [ext] add_comm_group module distrib_mul_action mul_action has_scalar
+
+/--
+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.
+-/
+-- We prove this with the explicit `is_iso_iff_nonzero` assumption,
+-- rather than just `[simple X]`, as this form is useful for
+-- Müger's formulation of semisimplicity.
+lemma finrank_endomorphism_eq_one
+  {X : C} (is_iso_iff_nonzero : ∀ f : X ⟶ X, is_iso f ↔ f ≠ 0)
+  [I : finite_dimensional 𝕜 (X ⟶ X)] :
+  finrank 𝕜 (X ⟶ X) = 1 :=
+begin
+  have id_nonzero := (is_iso_iff_nonzero (𝟙 X)).mp (by apply_instance),
+  apply finrank_eq_one (𝟙 X),
+  { exact id_nonzero, },
+  { intro f,
+    haveI : nontrivial (End X) := nontrivial_of_ne _ _ id_nonzero,
+    obtain ⟨c, nu⟩ := @exists_spectrum_of_is_alg_closed_of_finite_dimensional 𝕜 _ _ (End X) _ _ _
+      (by { convert I, ext; refl, ext; refl, }) (End.of f),
+    use c,
+    rw [is_unit_iff_is_iso, is_iso_iff_nonzero, ne.def, not_not, sub_eq_zero,
+      algebra.algebra_map_eq_smul_one] at nu,
+    exact nu.symm, },
+end
+
+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)] :
+  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) :
+  ∃ c : 𝕜, c • 𝟙 X = f :=
+(finrank_eq_one_iff_of_nonzero' (𝟙 X) (id_nonzero X)).mp (finrank_endomorphism_simple_eq_one 𝕜 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.
+-/
+-- 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)]`.
+lemma finrank_hom_simple_simple_le_one
+  (X Y : C) [∀ X Y : C, finite_dimensional 𝕜 (X ⟶ Y)] [simple.{v} X] [simple.{v} Y] :
+  finrank 𝕜 (X ⟶ Y) ≤ 1 :=
+begin
+  cases subsingleton_or_nontrivial (X ⟶ Y) with h,
+  { resetI,
+    convert zero_le_one,
+    exact finrank_zero_of_subsingleton, },
+  { obtain ⟨f, nz⟩ := (nontrivial_iff_exists_ne 0).mp h,
+    haveI fi := (is_iso_iff_nonzero f).mpr nz,
+    apply finrank_le_one f,
+    intro g,
+    obtain ⟨c, w⟩ := endomorphism_simple_eq_smul_id 𝕜 (g ≫ inv f),
+    exact ⟨c, by simpa using w =≫ f⟩, },
+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] :
+  finrank 𝕜 (X ⟶ Y) = 1 ↔ nonempty (X ≅ Y) :=
+begin
+  fsplit,
+  { intro h,
+    rw finrank_eq_one_iff' at h,
+    obtain ⟨f, nz, -⟩ := h,
+    rw ←is_iso_iff_nonzero at nz,
+    exactI ⟨as_iso f⟩, },
+  { rintro ⟨f⟩,
+    have le_one := finrank_hom_simple_simple_le_one 𝕜 X Y,
+    have zero_lt : 0 < finrank 𝕜 (X ⟶ Y) :=
+      finrank_pos_iff_exists_ne_zero.mpr ⟨f.hom, (is_iso_iff_nonzero f.hom).mp infer_instance⟩,
+    linarith, }
+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] :
+  finrank 𝕜 (X ⟶ Y) = 0 ↔ ¬ nonempty (X ≅ Y) :=
+begin
+  rw ←not_congr (finrank_hom_simple_simple_eq_one_iff 𝕜 X Y),
+  refine ⟨λ h, by { rw h, simp, }, λ h, _⟩,
+  have := finrank_hom_simple_simple_le_one 𝕜 X Y,
+  interval_cases finrank 𝕜 (X ⟶ Y) with h',
+  { exact h', },
+  { exact false.elim (h h'), },
+end
 
 end category_theory

src/category_theory/simple.lean

@@ -68,6 +68,9 @@ end
 lemma id_nonzero (X : C) [simple.{v} X] : 𝟙 X ≠ 0 :=
 (simple.mono_is_iso_iff_nonzero (𝟙 X)).mp (by apply_instance)
 
+instance (X : C) [simple.{v} X] : nontrivial (End X) :=
+nontrivial_of_ne 1 0 (id_nonzero X)
+
 section
 variable [has_zero_object C]
 local attribute [instance] has_zero_object.has_zero

src/linear_algebra/finite_dimensional.lean

@@ -1252,6 +1252,16 @@ lemma finrank_eq_one_iff_of_nonzero (v : V) (nz : v ≠ 0) :
 ⟨λ h, by { convert (singleton_is_basis v nz h).2, simp },
   λ s, finrank_eq_card_basis ⟨linear_independent_singleton nz, by { convert s, simp }⟩⟩
 
+/--
+A module with a nonzero vector `v` has dimension 1 iff every vector is a multiple of `v`.
+-/
+lemma finrank_eq_one_iff_of_nonzero' (v : V) (nz : v ≠ 0) :
+  finrank K V = 1 ↔ ∀ w : V, ∃ c : K, c • v = w :=
+begin
+  rw finrank_eq_one_iff_of_nonzero v nz,
+  apply span_singleton_eq_top_iff,
+end
+
 /--
 A module has dimension 1 iff there is some `v : V` so `{v}` is a basis.
 -/
@@ -1278,7 +1288,7 @@ begin
   convert (is_basis_singleton_iff ({v} : set V) v).symm,
   ext ⟨x, ⟨⟩⟩,
   refl,
-  apply_instance, apply_instance, -- Not sure why this aren't found automatically.
+  apply_instance, apply_instance, -- Not sure why these aren't found automatically.
 end
 
 /--