English
There is a canonical isomorphism between a subgroup H ⊆ G and its image H.map e under an isomorphism e: G ≃* G'. The construction is functorial with respect to e.
Русский
Существует канонический изоморфизм между подгруппой H ⊆ G и её изображением H.map e под изоморфизмом e: G ≃* G'. Конструкция фантазональна по отношению к e.
LaTeX
$$$\\operatorname{subgroupMap}(e)(H) \\cong \\mathrm{H.map}(e)$$$
Lean4
/-- A subgroup is isomorphic to its image under an isomorphism. If you only have an injective map,
use `Subgroup.equivMapOfInjective`. -/
@[to_additive /-- An additive subgroup is isomorphic to its image under an isomorphism. If you only
have an injective map, use `AddSubgroup.equivMapOfInjective`. -/
]
def subgroupMap (e : G ≃* G') (H : Subgroup G) : H ≃* H.map (e : G →* G') :=
MulEquiv.submonoidMap (e : G ≃* G') H.toSubmonoid
