strongMono_of_regularMono — Mathlib

English

If C is a IsRegularMonoCategory, then it is a StrongMonoCategory.

Русский

Если C является IsRegularMonoCategory, то она является StrongMonoCategory.

LaTeX

$$[IsRegularMonoCategory C] ⇒ [StrongMonoCategory C]$$

Lean4

instance (priority := 100) strongMono_of_regularMono (f : X ⟶ Y) [RegularMono f] : StrongMono f :=
  StrongMono.mk'
    (by
      intro A B z hz u v sq
      have : v ≫ (RegularMono.left : Y ⟶ RegularMono.Z f) = v ≫ RegularMono.right :=
        by
        apply (cancel_epi z).1
        repeat (rw [← Category.assoc, ← eq_whisker sq.w])
        simp only [Category.assoc, RegularMono.w]
      obtain ⟨t, ht⟩ := RegularMono.lift' _ _ this
      refine CommSq.HasLift.mk' ⟨t, (cancel_mono f).1 ?_, ht⟩
      simp only [Category.assoc, ht, sq.w])

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