ext — Mathlib

English

The inverse of the domain-unique isomorphism has a lifting structure over the identity on the domain.

Русский

Обратный к доменной уникальной изоморфности имеет подъем над тождественным отображением на области.

LaTeX

$$$IsHomLift p (\\mathsf{Id}_R) (domainUniqueUpToIso p f φ φ').inv$$$

Lean4

/-- Given a Cartesian morphism `φ : a ⟶ b` lying over `f : R ⟶ S` in `𝒳`, and two morphisms
`ψ ψ' : a' ⟶ a` such that `ψ ≫ φ = ψ' ≫ φ`. Then we must have `ψ = ψ'`. -/
protected theorem ext (φ : a ⟶ b) [IsCartesian p f φ] {a' : 𝒳} (ψ ψ' : a' ⟶ a) [IsHomLift p (𝟙 R) ψ]
    [IsHomLift p (𝟙 R) ψ'] (h : ψ ≫ φ = ψ' ≫ φ) : ψ = ψ' := by
  rw [map_uniq p f φ (ψ ≫ φ) ψ rfl, map_uniq p f φ (ψ ≫ φ) ψ' h.symm]

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