mono_iff_isIso_fst — Mathlib

English

Same as above: Mono f iff IsIso c.fst.

Русский

То же: Mono f эквивалентно IsIso c.fst.

LaTeX

$$$(\text{mono } f) \Leftrightarrow IsIso c.fst$$$

Lean4

theorem mono_iff_isIso_fst (hc : IsLimit c) : Mono f ↔ IsIso c.fst :=
  by
  rw [mono_iff_fst_eq_snd hc]
  constructor
  · intro h
    obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
    refine ⟨φ, PullbackCone.IsLimit.hom_ext hc ?_ ?_, hφ₁⟩
    · simp only [assoc, hφ₁, id_comp, comp_id]
    · simp only [assoc, hφ₂, id_comp, comp_id, h]
  · intro
    obtain ⟨φ, hφ₁, hφ₂⟩ := PullbackCone.IsLimit.lift' hc (𝟙 X) (𝟙 X) (by simp)
    have : IsSplitEpi φ := IsSplitEpi.mk ⟨SplitEpi.mk c.fst (by rw [← cancel_mono c.fst, assoc, id_comp, hφ₁, comp_id])⟩
    rw [← cancel_epi φ, hφ₁, hφ₂]

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