fiberEquiv — Mathlib

English

There is a canonical equivalence between any two nonempty fibers of a monoid hom f.

Русский

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

LaTeX

$$f.fiberEquiv a b : f^{-1}({f a}) ≃ f^{-1}({f b})$$

Lean4

/-- An equivalence between any two non-empty fibers of a `MonoidHom`. -/
@[to_additive /-- An equivalence between any two non-empty fibers of an `AddMonoidHom`. -/
    ]
def fiberEquiv (f : α →* H) (a b : α) : f ⁻¹' {f a} ≃ f ⁻¹' {f b} :=
  (f.fiberEquivKer a).trans (f.fiberEquivKer b).symm

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