lift_snd — Mathlib

English

Given a kernel pair k of f, with p,q:S→X and w:p ≫ f = q ≫ f, the lift satisfies (k.lift p q w) ≫ b = q.

Русский

Для kernel-пары k морфизмов f и произвольных p,q:S→X и w: p ≫ f = q ≫ f, лифт удовлетворяет (k.lift p q w) ≫ b = q.

LaTeX

$$$k.lift\\ p\\ q\\ w \\;≫\\; b = q$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_snd {S : C} (k : IsKernelPair f a b) (p q : S ⟶ X) (w : p ≫ f = q ≫ f) : k.lift p q w ≫ b = q :=
  PullbackCone.IsLimit.lift_snd _ _ _ _

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