refactor(RepresentationTheory/Induced): add induced representations API and remove tech debt

Mathlib/RepresentationTheory/Coinduced.lean

@@ -69,7 +69,6 @@ def coindV : Submodule k (H → A) where
 lemma mem_coindV (f : H → A) : f ∈ coindV φ σ ↔ ∀ (g : G) (h : H), f (φ g * h) = σ g (f h) :=
   Iff.rfl
 
-set_option backward.isDefEq.respectTransparency.types false in
 /--
 If `ρ : Representation k G A` and `φ : G →* H` then `coind φ ρ` is the representation
 coinduced by `ρ` along `φ`, defined as the following action of `H` on the submodule `coindV φ ρ`
@@ -78,14 +77,17 @@ to the function sending `h₁` to `f (h₁ * h)`.
 
 See also `Rep.coind` and `Representation.coind'` for variants involving the category `Rep k G`.
 -/
-@[simps]
+@[simps -isSimp]
 def coind : Representation k H (coindV φ ρ) where
-  toFun h := (LinearMap.funLeft _ _ (· * h)).restrict fun x hx g h₁ => by
-    simpa [mul_assoc] using hx g (h₁ * h)
+  toFun h := (LinearMap.funLeft _ _ (· * h)).restrict fun x hx => (mem_coindV φ ρ _).mpr <| by
+      simp [(mem_coindV φ ρ _).mp hx, mul_assoc]
   map_one' := by ext; simp
   map_mul' _ _ := by ext; simp [mul_assoc]
 
-set_option backward.isDefEq.respectTransparency.types false in
+@[simp]
+lemma coind_apply_apply (h x : H) (f : coindV φ ρ) :
+    (coind φ ρ h f).val x = f.val (x * h) := rfl
+
 variable {σ ρ} in
 /-- Given a monoid homomorphism `φ : G →* H` and an intertwining map `f : σ ⟶ ρ`, there is a
   natural intertwining map `coind φ σ ⟶ coind φ ρ` given by postcomposition by `f`. -/
@@ -187,7 +189,7 @@ variable {A} in
 @[ext]
 lemma coind'_ext {f g : coind' φ A} (hfg : ∀ h, f.hom.toLinearMap (.single h 1) =
     g.hom.toLinearMap (.single h 1)) : f = g :=
-  Rep.hom_ext <| by ext1; dsimp; ext h; simpa using hfg h
+  Rep.hom_ext <| by ext h; simpa using hfg h
 
 /-- Given a monoid morphism `φ : G →* H` and a morphism of `G`-representations `f : A ⟶ B`, there
 is a natural `H`-representation morphism `coind' φ A ⟶ coind' φ B`, given by postcomposition
