English
Given f: G →* H and N ≤ f⁻¹(M), there is a natural induced map G/N →* H/M.
Русский
Дан гомоморфизм f: G →* H и N ≤ f⁻¹(M); существует естественное индуцированное отображение G/N →* H/M.
LaTeX
$$$\\text{map} \\; M \\; f \\; h : G/N \\to^* H/M$ is defined and is a homomorphism provided $N \\le f^{-1}(M)$.$$
Lean4
/-- A group homomorphism `f : G →* H` induces a map `G/N →* H/M` if `N ⊆ f⁻¹(M)`. -/
@[to_additive /-- An `AddGroup` homomorphism `f : G →+ H` induces a map `G/N →+ H/M` if `N ⊆ f⁻¹(M)`. -/
]
def map (M : Subgroup H) [M.Normal] (f : G →* H) (h : N ≤ M.comap f) : G ⧸ N →* H ⧸ M :=
by
refine QuotientGroup.lift N ((mk' M).comp f) ?_
intro x hx
refine QuotientGroup.eq.2 ?_
rw [mul_one, Subgroup.inv_mem_iff]
exact h hx
