coind' — Mathlib

English

There is a natural map between coind' φ A and coind' φ B induced by f: A ⟶ B, defined by postcomposition in the appropriate setting.

Русский

Существует естественный переход от коинд' φ A к коинд' φ B, индуцируемый f: A ⟶ B.

LaTeX

$$$\mathrm{coind}'_\phi f: \mathrm{coind}'_\phi A \to \mathrm{coind}'_\phi B$$$

Lean4

/-- If `φ : G →* H` and `A : Rep k G` then `coind' φ A`, the coinduction of `A` along `φ`,
is defined as an `H`-action on `Hom_{k[G]}(k[H], A)`. If `f : k[H] → A` is `G`-equivariant
then `(h • f) (r • h₁) := r • f (h₁ * h)`, where `r : k`.
-/
noncomputable abbrev coind' : Rep k H :=
  Rep.of (Representation.coind' φ A)

Похожие утверждения