map — Mathlib

English

The image of a subgroup under a monoid homomorphism is itself a subgroup of the codomain.

Русский

Образ подгруппы под моноид-гомоморфизмом является подгруппой целевой группы.

LaTeX

$$$ \\operatorname{Subgroup.map} f H \\subseteq N \\text{ is a subgroup of } N $$$

Lean4

/-- The image of a subgroup along a monoid homomorphism is a subgroup. -/
@[to_additive /-- The image of an `AddSubgroup` along an `AddMonoid` homomorphism
          is an `AddSubgroup`. -/
    ]
def map (f : G →* N) (H : Subgroup G) : Subgroup N :=
  { H.toSubmonoid.map f with
    carrier := f '' H
    inv_mem' := by
      rintro _ ⟨x, hx, rfl⟩
      exact ⟨x⁻¹, H.inv_mem hx, f.map_inv x⟩ }

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