lift' — Mathlib

English

There exists a lift l: A → S.X₁ such that l ≫ S.f = k when S is exact and k ≫ S.g = 0 with S.f mono.

Русский

При точности S и условии k ≫ S.g = 0 и моно S.f существует подъём l: A → S.X₁ такой, что l ≫ S.f = k.

LaTeX

$$$\exists l : A \to S.X_1,\ l \;\;\; S.f = k$$$

Lean4

theorem lift' (hS : S.Exact) {A : C} (k : A ⟶ S.X₂) (hk : k ≫ S.g = 0) [Mono S.f] : ∃ (l : A ⟶ S.X₁), l ≫ S.f = k :=
  ⟨hS.lift k hk, by simp⟩

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