English
There exists a canonical structure that turns a family of maps R → S, compatible with both ring operations and a group action twisted by φ, into a MulSemiringActionSemiHomClass. In particular, the collection of φ-twisted equivariant additive semiring homomorphisms from R to S forms a coherent class with respect to the given action data.
Русский
Существует каноническая структура, переводящая множество отображений R → S, совместимых как по кольцевой структуре, так и с действием группы, связанные с φ, в класс MulSemiringActionSemiHomClass. В частности, множество φ-«скрученных» эквивariantных аддитивных полугомоморфизмов R → S образует согласованный класс относительно данных действия.
LaTeX
$$$\operatorname{MulSemiringActionSemiHomClass}(R \to_{\phi}^{*} S) \; \phi \; R \; S$$$
Lean4
instance : MulSemiringActionSemiHomClass (R →ₑ+*[φ] S) φ R S
where
map_zero m := m.map_zero'
map_add m := m.map_add'
map_one := MulSemiringActionHom.map_one'
map_mul := MulSemiringActionHom.map_mul'
map_smulₛₗ m := m.map_smul'
