English
There is a canonical linear equivalence between the H-representation morphisms from Ind_φ(A) to B and the G-representation morphisms from A to Res_φ(B).
Русский
Существует каноническое линейное эквивалентное отображение между гомоморфизмами Ind_φ(A) → B над H и A → Res_φ(B) над G.
LaTeX
$$$$\mathrm{IndResHomEquiv}_\phi(A,B): (\mathrm{Ind}_\phi A \to B) \simeq\ (A \to (\mathrm{Res}_\phi B)).$$$$
Lean4
/-- Given a group homomorphism `φ : G →* H`, an `H`-representation `B`, and a `G`-representation
`A`, there is a `k`-linear equivalence between the `H`-representation morphisms `ind φ A ⟶ B` and
the `G`-representation morphisms `A ⟶ B`. -/
@[simps]
noncomputable def indResHomEquiv : (ind φ A ⟶ B) ≃ₗ[k] (A ⟶ (Action.res _ φ).obj B)
where
toFun
f :=
{ hom := ModuleCat.ofHom (f.hom.hom ∘ₗ IndV.mk φ A.ρ 1)
comm
g := by
ext x
have := (hom_comm_apply f (φ g) (IndV.mk φ A.ρ 1 x)).symm
simp_all [← Coinvariants.mk_inv_tmul] }
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun
f :=
{ hom :=
ModuleCat.ofHom <|
Representation.Coinvariants.lift _ (TensorProduct.lift <| lift _ _ _ fun h => B.ρ h⁻¹ ∘ₗ f.hom.hom) fun _ =>
by ext; have := hom_comm_apply f; simp_all
comm _ := by ext; simp [ModuleCat.endRingEquiv] }
left_inv
f := by
ext h a
simpa using (hom_comm_apply f h⁻¹ (IndV.mk φ A.ρ 1 a)).symm
right_inv _ := by ext; simp
