English
There is a k-algebra homomorphism α: (G → k) →_k (G → k) obtained from the rightFDRep component, with a two-sided inverse provided by the inverse component; α preserves multiplication, making it an algebra automorphism of the function algebra.
Русский
Существует алгеброгомом от правого регулярного представления к X, порожденный компонентом rightFDRep, с инверсией, и он сохраняет умножение: α(fg) = α(f)α(g).
LaTeX
$$$\alpha = (\eta.hom.hom.app rightFDRep).hom : (G \to k) \to_k (G \to k),\; α(fg) = α(f) α(g)$$$
Lean4
theorem toRightFDRepComp_injective {η₁ η₂ : Aut (forget k G)}
(h : η₁.hom.hom.app rightFDRep = η₂.hom.hom.app rightFDRep) : η₁ = η₂ :=
by
have := Fintype.ofFinite G
classical
ext X v
have h1 := η₁.hom.hom.naturality (ofRightFDRep X v)
have h2 := η₂.hom.hom.naturality (ofRightFDRep X v)
rw [h, ← h2] at h1
simpa using congr(($h1).hom (single 1 1))
