isLocallyBijective_iff_isIso — Mathlib

English

W f is equivalent to f being locally bijective (locally injective and locally surjective).

Русский

W f эквивалентно тому, что f локально биективен (локально инъективен и локально сюръективен).

LaTeX

$$$J.W f \iff (\mathrm{Presheaf.IsLocallyInjective} J f \land \mathrm{Presheaf.IsLocallySurjective} J f).$$$

Lean4

theorem isLocallyBijective_iff_isIso : IsLocallyInjective f ∧ IsLocallySurjective f ↔ IsIso f :=
  by
  constructor
  · rintro ⟨_, _⟩
    rw [← isIso_iff_of_reflects_iso f (sheafCompose J (forget A)), ← isLocallyBijective_iff_isIso']
    constructor <;> infer_instance
  · intro
    constructor <;> infer_instance

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