@@ -224,7 +226,6 @@ noncomputable def coindVEquiv :
   left_inv x := by simp
   right_inv x := coind'_ext φ fun _ => by simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- `coind φ A` and `coind' φ A` are isomorphic representations, with the underlying
 `k`-linear equivalence given by `coindVEquiv`. -/
 noncomputable def coindIso : coind φ A ≅ coind' φ A :=
@@ -243,14 +244,13 @@ end CoindIso
 
 noncomputable section Adjunction
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- The morphism induced by the adjunction between `res φ` and `coind φ` sending a morphism
   `f : res φ B ⟶ A` to the morphism `B ⟶ coind φ A` given by the underlying linear map sending
   `b : B.V` to the function sending `h : H` to `f ((B.ρ h) b)`. -/
 def resCoindToHom (B : Rep k H) (A : Rep k G) (f : res φ B ⟶ A) : B ⟶ (coind φ A) :=
-  Rep.ofHom ⟨(LinearMap.pi fun h => f.hom.toLinearMap ∘ₗ
-    Rep.ρ B h).codRestrict _ fun _ _ _ => by simpa using hom_comm_apply f _ _, fun g ↦ by
-    dsimp; ext; simp⟩
+  Rep.ofHom ⟨(LinearMap.pi fun h => f.hom.toLinearMap ∘ₗ Rep.ρ B h).codRestrict _ fun b =>
+    (Representation.mem_coindV φ A.ρ _).mpr <| fun g h => by
+      simpa using hom_comm_apply f g ((B.ρ h) b), fun _ ↦ by ext; simp⟩
 
 @[simp]
 lemma resCoindToHom_hom_apply_coe (B : Rep k H) (A : Rep k G) (f : res φ B ⟶ A) (c : ↑B.V)
@@ -270,7 +270,6 @@ info: _.1 (@DFunLike.coe _ _.1 _ _ (@ConcreteCategory.hom (Rep _ _ _ _) _ _ _ _
 
 attribute [pp_with_univ] Rep coind
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Given a monoid homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
 `A`, there is a `k`-linear equivalence between the `G`-representation morphisms `res φ B ⟶ A` and
 the `H`-representation morphisms `B ⟶ coind φ A`.

Mathlib/RepresentationTheory/FiniteIndex.lean

@@ -70,13 +70,13 @@ lemma indToCoindAux_mul_snd (g g₁ : G) (a : A) (s : S) :
 
 @[simp]
 lemma indToCoindAux_mul_fst (g₁ g₂ : G) (a : A) (s : S) :
-     indToCoindAux A (s * g₁) (A.ρ s a) g₂ = indToCoindAux A g₁ a g₂ := by
+     indToCoindAux A (s * g₁) a g₂ = indToCoindAux A g₁ (A.ρ s⁻¹ a) g₂ := by
   rcases em ((QuotientGroup.rightRel S).r g₂ g₁) with ⟨s₁, rfl⟩ | h
-  · simp only [indToCoindAux, LinearMap.pi_apply]
+  · simp only [indToCoindAux, mul_inv_rev, LinearMap.pi_apply]
     rw [dite_eq_left ⟨s₁ * s⁻¹, by simp [S.1.smul_def, smul_eq_mul, mul_assoc]⟩,
       dite_eq_left ⟨s₁, rfl⟩, ← Module.End.mul_apply, ← map_mul]
-    congr
-    simp [Subtype.ext_iff, S.1.smul_def, mul_assoc]
+    congr 2
+    simp [Subtype.ext_iff, S.1.smul_def]
   · rw [indToCoindAux_of_not_rel (h := h), indToCoindAux_of_not_rel]
     exact mt (fun ⟨s₁, hs₁⟩ => ⟨s₁ * s, by simp_all [S.1.smul_def, mul_assoc]⟩) h
 
@@ -99,15 +99,18 @@ lemma indToCoindAux_comm {A B : Rep k S} (f : A ⟶ B) (g₁ g₂ : G) (a : A) :
   · simp [S.1.smul_def, hom_comm_apply]
   · simp [indToCoindAux_of_not_rel (h := h)]
 
-set_option backward.isDefEq.respectTransparency.types false in
 variable (A) in
 /-- Let `S ≤ G` be a subgroup and `A` a `k`-linear `S`-representation. This is the `k`-linear map
 `Ind_S^G(A) →ₗ[k] Coind_S^G(A)` sending `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`. -/
-noncomputable abbrev indToCoind :
+noncomputable def indToCoind :
     ind S.subtype A →ₗ[k] coind S.subtype A :=
-  Representation.Coinvariants.lift _ (TensorProduct.lift <| (linearCombination _ fun g =>
-    LinearMap.codRestrict _ (indToCoindAux A g) fun _ _ _ => by simp) ∘ₗ
-    (MonoidAlgebra.coeffLinearEquiv k).toLinearMap) fun _ => by ext; simp
+  Representation.IndV.lift S.subtype A.ρ
+    (fun g => LinearMap.codRestrict _ (indToCoindAux A g) (by simp)) (by intros; ext; simp)
+
+lemma indToCoind_mk (g : G) (a : A) :
+    indToCoind A (IndV.mk S.subtype A.ρ g a) = indToCoindAux A g a := by
+  ext
+  simp [indToCoind]
 
 variable [S.FiniteIndex]
 
@@ -145,44 +148,40 @@ lemma coindToInd_of_support_subset_orbit (g : G) (f : coind S.subtype A)
 
 variable (A)
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma coindToInd_indToCoind : A.indToCoind ∘ₗ A.coindToInd = LinearMap.id := by
   ext g a
   simp only [LinearMap.coe_comp, Function.comp_apply, LinearMap.id_coe, id_eq]
   conv_lhs => rw [coindToInd_apply]
   simp only [map_sum, AddSubmonoidClass.coe_finsetSum, Finset.sum_apply]
   rw [Finset.sum_eq_single ⟦a⟧]
-  · simp
+  · simp [indToCoind_mk _]
   · intro b _ hb
     induction b using Quotient.inductionOn with | h b =>
-    simpa using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)
+    simpa [indToCoind_mk _] using indToCoindAux_of_not_rel b a (g.1 b) (mt Quotient.sound hb.symm)
   · simp
 
-set_option backward.isDefEq.respectTransparency.types false in
 lemma indToCoind_coindToInd : A.coindToInd ∘ₗ A.indToCoind = LinearMap.id := by
   ext g a
-  simp only [LinearMap.comp_apply, AlgebraTensorModule.curry_apply,
-    TensorProduct.curry_apply, LinearMap.coe_restrictScalars, LinearMap.id_apply]
+  simp only [LinearMap.comp_apply, LinearMap.id_apply]
   rw [coindToInd_of_support_subset_orbit g]
-  · simp
+  · simp [indToCoind_mk _]
   · intro x hx
     contrapose hx
-    simpa using indToCoindAux_of_not_rel g x a hx
+    simpa [indToCoind_mk _] using indToCoindAux_of_not_rel g x a hx
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Let `S ≤ G` be a finite index subgroup, `g₁, ..., gₙ` a set of right coset representatives of
 `S`, and `A` a `k`-linear `S`-representation. This is an isomorphism `Ind_S^G(A) ≅ Coind_S^G(A)`.
 The forward map sends `(⟦g ⊗ₜ[k] a⟧, sg) ↦ ρ(s)(a)`, and the inverse sends `f : G → A` to
 `∑ᵢ ⟦gᵢ ⊗ₜ[k] f(gᵢ)⟧` for `1 ≤ i ≤ n`. -/
 @[simps! hom_hom_toLinearMap inv_hom_toLinearMap]
 noncomputable def indCoindIso (A : Rep.{max w u} k S) :
     ind S.subtype A ≅ coind S.subtype A :=
-  mkIso (.mk (.ofLinearMap (indToCoind A) (coindToInd A)
-    (coindToInd_indToCoind A) (indToCoind_coindToInd A)) <| fun g ↦ by ext; simp)
+  mkIso (.mk (.ofLinearMap _ _ (coindToInd_indToCoind A) (indToCoind_coindToInd A)) fun g ↦ by
+    ext h
+    simp [indToCoind_mk _])
 
 variable (k S)
 
-set_option backward.isDefEq.respectTransparency.types false in
 /-- Given a finite index subgroup `S ≤ G`, this is a natural isomorphism between the `Ind_S^G` and
 `Coind_G^S` functors `Rep k S ⥤ Rep k G`. -/
 @[implicit_reducible, simps! hom_app inv_app]
@@ -191,7 +190,7 @@ noncomputable def indCoindNatIso :
   NatIso.ofComponents (fun (A : Rep k S) => indCoindIso A) fun f => by
     simp only [indFunctor_obj, coindFunctor_obj];
     ext g1 x g2
-    simp [indToCoind, indMap, indToCoindAux_comm]
+    simp [indToCoind, indToCoindAux_comm]
 
 /-- Given a finite index subgroup `S ≤ G`, `Ind_S^G` is right adjoint to the restriction functor
 `Res k G ⥤ Res k S`, since it is naturally isomorphic to `Coind_S^G`. -/