coinvariantsTensorIndInv — Mathlib

English

There are canonical linear maps between coinvariants and induced coinvariants that respect the IndV constructions; in particular, the mk-tensor maps commute with the induced identifications.

Русский

Существуют канонические линейные отображения между коинвариантами и индуцированными коинвариантами, которые сохраняют конструкции IndV; в частности, отображения mk-тензора совместимы с индуцированными идентификациями.

LaTeX

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

Lean4

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

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