English
Two coinduction functors from Rep k G to Rep k H, namely coindFunctor k φ and coindFunctor' k φ, are naturally isomorphic; the objectwise isomorphism is given by coindIso φ.
Русский
Два функторa коиндукции между категориальными представлениями естественным образом изоморфны; на объектах изоморфизм задаётся через coindIso φ.
LaTeX
$$$\mathrm{coindFunctor}\_k\phi \cong \mathrm{coindFunctor}'\_k\phi$$$
Lean4
/-- Given a monoid homomorphism `φ : G →* H`, the coinduction functors `Rep k G ⥤ Rep k H` given by
`coindFunctor k φ` and `coindFunctor' k φ` are naturally isomorphic, with isomorphism on objects
given by `coindIso φ`. -/
@[simps!]
noncomputable def coindFunctorIso : coindFunctor k φ ≅ coindFunctor' k φ :=
NatIso.ofComponents (coindIso φ) fun _ =>
by
simp only [coindFunctor_obj, coindFunctor'_obj]
ext
simp
