English
Auxiliary relation for diagonalHomEquiv_symm_partialProd_succ linking f and contraction nth partial prod.
Русский
Вспомогательное соотношение diagonalHomEquiv_symm_partialProd_succ, связывающее f и contraction nth partialProd.
LaTeX
$$$$ ((\\text{diagonalHomEquiv } n A).symm f).hom (\\mathrm{single}(\\mathrm{partialProd}(g) \\circ a) 1) = f( \\mathrm{contractNth}(a, (· * ·), g)). $$$$
Lean4
/-- Given a `k`-linear `G`-representation `(A, ρ₁)`, this is the 'internal Hom' functor sending
`(B, ρ₂)` to the representation `Homₖ(A, B)` that maps `g : G` and `f : A →ₗ[k] B` to
`(ρ₂ g) ∘ₗ f ∘ₗ (ρ₁ g⁻¹)`. -/
@[simps]
protected noncomputable def ihom (A : Rep k G) : Rep k G ⥤ Rep k G
where
obj B := Rep.of (Representation.linHom A.ρ B.ρ)
map := fun {X} {Y} f =>
{ hom := ModuleCat.ofHom (LinearMap.llcomp k _ _ _ f.hom.hom)
comm g := by ext; simp [ModuleCat.endRingEquiv, hom_comm_apply] }
map_id := fun _ => by ext; rfl
map_comp := fun _ _ => by ext; rfl
