mono_pullback_to_prod — Mathlib

English

The map X ×[Z] Y → X × Y obtained as a lift from pullback is mono.

Русский

Отображение X ×[Z] Y → X × Y, получаемое как лифт из pullback, моно.

LaTeX

$$$\text{Mono} (\text{prod.lift}(\text{pullback.fst } f g)(\text{pullback.snd } f g)).$$$

Lean4

/-- The map `X ×[Z] Y ⟶ X × Y` is mono. -/
instance mono_pullback_to_prod {C : Type*} [Category C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasBinaryProduct X Y] : Mono (prod.lift (pullback.fst f g) (pullback.snd f g)) :=
  ⟨fun {W} i₁ i₂ h => by
    ext
    · simpa using congrArg (fun f => f ≫ prod.fst) h
    · simpa using congrArg (fun f => f ≫ prod.snd) h⟩

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