lift_f — Mathlib

English

If S is exact and k: A → S.X₂ satisfies k ≫ S.g = 0 with S.f mono, then hS.lift k hk ≫ S.f = k.

Русский

Если S точен, k: A → S.X₂ удовлетворяет k ≫ S.g = 0 и S.f моно, тогда hS.lift k hk потом S.f равняется k.

LaTeX

$$$hS.lift k hk \;\; \text{and} \;\; (hS.lift k hk) \;\; \Rightarrow \; (hS.lift k hk) \gg S.f = k$$$

Lean4

@[reassoc (attr := simp)]
theorem lift_f (hS : S.Exact) {A : C} (k : A ⟶ S.X₂) (hk : k ≫ S.g = 0) [Mono S.f] : hS.lift k hk ≫ S.f = k :=
  Fork.IsLimit.lift_ι _

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