English
The domain-conjugation equivalence domCongr k A e aligns with mapDomainAlgHom: the underlying AlgHom of domCongr is equal to mapDomainAlgHom k A e.
Русский
Связь domCongr и mapDomainAlgHom: соответствующее алгебро-гомоморфизм domCongr имеет ту же матричную форму как mapDomainAlgHom k A e.
LaTeX
$$$(\\mathrm{domCongr}\\ k\\;A\\;e).\\mathrm{toAlgHom} = \\mathrm{mapDomainAlgHom}\\ k\\;A\\;e.$$$
Lean4
/-- If `e : G ≃* H` is a multiplicative equivalence between two monoids, then
`MonoidAlgebra.domCongr e` is an algebra equivalence between their monoid algebras. -/
@[to_additive /-- If `e : G ≃+ H` is an additive equivalence between two additive monoids, then
`AddMonoidAlgebra.domCongr e` is an algebra equivalence between their additive monoid algebras. -/
]
def domCongr (e : G ≃* H) : MonoidAlgebra A G ≃ₐ[k] MonoidAlgebra A H :=
AlgEquiv.ofLinearEquiv (Finsupp.domLCongr e : (G →₀ A) ≃ₗ[k] (H →₀ A))
((equivMapDomain_eq_mapDomain _ _).trans <| mapDomain_one e)
(fun f g =>
(equivMapDomain_eq_mapDomain _ _).trans <|
(mapDomain_mul e f g).trans <|
congr_arg₂ _ (equivMapDomain_eq_mapDomain _ _).symm (equivMapDomain_eq_mapDomain _ _).symm)
