English
Domain-preserving algebra homomorphisms respect composition: mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g) ∘ (mapDomainAlgHom k A f).
Русский
Алгеброморфизмы, сохраняющие домен, сохраняют композицию: mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g) ∘ (mapDomainAlgHom k A f).
LaTeX
$$$\\mathrm{mapDomainAlgHom}\\ k\\;A\\;(g\\cdot f) = (\\mathrm{mapDomainAlgHom}\\ k\\;A\\;g)\\circ (\\mathrm{mapDomainAlgHom}\\ k\\;A\\;f).$$$
Lean4
@[to_additive (attr := simp)]
theorem mapDomainAlgHom_comp (k A) {G₁ G₂ G₃} [CommSemiring k] [Semiring A] [Algebra k A] [Monoid G₁] [Monoid G₂]
[Monoid G₃] (f : G₁ →* G₂) (g : G₂ →* G₃) :
mapDomainAlgHom k A (g.comp f) = (mapDomainAlgHom k A g).comp (mapDomainAlgHom k A f) := by ext;
simp [mapDomain_comp]
