lift_fst — 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) ≫ a = p.

Русский

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

LaTeX

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

Lean4

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

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