subgroupMap — Mathlib

English

For a group homomorphism f: G →* G' and a subgroup H ≤ G, the map Subgroup.subgroupMap H → G' is surjective; every subgroup of the image lifts from some subgroup of G.

Русский

Для гомоморфизма f: G →* G' и подгруппы H ⊆ G отображение Subgroup.subgroupMap(H) на подгруппы образа сюръективно; любая подгруппа образа восстанавливается из подгруппы наверху.

LaTeX

$$Surjective (f.subgroupMap H)$$

Lean4

/-- The `MonoidHom` from a subgroup to its image. -/
@[to_additive (attr := simps!) /-- the `AddMonoidHom` from an additive subgroup to its image -/
    ]
def subgroupMap (f : G →* G') (H : Subgroup G) : H →* H.map f :=
  f.submonoidMap H.toSubmonoid

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