English
From η one obtains a k-algebra homomorphism α: (G → k) →_k (G → k) whose underlying linear map is α = (η.hom.hom.app rightFDRep).hom; thus α is a homomorphism of k-algebras from the function algebra to itself.
Русский
Из η выводится алгеброгомом F: (G → k) →_k (G → k) с основанием линейного отображения F = (η.hom.hom.app rightFDRep).hom; следовательно, F является гомоморфизмом к-алгебр
LaTeX
$$$\alpha : (G \to k) \to_k (G \to k) := (\eta.hom.hom.app rightFDRep).hom \\text{and } α: (G \to k) \to_α[k] (G \to k) \text{ satisfies } α(fg) = α(f)α(g).$$
Lean4
/-- The `rightFDRep` component of `η : Aut (forget k G)` gives rise to
an algebra morphism `(G → k) →ₐ[k] (G → k)`. -/
def algHomOfRightFDRepComp (η : Aut (forget k G)) : (G → k) →ₐ[k] (G → k) :=
by
let α : (G → k) →ₗ[k] (G → k) := (η.hom.hom.app rightFDRep).hom
let α_inv : (G → k) →ₗ[k] (G → k) := (η.inv.hom.app rightFDRep).hom
refine AlgHom.ofLinearMap α ?_ (map_mul_toRightFDRepComp η)
suffices α (α_inv 1) = (1 : G → k) by
have h := this
rwa [← one_mul (α_inv 1), map_mul_toRightFDRepComp, h, mul_one] at this
have := η.inv_hom_id
apply_fun (fun x ↦ (x.hom.app rightFDRep).hom (1 : G → k)) at this
exact this
