English
For a monoid hom φ, an H-representation B and a G-representation A, there is a canonical k-linear bijection between the G-equivariant morphisms B → A and the H-morphisms B → coind φ A.
Русский
Для монойдного гомоморфизма φ, H-репрезентации B и G-репрезентации A существует каноническое k-линейное биекция между г-эквівариантными морфизмами B → A и г-морфизмами B → coind φ A.
LaTeX
$$$\big(B \to A\big)^{G} \cong_\text{linear} \big(B \to \mathrm{coind}_\phi A\big)$$
Lean4
/-- 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 `B ⟶ A` and the
`H`-representation morphisms `B ⟶ coind φ A`. -/
@[simps]
noncomputable def resCoindHomEquiv (B : Rep k H) (A : Rep k G) : ((Action.res _ φ).obj B ⟶ A) ≃ₗ[k] (B ⟶ coind φ A)
where
toFun
f :=
{ hom :=
ModuleCat.ofHom <|
(LinearMap.pi fun h => f.hom.hom ∘ₗ Rep.ρ B h).codRestrict _ fun _ _ _ => by simpa using hom_comm_apply f _ _
comm _ := by ext; simp [ModuleCat.endRingEquiv] }
map_add' _ _ := rfl
map_smul' _ _ := rfl
invFun
f :=
{ hom := ModuleCat.ofHom (LinearMap.proj 1 ∘ₗ ((Rep.ρ A).coindV φ).subtype ∘ₗ f.hom.hom)
comm
g := by
ext x
have := ((f.hom x).2 g 1).symm
have := hom_comm_apply f (φ g) x
simp_all }
left_inv := by intro; ext; simp
right_inv z := by ext; have := hom_comm_apply z; simp_all
