coinvariantsTensorIndIso — Mathlib

English

There is a natural isomorphism between the coinvariants of Ind φ A and the restriction-on-Res construction applied to A, observed as a natural isomorphism of functors.

Русский

Существует естественный изоморфизм между коинвариантами Ind φ A и ограничением Res φ применительно к A, рассматриваемый как естественный изоморфизм функторов.

LaTeX

$$$$\mathrm{coinvariantsTensorIndNatIso}_{\phi} : (Ind_φ A) \, ⊗ \, - \, ≅ \, - \, ⊗ \, Res_φ A.$$$$

Lean4

/-- Given a group hom `φ : G →* H`, `A : Rep k G` and `B : Rep k H`, this is the `k`-linear
isomorphism `(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`. -/
@[simps]
noncomputable def coinvariantsTensorIndIso :
    ((coinvariantsTensor k H).obj (ind φ A)).obj B ≅ ((coinvariantsTensor k G).obj A).obj ((Action.res _ φ).obj B)
    where
  hom := coinvariantsTensorIndHom φ A B
  inv := coinvariantsTensorIndInv φ A B
  hom_inv_id := by
    ext h a b
    simpa [tensorObj_def, tensorObj, coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom,
      Coinvariants.mk_eq_iff] using Coinvariants.mem_ker_of_eq h (IndV.mk φ _ h a ⊗ₜ[k] b) _ <| by simp
  inv_hom_id := by
    ext
    simp [tensorObj_def, tensorObj, coinvariantsTensorIndInv, coinvariantsTensorMk, coinvariantsTensorIndHom]

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