English
A related universal description expresses preimages and images of MK under subgroup actions as a union over cosets specified by the subgroup lattice.
Русский
Связанные формулировки выражают предобраз и образ MK через объединения по косетам над подгруппами.
LaTeX
$$$\text{Preimage}(\text{QuotientGroup.mk}, \text{image}(\text{QuotientGroup.mk} \, s)) = \bigcup_{i} (\cdot i)^{-1}(s)$$$
Lean4
@[to_additive]
theorem preimage_image_mk (N : Subgroup α) (s : Set α) :
mk ⁻¹' ((mk : α → α ⧸ N) '' s) = ⋃ x : N, (· * (x : α)) ⁻¹' s :=
by
ext x
simp only [QuotientGroup.eq, SetLike.exists, exists_prop, Set.mem_preimage, Set.mem_iUnion, Set.mem_image]
exact ⟨fun ⟨y, hs, hN⟩ => ⟨_, N.inv_mem hN, by simpa using hs⟩, fun ⟨z, hz, hxz⟩ => ⟨x * z, hxz, by simpa using hz⟩⟩
