English
If ψ is Cartesian and φ is a hom lift, then the inducedMap comp property yields (ι R).map (inducedMap f ψ φ) ≫ ψ = φ.
Русский
Если ψ картезианален и φ подъем морфизма, то свойство inducedMap comp даёт (ι R).map (inducedMap f ψ φ) ≫ ψ = φ.
LaTeX
$$$ (ι R).map (inducedMap f ψ φ) ≫ ψ = φ $$$
Lean4
/-- Given `a : 𝒳`, `b : Fib p R`, and a diagram
```
b --φ--> a
- -
| |
v v
R --f--> S
```
It can be factorized as
```
b --τ--> b'--ψ--> a
- - -
| | |
v v v
R ====== R --f--> S
```
with `ψ` Cartesian over `f` and `τ` a map in `Fib p R`. -/
theorem fiber_factorization (ha : p.obj a = S) {b : Fib p R} (f : R ⟶ S) (φ : (ι R).obj b ⟶ a) [IsHomLift p f φ] :
∃ (b' : Fib p R) (τ : b ⟶ b') (ψ : (ι R).obj b' ⟶ a), IsStronglyCartesian p f ψ ∧ (((ι R).map τ) ≫ ψ = φ) :=
let ψ := pullbackMap f ha
⟨mkPullback f ha, inducedMap f ψ φ, ψ, inferInstance, inducedMap_comp f ψ φ⟩
