English
If n ∈ N, then toEndHom N n = identity on the quotient G/N.
Русский
Если n ∈ N, то toEndHom N n = идентичность на частично-образе G/N.
LaTeX
$$$toEndHom N n = \mathrm{id}$ whenever $n \in N$$$
Lean4
/-- If `N` is a normal subgroup of `G`, then this is the group homomorphism
sending an element `g` of `G` to the `G`-endomorphism of `G ⧸ₐ N` given by
multiplication with `g⁻¹` on the right. -/
def toEndHom [N.Normal] : G →* End (G ⧸ₐ N)
where
toFun
v :=
{ hom :=
Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) <| fun a b h ↦
Quotient.sound <| by
apply (QuotientGroup.leftRel_apply).mpr
simpa [mul_assoc] using Subgroup.Normal.conj_mem ‹_› _ (QuotientGroup.leftRel_apply.mp h) _
comm := fun (g : G) ↦ by
ext (x : G ⧸ N)
induction x using Quotient.inductionOn with
| _ x
simp only [FintypeCat.comp_apply, Action.FintypeCat.ofMulAction_apply, Quotient.lift_mk]
change Quotient.lift (fun σ ↦ ⟦σ * v⁻¹⟧) _ (⟦g • x⟧) = _
simp only [smul_eq_mul, Quotient.lift_mk, mul_assoc]
rfl }
map_one' := by
apply Action.hom_ext
ext (x : G ⧸ N)
induction x using Quotient.inductionOn
simp
map_mul' σ
τ := by
apply Action.hom_ext
ext (x : G ⧸ N)
induction x using Quotient.inductionOn with
| _ x
change ⟦x * (σ * τ)⁻¹⟧ = ⟦x * τ⁻¹ * σ⁻¹⟧
rw [mul_inv_rev, mul_assoc]
