English
If K ≤ K' are subgroups of N and f : G →* N is a monoid homomorphism, then comap f K ≤ comap f K'.
Русский
Если K ≤ K' — подгруппы N и f : G →* N — моноид-гомоморфизм, то preimage подгруппы по f сохраняет неубывание: comap f K ≤ comap f K'.
LaTeX
$$$ K \\le K' \\Rightarrow comap f K \\le comap f K' $$$
Lean4
/-- The preimage of a subgroup along a monoid homomorphism is a subgroup. -/
@[to_additive /-- The preimage of an `AddSubgroup` along an `AddMonoid` homomorphism
is an `AddSubgroup`. -/
]
def comap {N : Type*} [Group N] (f : G →* N) (H : Subgroup N) : Subgroup G :=
{ H.toSubmonoid.comap f with
carrier := f ⁻¹' H
inv_mem' := fun {a} ha => show f a⁻¹ ∈ H by rw [f.map_inv]; exact H.inv_mem ha }
