isIso_of_mono_of_eq_card_fiber — Mathlib

English

A mono between objects with equally sized fibers is an iso.

Русский

Мономорфизм между объектами с равной размерностью фиберной оболочки является изоморфизмом.

LaTeX

$$((Mono f) \land Nat.card (F.obj X).carrier = Nat.card (F.obj Y).carrier) \rightarrow IsIso f$$

Lean4

/-- A mono between objects with equally sized fibers is an iso. -/
theorem isIso_of_mono_of_eq_card_fiber {X Y : C} (f : X ⟶ Y) [Mono f] (h : Nat.card (F.obj X) = Nat.card (F.obj Y)) :
    IsIso f :=
  by
  have : IsIso (F.map f) := by
    apply (ConcreteCategory.isIso_iff_bijective (F.map f)).mpr
    apply (Fintype.bijective_iff_injective_and_card (F.map f)).mpr
    refine ⟨injective_of_mono_of_preservesPullback (F.map f), ?_⟩
    simp only [← Nat.card_eq_fintype_card, h]
  exact isIso_of_reflects_iso f F

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