map_uniq — Mathlib

English

The map produced by the strongly Cartesian construction is itself a lift of g along p.

Русский

Отображение, полученное конструированием strongly Cartesian, само является подъёмом g вдоль p.

LaTeX

$$$\\text{map\_isHomLift}(p,f,g,φ,hf',φ') :\\; IsHomLift(p,g,\\text{map}(p,f,φ,hf',φ')).$$$

Lean4

/-- Given a diagram
```
a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S
```
such that `φ` is strongly Cartesian, and morphisms `φ' : a' ⟶ b`, `ψ : a' ⟶ a` such that
`ψ ≫ φ = φ'`. Then `ψ` is the map induced by the universal property. -/
theorem map_uniq (ψ : a' ⟶ a) [IsHomLift p g ψ] (hψ : ψ ≫ φ = φ') : ψ = map p f φ hf' φ' :=
  (Classical.choose_spec <| universal_property p f φ _ _ hf' φ').2 ψ ⟨inferInstance, hψ⟩

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