map_uniq — Mathlib

English

If φ is Cartesian over f, then the map IsCartesian.map p f φ φ is the identity on a.

Русский

Если φ картинизирован над f, то IsCartesian.map p f φ φ = id_a.

LaTeX

$$$IsCartesian.map\\ p\\ f\\ φ\\ φ = 𝟙 a$$$

Lean4

/-- Given a Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and another morphism
`φ' : a' ⟶ b` which also lifts `f`. Then any morphism `ψ : a' ⟶ a` lifting `𝟙 R` such that
`g ≫ ψ = φ'` must equal the map induced from the universal property of `φ`. -/
theorem map_uniq (ψ : a' ⟶ a) [IsHomLift p (𝟙 R) ψ] (hψ : ψ ≫ φ = φ') : ψ = IsCartesian.map p f φ φ' :=
  (Classical.choose_spec <| IsCartesian.universal_property (p := p) (f := f) (φ := φ) φ').2 ψ ⟨inferInstance, hψ⟩

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