isIso_diagonal_iff — Mathlib

English

If f is mono, then diagonal f is an isomorphism.

Русский

Если f моно, то диагональная сумма δ_f является изоморфизмом.

LaTeX

$$$ \\operatorname{Mono}(f) \\Rightarrow \\operatorname{IsIso}(\\operatorname{diagonal}(f)). $$$

Lean4

theorem isIso_diagonal_iff : IsIso (diagonal f) ↔ Mono f :=
  ⟨fun H ↦
    ⟨fun _ _ e ↦ by
      rw [← lift_fst _ _ e, (cancel_epi (g := fst f f) (h := snd f f) (diagonal f)).mp (by simp), lift_snd]⟩,
    fun _ ↦ inferInstance⟩

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