English
If two automorphisms η1, η2 of forget k G have the same rightFDRep component, then they are equal: η1 = η2.
Русский
Если два автоморфизма η1, η2 забывательного functor имеют одинаковый компонент в rightFDRep, то они равны.
LaTeX
$$$η_1.hom.hom.app rightFDRep = η_2.hom.hom.app rightFDRep \Rightarrow η_1 = η_2$$$
Lean4
/-- For `v : X` and `G` a finite group, the representation morphism from the right
regular representation `rightFDRep` to `X` sending `single 1 1` to `v`. -/
@[simps]
def ofRightFDRep [Fintype G] (X : FDRep k G) (v : X) : rightFDRep ⟶ X
where
hom := ofHom (sumSMulInv v)
comm
t := by
ext f
let φ_term (X : FDRep k G) (f : G → k) v s := (f s) • (X.ρ s⁻¹ v)
have := sum_map univ (mulRightEmbedding t⁻¹) (φ_term X (rightRegular t f) v)
simpa [φ_term] using this
