mk — Mathlib · SciLib

English

IndV is the k-module of coinvariants of the tensor product of k[H] and A with G-action induced by φ.

Русский

IndV — это k-модуль коинвариантов тензорного произведения k[H] ⊗ A, где действие G индуцировано через φ.

LaTeX

$$IndV := Coinvariants (V := TensorProduct k (H →₀ k) A) (Representation.tprod ((leftRegular k H).comp φ) ρ)$$

Lean4

/-- Given a group homomorphism `φ : G →* H` and a `G`-representation `(A, ρ)`, this is the
`H → A →ₗ[k] (k[H] ⊗[k] A)_G` sending `h, a` to `⟦h ⊗ₜ a⟧`. -/
noncomputable abbrev mk (h : H) : A →ₗ[k] IndV φ ρ :=
  Coinvariants.mk _ ∘ₗ TensorProduct.mk k _ _ (single h 1)

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