English
If f is a star-monoid homomorphism, the induced map on unitary subgroups preserves unitary status: f r is unitary whenever r is unitary.
Русский
Если f — гомоморфизм звёздного моноида, индуцированное отображение между унитарными подгруппами сохраняет унитарность: если r унитарен, то f(r) тоже унитарен.
LaTeX
$$$f: R \\to\\star* S$, $r\\in \\mathrm{unitary}(R) \\Rightarrow f(r) \\in \\mathrm{unitary}(S)$$$
Lean4
/-- The star monoid homomorphism between unitary subgroups induced by a star monoid homomorphism of
the underlying star monoids. -/
@[simps]
def map (f : R →⋆* S) : unitary R →⋆* unitary S
where
toFun := Subtype.map f (fun _ ↦ map_mem f)
map_one' := Subtype.ext <| map_one f
map_mul' _ _ := Subtype.ext <| map_mul f _ _
map_star' _ := Subtype.ext <| map_star f _
