|
| 1 | +/- |
| 2 | +Copyright (c) 2025 Sophie Morel. All rights reserved. |
| 3 | +Released under Apache 2.0 license as described in the file LICENSE. |
| 4 | +Authors: Sophie Morel |
| 5 | +-/ |
| 6 | +import Mathlib.Algebra.Category.FGModuleCat.Abelian |
| 7 | +import Mathlib.Algebra.Category.ModuleCat.Injective |
| 8 | +import Mathlib.RepresentationTheory.Character |
| 9 | +import Mathlib.RepresentationTheory.Maschke |
| 10 | +import Mathlib.RingTheory.SimpleModule.InjectiveProjective |
| 11 | + |
| 12 | +/-! |
| 13 | +# Applications of Maschke's theorem |
| 14 | +
|
| 15 | +This proves some properties of representations that follow from Maschke's |
| 16 | +theorem. |
| 17 | +
|
| 18 | +We prove that, if `G` is a finite group whose order is invertible in a field `k`, |
| 19 | +then every object of `Rep k G` (resp. `FDRep k G`) is injective and projective. |
| 20 | +
|
| 21 | +We also give two simpleness criteria for an object `V` of `FDRep k G`, when `k` is |
| 22 | +an algebraically closed field in which the order of `G` is invertible: |
| 23 | +* `FDRep.simple_iff_end_is_rank_one`: `V` is simple if and only `V ⟶ V` is a `k`-vector |
| 24 | +space of dimension `1`. |
| 25 | +* `FDRep.simple_iff_char_is_norm_one`: when `k` is characteristic zero, `V` is simple |
| 26 | +if and only if `∑ g : G, V.character g * V.character g⁻¹ = Fintype.card G`. |
| 27 | +
|
| 28 | +-/ |
| 29 | + |
| 30 | +universe u |
| 31 | + |
| 32 | +variable {k : Type u} [Field k] {G : Type u} [Fintype G] [Group G] |
| 33 | + |
| 34 | +open CategoryTheory Limits |
| 35 | + |
| 36 | +namespace Rep |
| 37 | + |
| 38 | +variable [NeZero (Fintype.card G : k)] |
| 39 | + |
| 40 | +/-- |
| 41 | +If `G` is finite and its order is nonzero in the field `k`, then every object of |
| 42 | +`Rep k G` is injective. |
| 43 | +-/ |
| 44 | +instance (V : Rep k G) : Injective V := by |
| 45 | + rw [← Rep.equivalenceModuleMonoidAlgebra.map_injective_iff, |
| 46 | + ← Module.injective_iff_injective_object] |
| 47 | + exact Module.injective_of_isSemisimpleRing _ _ |
| 48 | + |
| 49 | +/-- |
| 50 | +If `G` is finite and its order is nonzero in the field `k`, then every object of |
| 51 | +`Rep k G` is projective. |
| 52 | +-/ |
| 53 | +-- Will this clash with the previously defined `Projective` instances? |
| 54 | +instance (V : Rep k G) : Projective V := by |
| 55 | + rw [← Rep.equivalenceModuleMonoidAlgebra.map_projective_iff, |
| 56 | + ← IsProjective.iff_projective] |
| 57 | + exact Module.projective_of_isSemisimpleRing _ _ |
| 58 | + |
| 59 | +end Rep |
| 60 | + |
| 61 | +namespace FDRep |
| 62 | + |
| 63 | +/-- |
| 64 | +If `G` is finite and its order is nonzero in the field `k`, then every object of |
| 65 | +`FDRep k G` is injective. |
| 66 | +-/ |
| 67 | +instance [NeZero (Fintype.card G : k)] (V : FDRep k G) : Injective V := |
| 68 | + (forget₂ (FDRep k G) (Rep k G)).injective_of_map_injective inferInstance |
| 69 | + |
| 70 | +/-- |
| 71 | +If `G` is finite and its order is nonzero in the field `k`, then every object of |
| 72 | +`FDRep k G` is projective. |
| 73 | +-/ |
| 74 | +instance [NeZero (Fintype.card G : k)] (V : FDRep k G) : Projective V := |
| 75 | + (forget₂ (FDRep k G) (Rep k G)).projective_of_map_projective inferInstance |
| 76 | + |
| 77 | +variable [IsAlgClosed k] |
| 78 | + |
| 79 | +/-- |
| 80 | +If `G` is finite and its order is nonzero in an algebraically closed field `k`, |
| 81 | +then an object of `FDRep k G` is simple if and only if its space of endomorphisms is |
| 82 | +a `k`-vector space of dimension `1`. |
| 83 | +-/ |
| 84 | +lemma simple_iff_end_is_rank_one [NeZero (Fintype.card G : k)] (V : FDRep k G) : |
| 85 | + Simple V ↔ Module.finrank k (V ⟶ V) = 1 where |
| 86 | + mp h := finrank_endomorphism_simple_eq_one k V |
| 87 | + mpr h := by |
| 88 | + refine { mono_isIso_iff_nonzero {W} f _ := ⟨fun hf habs ↦ ?_, fun hf ↦ ?_⟩ } |
| 89 | + · rw [habs, isIsoZero_iff_source_target_isZero] at hf |
| 90 | + obtain ⟨g, hg⟩ : ∃ g : V ⟶ V, g ≠ 0 := |
| 91 | + (Module.finrank_pos_iff_exists_ne_zero (R := k)).mp (by grind) |
| 92 | + exact hg (hf.2.eq_zero_of_src g) |
| 93 | + · suffices Epi f by exact isIso_of_mono_of_epi f |
| 94 | + suffices Epi (Abelian.image.ι f) by |
| 95 | + rw [← Abelian.image.fac f] |
| 96 | + exact epi_comp _ _ |
| 97 | + rw [← Abelian.image.fac f] at hf |
| 98 | + set ι := Abelian.image.ι f |
| 99 | + set φ := Injective.factorThru (𝟙 _) ι |
| 100 | + have hφι : φ ≫ ι ≠ 0 := by |
| 101 | + intro habs |
| 102 | + have hιφ : 𝟙 _ = ι ≫ φ := (Injective.comp_factorThru (𝟙 _) ι).symm |
| 103 | + apply_fun (· ≫ ι) at hιφ |
| 104 | + simp_all |
| 105 | + obtain ⟨c, hc⟩ : ∃ c : k, c • _ = 𝟙 V := (finrank_eq_one_iff_of_nonzero' _ hφι).mp h (𝟙 V) |
| 106 | + refine Preadditive.epi_of_cancel_zero _ (fun g hg ↦ ?_) |
| 107 | + apply_fun (· ≫ g) at hc |
| 108 | + simpa [hg] using hc.symm |
| 109 | + |
| 110 | +/-- |
| 111 | +If `G` is finite and `k` an algebraically closed field of characteristic `0`, |
| 112 | +then an object of `FDRep k G` is simple if and only if its character has norm `1`. |
| 113 | +-/ |
| 114 | +lemma simple_iff_char_is_norm_one [CharZero k] (V : FDRep k G) : |
| 115 | + Simple V ↔ ∑ g : G, V.character g * V.character g⁻¹ = Fintype.card G where |
| 116 | + mp h := by |
| 117 | + have := invertibleOfNonzero (NeZero.ne (Fintype.card G : k)) |
| 118 | + classical |
| 119 | + have : ⅟(Fintype.card G : k) • ∑ g, V.character g * V.character g⁻¹ = 1 := by |
| 120 | + simpa only [Nonempty.intro (Iso.refl V), ↓reduceIte] using char_orthonormal V V |
| 121 | + apply_fun (· * (Fintype.card G : k)) at this |
| 122 | + rwa [mul_comm, ← smul_eq_mul, smul_smul, mul_invOf_self, smul_eq_mul, one_mul, one_mul] at this |
| 123 | + mpr h := by |
| 124 | + have := invertibleOfNonzero (NeZero.ne (Fintype.card G : k)) |
| 125 | + have eq := FDRep.scalar_product_char_eq_finrank_equivariant V V |
| 126 | + rw [h] at eq |
| 127 | + simp only [invOf_eq_inv, smul_eq_mul, inv_mul_cancel_of_invertible] at eq |
| 128 | + rw [simple_iff_end_is_rank_one, ← Nat.cast_inj (R := k), ← eq, Nat.cast_one] |
| 129 | + |
| 130 | +end FDRep |
0 commit comments