English
For a monoid hom f: α →* H and a ∈ α, there is a natural equivalence between the fiber f^{-1}({f a}) and the kernel f.ker.
Русский
Для гомоморфизма моноидов f и элемента a существует естественное эквивалентное отображение между фибром f^{-1}({f a}) и ядром f.
LaTeX
$$$f^{-1} \\{f(a)\\} \\cong f.\\ker$$$
Lean4
/-- An equivalence between any non-empty fiber of a `MonoidHom` and its kernel. -/
@[to_additive /-- An equivalence between any non-empty fiber of an `AddMonoidHom` and its kernel. -/
]
def fiberEquivKer (f : α →* H) (a : α) : f ⁻¹' {f a} ≃ f.ker :=
.trans
(Equiv.setCongr <|
Set.ext fun _ => by
rw [mem_preimage, mem_singleton_iff, mem_smul_set_iff_inv_smul_mem, SetLike.mem_coe, mem_ker, smul_eq_mul,
map_mul, map_inv, inv_mul_eq_one, eq_comm])
(Subgroup.leftCosetEquivSubgroup a)
