coinvariantsTensorIndHom — Mathlib

English

There is a canonical k-linear map Ind_φ(A) ⊗ B → A ⊗ Res_φ(B) sending [h ⊗ a] ⊗ b to [a ⊗ ρ(h)(b)].

Русский

Существует каноническое k-линейное отображение Ind_φ(A) ⊗ B → A ⊗ Res_φ(B), отправляющее [h ⊗ a] ⊗ b в [a ⊗ ρ(h)(b)].

LaTeX

$$$$\mathrm{coinvariantsTensorIndHom}_{\phi}(A,B): (\mathrm{Ind}_\phi A \otimes B) \to (A \otimes \mathrm{Res}_\phi B)$$$$

Lean4

/-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear map
`(Ind(φ)(A) ⊗ B))_H ⟶ (A ⊗ Res(φ)(B))_G` sending `⟦h ⊗ₜ a⟧ ⊗ₜ b` to `⟦a ⊗ ρ(h)(b)⟧` for all
`h : H`, `a : A`, and `b : B`. -/
noncomputable def coinvariantsTensorIndHom :
    ((coinvariantsTensor k H).obj (ind φ A)).obj B ⟶ ((coinvariantsTensor k G).obj A).obj ((Action.res _ φ).obj B) :=
  ModuleCat.ofHom <|
    Coinvariants.lift _
      (TensorProduct.lift <|
        Coinvariants.lift _
          (TensorProduct.lift <|
            Finsupp.lift _ _ _ fun g => ((coinvariantsTensorMk A ((Action.res _ φ).obj B)).compl₂ (B.ρ g)))
          fun s => by ext; simpa [coinvariantsTensorMk, Coinvariants.mk_eq_iff] using Coinvariants.sub_mem_ker s _)
      fun _ =>
      by
      simp only [MonoidalCategory.curriedTensor_obj_obj, Action.tensorObj_V, tensorObj_def, tensorObj]
      ext
      simp

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