fiberEquivKerOfSurjective — Mathlib

English

For a surjective monoid hom f, and h ∈ H, there is an equivalence between the fiber f^{-1}({h}) and the kernel f.ker.

Русский

Для сюръективного гомоморфизма f и h ∈ H существует эквивалентность между фиберf^{-1}({h}) и ядром f.

LaTeX

$$$f^{-1}\\{h\\} \\simeq f.\\ker$ for surjective f$$

Lean4

/-- An equivalence between any fiber of a surjective `MonoidHom` and its kernel. -/
@[to_additive /-- An equivalence between any fiber of a surjective `AddMonoidHom` and its kernel. -/
    ]
noncomputable def fiberEquivKerOfSurjective {f : α →* H} (hf : Function.Surjective f) (h : H) : f ⁻¹' { h } ≃ f.ker :=
  (hf h).choose_spec ▸ f.fiberEquivKer (hf h).choose

Похожие утверждения