monomorphisms — Mathlib

English

The base-change stability for monomorphisms holds.

Русский

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

LaTeX

$$IsStableUnderBaseChange.monomorphisms$$

Lean4

instance monomorphisms : (monomorphisms C).IsStableUnderBaseChange where
  of_isPullback {X Y Y' S f g f' g'} h
    hg := by
    have : Mono g := hg
    constructor
    intro Z f₁ f₂ h₁₂
    apply PullbackCone.IsLimit.hom_ext h.isLimit
    · rw [← cancel_mono g]
      dsimp
      simp only [Category.assoc, h.w, reassoc_of% h₁₂]
    · exact h₁₂

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