exists_isCartesian — Mathlib

English

In a prefibered context, for any a with p.obj a = S and arrow f: R ⟶ S, there exists a Cartesian lift: a morphism φ: b ⟶ a with IsCartesian property.

Русский

В префабрифицированном контексте для любого a с p.obj a = S и стрелы f: R ⟶ S существует картизантный подъем: φ: b ⟶ a s IsCartesian.

LaTeX

$$$\exists b, φ : b \to a, IsCartesian\ p\ f\ φ$$$

Lean4

protected theorem exists_isCartesian (p : 𝒳 ⥤ 𝒮) [p.IsPreFibered] {a : 𝒳} {R S : 𝒮} (ha : p.obj a = S) (f : R ⟶ S) :
    ∃ (b : 𝒳) (φ : b ⟶ a), IsCartesian p f φ := by subst ha; exact IsPreFibered.exists_isCartesian' f

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