English
There is a natural H-representation morphism coind φ A ⟶ coind φ B induced by a morphism f: A ⟶ B in G-representations, given by postcomposition by f.
Русский
Существует естественный гомоморфизм коинд φ A ⟶ коинд φ B индуцируемый гомоморфизмом f: A ⟶ B в представлениях над G, задаваемый посткомпозицией по f.
LaTeX
$$$\text{coind }\phi\,f:\, \text{coind }\phi\,A \to \text{coind }\phi\,B.$$$
Lean4
/-- 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 by
`f`. -/
@[simps]
noncomputable def coindMap {A B : Rep k G} (f : A ⟶ B) : coind φ A ⟶ coind φ B
where
hom := ModuleCat.ofHom <| (f.hom.hom.compLeft H).restrict fun x h y z => by simp [h y z, hom_comm_apply]
comm _ := by ext; simp [ModuleCat.endRingEquiv]
