fiberEquivOfSurjective — Mathlib

English

There is a global equivalence between any two nonempty fibers of a surjective monoid hom.

Русский

Существует глобальная эквивалентность между любыми двумя непустыми фибрами сюръективного гомоморфизма моноидов.

LaTeX

$$f.fiberEquivOfSurjective hf h h' : f^{-1}({h}) ≃ f^{-1}({h'})$$

Lean4

/-- An equivalence between any two fibers of a surjective `MonoidHom`. -/
@[to_additive /-- An equivalence between any two fibers of a surjective `AddMonoidHom`. -/
    ]
noncomputable def fiberEquivOfSurjective {f : α →* H} (hf : Function.Surjective f) (h h' : H) :
    f ⁻¹' { h } ≃ f ⁻¹' { h' } :=
  (fiberEquivKerOfSurjective hf h).trans (fiberEquivKerOfSurjective hf h').symm

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