reflects_mono_of_reflectsLimit — Mathlib

English

If F reflects pullbacks, then it reflects monomorphisms.

Русский

ЕслиF отражает pullbacks, то он отражает мономорфизмы.

LaTeX

$$$\\text{ReflectsLimit}(\\mathrm{cospan}\\ f\\ f)\\ F]\\;\\land\\ mono(F.map f) \\Rightarrow mono(f)$$$

Lean4

/-- If `F` reflects pullbacks, then it reflects monomorphisms. -/
theorem reflects_mono_of_reflectsLimit {X Y : C} (f : X ⟶ Y) [ReflectsLimit (cospan f f) F] [Mono (F.map f)] : Mono f :=
  by
  have := PullbackCone.isLimitMkIdId (F.map f)
  simp_rw [← F.map_id] at this
  apply PullbackCone.mono_of_isLimitMkIdId _ (isLimitOfIsLimitPullbackConeMap F _ this)

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