From bcff648f44aa9400c9dbb47ad71f97e44b87b0c0 Mon Sep 17 00:00:00 2001 From: Johan Commelin Date: Mon, 24 Feb 2025 10:24:39 +0100 Subject: [PATCH] chore(RepresentationTheory): generalize most of FDRep to commutative rings --- Mathlib/RepresentationTheory/FDRep.lean | 73 +++++++++++++------------ 1 file changed, 38 insertions(+), 35 deletions(-) diff --git a/Mathlib/RepresentationTheory/FDRep.lean b/Mathlib/RepresentationTheory/FDRep.lean index 5c30b1048a148..24304a5306ee7 100644 --- a/Mathlib/RepresentationTheory/FDRep.lean +++ b/Mathlib/RepresentationTheory/FDRep.lean @@ -45,32 +45,35 @@ open CategoryTheory.Limits /-- The category of finite dimensional `k`-linear representations of a monoid `G`. -/ -abbrev FDRep (k G : Type u) [Field k] [Monoid G] := - Action (FGModuleCat.{u} k) (MonCat.of G) +abbrev FDRep (R G : Type u) [Ring R] [Monoid G] := + Action (FGModuleCat.{u} R) (MonCat.of G) namespace FDRep -variable {k G : Type u} [Field k] [Monoid G] +variable {R k G : Type u} [CommRing R] [Field k] [Monoid G] -- Porting note: `@[derive]` didn't work for `FDRep`. Add the 4 instances here. -instance : LargeCategory (FDRep k G) := inferInstance -instance : ConcreteCategory (FDRep k G) (Action.HomSubtype _ _) := inferInstance -instance : Preadditive (FDRep k G) := inferInstance +instance : LargeCategory (FDRep R G) := inferInstance +instance : ConcreteCategory (FDRep R G) (Action.HomSubtype _ _) := inferInstance +instance : Preadditive (FDRep R G) := inferInstance instance : HasFiniteLimits (FDRep k G) := inferInstance -instance : Linear k (FDRep k G) := by infer_instance +instance : Linear R (FDRep R G) := by infer_instance -instance : CoeSort (FDRep k G) (Type u) := +instance : CoeSort (FDRep R G) (Type u) := ⟨fun V => V.V⟩ -instance (V : FDRep k G) : AddCommGroup V := by - change AddCommGroup ((forget₂ (FDRep k G) (FGModuleCat k)).obj V).obj; infer_instance +instance (V : FDRep R G) : AddCommGroup V := by + change AddCommGroup ((forget₂ (FDRep R G) (FGModuleCat R)).obj V).obj; infer_instance -instance (V : FDRep k G) : Module k V := by - change Module k ((forget₂ (FDRep k G) (FGModuleCat k)).obj V).obj; infer_instance +instance (V : FDRep R G) : Module R V := by + change Module R ((forget₂ (FDRep R G) (FGModuleCat R)).obj V).obj; infer_instance + +instance (V : FDRep R G) : Module.Finite R V := by + change Module.Finite R ((forget₂ (FDRep R G) (FGModuleCat R)).obj V); infer_instance instance (V : FDRep k G) : FiniteDimensional k V := by - change FiniteDimensional k ((forget₂ (FDRep k G) (FGModuleCat k)).obj V); infer_instance + infer_instance /-- All hom spaces are finite dimensional. -/ instance (V W : FDRep k G) : FiniteDimensional k (V ⟶ W) := @@ -78,52 +81,52 @@ instance (V W : FDRep k G) : FiniteDimensional k (V ⟶ W) := (Functor.map_injective (forget₂ (FDRep k G) (FGModuleCat k))) /-- The monoid homomorphism corresponding to the action of `G` onto `V : FDRep k G`. -/ -def ρ (V : FDRep k G) : G →* V →ₗ[k] V := +def ρ (V : FDRep R G) : G →* V →ₗ[R] V := (ModuleCat.endRingEquiv _).toMonoidHom.comp (Action.ρ V).hom @[simp] -lemma endRingEquiv_symm_comp_ρ (V : FDRep k G) : +lemma endRingEquiv_symm_comp_ρ (V : FDRep R G) : (MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj).symm).comp (ρ V) = (Action.ρ V).hom := rfl @[simp] -lemma endRingEquiv_comp_ρ (V : FDRep k G) : +lemma endRingEquiv_comp_ρ (V : FDRep R G) : (MonoidHomClass.toMonoidHom (ModuleCat.endRingEquiv V.V.obj)).comp (Action.ρ V).hom = ρ V := rfl @[simp] -lemma hom_action_ρ (V : FDRep k G) (g : G) : (Action.ρ V g).hom = ρ V g := rfl +lemma hom_action_ρ (V : FDRep R G) (g : G) : (Action.ρ V g).hom = ρ V g := rfl /-- The underlying `LinearEquiv` of an isomorphism of representations. -/ -def isoToLinearEquiv {V W : FDRep k G} (i : V ≅ W) : V ≃ₗ[k] W := - FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i) +def isoToLinearEquiv {V W : FDRep R G} (i : V ≅ W) : V ≃ₗ[R] W := + FGModuleCat.isoToLinearEquiv ((Action.forget (FGModuleCat R) (MonCat.of G)).mapIso i) -theorem Iso.conj_ρ {V W : FDRep k G} (i : V ≅ W) (g : G) : +theorem Iso.conj_ρ {V W : FDRep R G} (i : V ≅ W) (g : G) : W.ρ g = (FDRep.isoToLinearEquiv i).conj (V.ρ g) := by rw [FDRep.isoToLinearEquiv, ← hom_action_ρ V, ← FGModuleCat.Iso.conj_hom_eq_conj, Iso.conj_apply, ← ModuleCat.hom_ofHom (W.ρ g), ← ModuleCat.hom_ext_iff, - Iso.eq_inv_comp ((Action.forget (FGModuleCat k) (MonCat.of G)).mapIso i)] + Iso.eq_inv_comp ((Action.forget (FGModuleCat R) (MonCat.of G)).mapIso i)] exact (i.hom.comm g).symm /-- Lift an unbundled representation to `FDRep`. -/ @[simps ρ] -abbrev of {V : Type u} [AddCommGroup V] [Module k V] [FiniteDimensional k V] - (ρ : Representation k G V) : FDRep k G := - ⟨FGModuleCat.of k V, MonCat.ofHom ρ ≫ MonCat.ofHom - (ModuleCat.endRingEquiv (ModuleCat.of k V)).symm.toMonoidHom⟩ +abbrev of {V : Type u} [AddCommGroup V] [Module R V] [Module.Finite R V] + (ρ : Representation R G V) : FDRep R G := + ⟨FGModuleCat.of R V, MonCat.ofHom ρ ≫ MonCat.ofHom + (ModuleCat.endRingEquiv (ModuleCat.of R V)).symm.toMonoidHom⟩ -instance : HasForget₂ (FDRep k G) (Rep k G) where - forget₂ := (forget₂ (FGModuleCat k) (ModuleCat k)).mapAction (MonCat.of G) +instance : HasForget₂ (FDRep R G) (Rep R G) where + forget₂ := (forget₂ (FGModuleCat R) (ModuleCat R)).mapAction (MonCat.of G) -theorem forget₂_ρ (V : FDRep k G) : ((forget₂ (FDRep k G) (Rep k G)).obj V).ρ = V.ρ := by +theorem forget₂_ρ (V : FDRep R G) : ((forget₂ (FDRep R G) (Rep R G)).obj V).ρ = V.ρ := by ext g v; rfl -- Verify that the monoidal structure is available. -example : MonoidalCategory (FDRep k G) := by infer_instance +example : MonoidalCategory (FDRep R G) := by infer_instance -example : MonoidalPreadditive (FDRep k G) := by infer_instance +example : MonoidalPreadditive (FDRep R G) := by infer_instance -example : MonoidalLinear k (FDRep k G) := by infer_instance +example : MonoidalLinear R (FDRep R G) := by infer_instance open Module @@ -139,13 +142,13 @@ theorem finrank_hom_simple_simple [IsAlgClosed k] (V W : FDRep k G) [Simple V] [ CategoryTheory.finrank_hom_simple_simple k V W /-- The forgetful functor to `Rep k G` preserves hom-sets and their vector space structure. -/ -def forget₂HomLinearEquiv (X Y : FDRep k G) : - ((forget₂ (FDRep k G) (Rep k G)).obj X ⟶ - (forget₂ (FDRep k G) (Rep k G)).obj Y) ≃ₗ[k] X ⟶ Y where +def forget₂HomLinearEquiv (X Y : FDRep R G) : + ((forget₂ (FDRep R G) (Rep R G)).obj X ⟶ + (forget₂ (FDRep R G) (Rep R G)).obj Y) ≃ₗ[R] X ⟶ Y where toFun f := ⟨f.hom, f.comm⟩ map_add' _ _ := rfl map_smul' _ _ := rfl - invFun f := ⟨(forget₂ (FGModuleCat k) (ModuleCat k)).map f.hom, f.comm⟩ + invFun f := ⟨(forget₂ (FGModuleCat R) (ModuleCat R)).map f.hom, f.comm⟩ left_inv _ := by ext; rfl right_inv _ := by ext; rfl