feat(RepresentationTheory/Rep): add instances and APIs (#41072)

Co-authored-by: Riccardo Brasca <riccardo.brasca@gmail.com>

Author: Whysoserioushah

Mathlib/RepresentationTheory/Intertwining.lean

@@ -226,6 +226,84 @@ lemma comp_add (f₁ f₂ : IntertwiningMap σ τ) (g : IntertwiningMap ρ σ) :
 lemma add_comp (f : IntertwiningMap σ τ) (g₁ g₂ : IntertwiningMap ρ σ) :
     comp f (g₁ + g₂) = comp f g₁ + comp f g₂ := by ext1; simp [LinearMap.comp_add]
 
+variable (A) in
+/-- The projection of a product representation onto its first component is an intertwining map. -/
+def fst : IntertwiningMap (ρ.prod σ) ρ where
+  toLinearMap := LinearMap.fst A V W
+  isIntertwining' _ := LinearMap.ext <| by simp
+
+variable (A) in
+/-- The projection of a product representation onto its second component is an intertwining map. -/
+def snd : IntertwiningMap (ρ.prod σ) σ where
+  toLinearMap := LinearMap.snd A V W
+  isIntertwining' _ := LinearMap.ext <| by simp
+
+@[simp]
+lemma fst_apply (v : V × W) : fst A ρ σ v = v.1 := rfl
+
+@[simp]
+lemma snd_apply (v : V × W) : snd A ρ σ v = v.2 := rfl
+
+@[simp, norm_cast] lemma coe_fst : ⇑(fst A ρ σ) = Prod.fst := rfl
+
+@[simp, norm_cast] lemma coe_snd : ⇑(snd A ρ σ) = Prod.snd := rfl
+
+lemma fst_surjective : Function.Surjective (fst A ρ σ) := LinearMap.fst_surjective
+
+lemma snd_surjective : Function.Surjective (snd A ρ σ) := LinearMap.snd_surjective
+
+section prod
+
+variable {ρ σ τ}
+/-- The product of two intertwining maps is an intertwining map. -/
+def prod (f : IntertwiningMap ρ σ) (g : IntertwiningMap ρ τ) : IntertwiningMap ρ (σ.prod τ) where
+  toLinearMap := f.toLinearMap.prod g.toLinearMap
+  isIntertwining' _ := LinearMap.ext <| by simp [f.isIntertwining, g.isIntertwining]
+
+@[simp]
+lemma fst_prod (f : IntertwiningMap ρ σ) (g : IntertwiningMap ρ τ) :
+    (fst A σ τ).comp (prod f g) = f := IntertwiningMap.ext <| LinearMap.fst_prod _ _
+
+@[simp]
+lemma snd_prod (f : IntertwiningMap ρ σ) (g : IntertwiningMap ρ τ) :
+    (snd A σ τ).comp (prod f g) = g := IntertwiningMap.ext <| LinearMap.snd_prod _ _
+
+lemma prod_comp (X : Type*) [AddCommMonoid X] [Module A X] {π : Representation A G X}
+    (f : IntertwiningMap ρ σ) (g₁ : IntertwiningMap σ τ) (g₂ : IntertwiningMap σ π) :
+    (prod g₁ g₂).comp f = prod (g₁.comp f) (g₂.comp f) :=
+  IntertwiningMap.ext <| LinearMap.prod_comp ..
+
+variable (A ρ σ) in
+/-- The left inclusion of a product representation is an intertwining map. -/
+def inl : IntertwiningMap ρ (ρ.prod σ) := prod (id ρ) 0
+
+variable (A ρ σ) in
+/-- The right inclusion of a product representation is an intertwining map. -/
+def inr : IntertwiningMap σ (ρ.prod σ) := prod (0 : IntertwiningMap σ ρ) (id σ)
+
+lemma range_inl : (inl A ρ σ).range = (snd A ρ σ).ker :=
+  Subrepresentation.ext <| LinearMap.range_inl ..
+
+lemma range_inr : (inr A ρ σ).range = (fst A ρ σ).ker :=
+  Subrepresentation.ext <| LinearMap.range_inr ..
+
+@[simp] lemma fst_comp_inl : (fst A ρ σ).comp (inl A ρ σ) = id ρ :=
+  IntertwiningMap.ext <| LinearMap.fst_comp_inl ..
+
+@[simp] lemma snd_comp_inl : (snd A ρ σ).comp (inl A ρ σ) = 0 :=
+  IntertwiningMap.ext <| LinearMap.snd_comp_inl ..
+
+@[simp] lemma fst_comp_inr : (fst A ρ σ).comp (inr A ρ σ) = 0 :=
+  IntertwiningMap.ext <| LinearMap.fst_comp_inr ..
+
+@[simp] lemma snd_comp_inr : (snd A ρ σ).comp (inr A ρ σ) = id σ :=
+  IntertwiningMap.ext <| LinearMap.snd_comp_inr ..
+
+@[simp] lemma coprod_inl_inr : (inl A ρ σ).comp (fst A ρ σ) + (inr A ρ σ).comp (snd A ρ σ) =
+    .id _ := IntertwiningMap.ext <| LinearMap.coprod_inl_inr
+
+end prod
+
 end IntertwiningMap
 
 /-- Equivalence between representations is a bijective intertwining map. -/

Mathlib/RepresentationTheory/Rep/Basic.lean

@@ -540,6 +540,37 @@ instance preservesColimits_forget :
     Limits.PreservesColimitsOfSize.{w, w} (forget₂ (Rep.{w} k G) (ModuleCat k)) :=
   Limits.preservesColimits_of_natIso (forgetNatIsoActionForget k G).symm
 
+instance : Limits.HasBinaryBiproducts (Rep.{w} k G) where
+  has_binary_biproduct A B := Limits.hasBinaryBiproduct_of_total
+    ⟨Rep.of (X := A.V × B.V) (A.ρ.prod B.ρ), Rep.ofHom (.fst k A.ρ B.ρ), Rep.ofHom (.snd k A.ρ B.ρ),
+      Rep.ofHom (.inl k A.ρ B.ρ), Rep.ofHom (.inr k A.ρ B.ρ), by ext1; simp,
+      by ext1; simp [zero_hom], by ext1; simp [zero_hom], by ext1; simp⟩ <| by
+    ext1; simp [Rep.add_hom]
+
+instance : Limits.HasZeroObject (Rep.{w} k G) where
+  zero := ⟨Rep.trivial k G PUnit, {
+    unique_to X := Nonempty.intro ⟨⟨0⟩, fun f ↦ by
+      ext x; have : x = 0 := Subsingleton.elim _ _; subst this; simp⟩
+    unique_from X := Nonempty.intro ⟨⟨0⟩, fun f ↦ by ext⟩
+  }⟩
+
+/-- An object of `Rep k G` is zero iff the underlying `k`-module is zero. -/
+lemma isZero_iff (M : Rep k G) : Limits.IsZero M ↔ Subsingleton M.V := by
+  simp [Limits.IsZero.iff_id_eq_zero, Rep.hom_ext_iff, Representation.IntertwiningMap.ext_iff,
+    ← ModuleCat.isZero_of_iff_subsingleton (R := k), ModuleCat.hom_ext_iff]
+
+instance : Limits.HasLimits (Rep.{w} k G) :=
+  Adjunction.has_limits_of_equivalence (repIsoAction k G).functor
+
+instance : Limits.HasColimits (Rep.{w} k G) :=
+  Adjunction.has_colimits_of_equivalence (repIsoAction k G).functor
+
+instance : Limits.ReflectsLimitsOfSize.{w, w} (forget₂ (Rep.{w} k G) (ModuleCat k)) :=
+  Limits.reflectsLimits_of_reflectsIsomorphisms
+
+instance : Limits.ReflectsColimitsOfSize.{w, w} (forget₂ (Rep.{w} k G) (ModuleCat k)) :=
+  Limits.reflectsColimits_of_reflectsIsomorphisms
+
 variable {k G} in
 theorem epi_iff_surjective (f : A ⟶ B) : Epi f ↔ Function.Surjective f.hom :=
   ⟨fun _ => (ModuleCat.epi_iff_surjective ((forget₂ _ _).map f)).1 inferInstance,

Mathlib/RepresentationTheory/Rep/Iso.lean

@@ -168,25 +168,6 @@ instance : (toModuleMonoidAlgebra.{w} (k := k) (G := G)).IsEquivalence :=
 instance : (ofModuleMonoidAlgebra (k := k) (G := G)).IsEquivalence :=
   (equivalenceModuleMonoidAlgebra (k := k) (G := G)).isEquivalence_inverse
 
-open MonoidalCategory in
-instance : Limits.HasBinaryBiproducts (Rep.{w} k G) where
-  has_binary_biproduct A B := Limits.hasBinaryBiproduct_of_total
-    ⟨Rep.of (X := A.V × B.V) (Representation.prod A.ρ B.ρ), Rep.ofHom ⟨LinearMap.fst k _ _, by
-      simp [LinearMap.ext_iff]⟩, Rep.ofHom ⟨LinearMap.snd k _ _, by simp [LinearMap.ext_iff]⟩,
-      Rep.ofHom ⟨LinearMap.inl _ _ _, by simp [LinearMap.ext_iff]⟩, Rep.ofHom ⟨LinearMap.inr _ _ _,
-      by simp [LinearMap.ext_iff]⟩, by ext : 2; simp, by ext : 2; simp [zero_hom], by
-      ext : 2; simp [zero_hom], by ext : 2; simp⟩ <| by
-    ext : 2; simp [← ofHom_comp, ← ofHom_add, LinearMap.ext_iff]
-
-instance : Limits.HasZeroObject (Rep.{w} k G) where
-  zero := ⟨Rep.trivial k G PUnit, {
-    unique_to X := Nonempty.intro ⟨⟨0⟩, fun f ↦ by
-      ext x; have : x = 0 := Subsingleton.elim _ _; subst this; simp⟩
-    unique_from X := Nonempty.intro ⟨⟨0⟩, fun f ↦ by ext⟩
-  }⟩
-
-instance : Limits.HasFiniteProducts (Rep.{w} k G) := hasFiniteProducts_of_has_binary_and_terminal
-
 instance : Abelian (Rep.{w} k G) := abelianOfEquivalence toModuleMonoidAlgebra
 
 -- TODO Verify that the equivalence with `ModuleCat k[G]` is a monoidal functor.

Mathlib/RepresentationTheory/Rep/Res.lean

@@ -5,8 +5,8 @@ Authors: Edison Xie
 -/
 module
 
-public import Mathlib.RepresentationTheory.Rep.Basic
-
+public import Mathlib.Algebra.Homology.ShortComplex.ShortExact
+public import Mathlib.RepresentationTheory.Rep.Iso
 /-!
 # Restriction of representations
 
@@ -88,6 +88,56 @@ instance : (resFunctor (k := k) f).Additive where
 instance {k : Type u} [CommSemiring k] : (resFunctor (k := k) f).Linear k where
   map_smul {_ _} _ _ := by ext : 2; simp [smul_hom]
 
+section ShortComplex
+
+open Limits
+
+variable {k : Type u} [Ring k]
+
+instance : PreservesLimits (resFunctor.{w} (k := k) f) :=
+  have : PreservesLimitsOfSize.{w, w} (resFunctor f ⋙ forget₂ (Rep.{w} k H) (ModuleCat k)) :=
+    inferInstanceAs (PreservesLimitsOfSize.{w, w} (forget₂ (Rep.{w} k G) (ModuleCat k)))
+  preservesLimits_of_reflects_of_preserves _ (forget₂ (Rep.{w} k H) (ModuleCat k))
+
+instance : Limits.PreservesColimits (resFunctor.{w} (k := k) f) :=
+  have : PreservesColimitsOfSize.{w, w} (resFunctor (k := k) f ⋙
+      forget₂ (Rep.{w} k H) (ModuleCat k)) :=
+    inferInstanceAs (PreservesColimitsOfSize.{w, w} (forget₂ (Rep.{w} k G) (ModuleCat k)))
+  preservesColimits_of_reflects_of_preserves _ (forget₂ (Rep.{w} k H) (ModuleCat k))
+
+/-- An object of `Rep k G` is zero iff its restriction to `H` is zero. -/
+lemma isZero_res_iff (M : Rep k G) :
+    IsZero (res f M) ↔ IsZero M := by
+  rw [isZero_iff, isZero_iff, Rep.res_obj_V]
+
+/--
+The instances above show that the restriction functor `res φ : Rep R G ⥤ Rep R H`
+preserves and reflects exactness. -/
+lemma res_map_exact {k : Type u} [CommRing k]
+    (S : ShortComplex (Rep.{w} k G)) :
+    (S.map (resFunctor f)).Exact ↔ S.Exact := by
+  rw [ShortComplex.exact_map_iff_of_faithful]
+
+lemma shortExact_res {k : Type u} [CommRing k] (φ : H →* G) {S : ShortComplex (Rep.{w} k G)} :
+    (S.map (resFunctor φ)).ShortExact ↔ S.ShortExact := by
+  constructor
+  · intro h
+    have h₁ := h.1
+    have h₂ := h.2
+    have h₃ := h.3
+    rw [ShortComplex.exact_map_iff_of_faithful] at h₁
+    simp only [ShortComplex.map_f, mono_iff_injective, ShortComplex.map_g,
+      epi_iff_surjective] at h₂ h₃
+    exact {exact := h₁, mono_f := mono_iff_injective _|>.2 h₂, epi_g := epi_iff_surjective _|>.2 h₃}
+  · rintro @⟨_, mono_f, epi_g⟩
+    exact {
+      exact := by rwa [ShortComplex.exact_map_iff_of_faithful]
+      mono_f := by simpa [mono_iff_injective] using! mono_f
+      epi_g := by simpa [epi_iff_surjective] using! epi_g
+    }
+
+end ShortComplex
+
 noncomputable section
 
 variable {G : Type v} [Group G] (A : Rep k G) (S : Subgroup G)

Mathlib/RepresentationTheory/Subrepresentation.lean

@@ -27,6 +27,7 @@ variable [Semiring A] [Monoid G] [AddCommMonoid W] [Module A W]
 /-- A subrepresentation of `G` of the `A`-module `W` is a submodule of `W`
 which is stable under the `G`-action.
 -/
+@[ext]
 structure Subrepresentation where
   /-- A subrepresentation is a submodule. -/
   toSubmodule : Submodule A W