English
For a subgroup I of G × H, the second Gerg kernel is the subset of H consisting of all h with (e_G, h) ∈ I.
Русский
Для подгруппы I подмножество H, состоящее из всех элементов h, таких что (e_G, h) ∈ I.
LaTeX
$$$$I.goursatSnd = \\{ h \\in H \\mid (e_G, h) \\in I \\}.$$$$
Lean4
/-- For `I` a subgroup of `G × H`, `I.goursatSnd` is the kernel of the projection map `I → G`,
considered as a subgroup of `H`.
This is the second subgroup appearing in Goursat's lemma. See `Subgroup.goursat`. -/
@[to_additive /-- For `I` a subgroup of `G × H`, `I.goursatSnd` is the kernel of the projection map `I → G`,
considered as a subgroup of `H`.
This is the second subgroup appearing in Goursat's lemma. See `AddSubgroup.goursat`. -/
]
def goursatSnd : Subgroup H :=
((MonoidHom.fst G H).comp I.subtype).ker.map ((MonoidHom.snd G H).comp I.subtype)
