English
If there exists for every object a Cartesian lift for every arrow, then the functor is fibered; equivalently, existence of strongly Cartesian lifts implies fiberedness.
Русский
Если для каждого объекта существует картизантный подъем для каждого стрелы, то функтор является фиберированным; существование сильнокартезиановых подъемов эквивалентно фиберированности.
LaTeX
$$$\forall a, \exists b, φ: IsStronglyCartesian p f φ \Rightarrow IsFibered p$$$
Lean4
/-- Alternate constructor for `IsFibered`, a functor `p : 𝒳 ⥤ 𝒴` is fibered if any diagram of the
form
```
a
-
|
v
R --f--> p(a)
```
admits a strongly Cartesian lift `b ⟶ a` of `f`. -/
theorem of_exists_isStronglyCartesian {p : 𝒳 ⥤ 𝒮}
(h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ (b : 𝒳) (φ : b ⟶ a), IsStronglyCartesian p f φ) : IsFibered p
where
exists_isCartesian' := by
intro a R f
obtain ⟨b, φ, hφ⟩ := h a R f
refine ⟨b, φ, inferInstance⟩
comp := fun R S T f g {a b c} φ ψ _ _ =>
have : p.IsStronglyCartesian f φ := isStronglyCartesian_of_exists_isCartesian p h _ _
have : p.IsStronglyCartesian g ψ := isStronglyCartesian_of_exists_isCartesian p h _ _
inferInstance
