subgroupComap — Mathlib

English

For a group homomorphism f: G →* G' and a subgroup H' ⊆ G', the preimage under f carries a natural MonoidHom structure from H'.comap f to H'.

Русский

Для гомоморфизма f: G →* G' и подгруппы H' ⊆ G' имеется естественная структура моноид-гомомома от H'.comap f к H'.

LaTeX

$$$f.subgroupComap(H'): H'.comap f \\to H'$$$

Lean4

/-- The `MonoidHom` from the preimage of a subgroup to itself. -/
@[to_additive (attr := simps!) /-- the `AddMonoidHom` from the preimage of an
    additive subgroup to itself. -/
    ]
def subgroupComap (f : G →* G') (H' : Subgroup G') : H'.comap f →* H' :=
  f.submonoidComap H'.toSubmonoid

Похожие утверждения