domainUniqueUpToIso_inv_isHomLift

English

The inverse of the domain-unique iso yields a lift with identity on R.

Русский

Обратный к domainUniqueUpToIso даёт подъем с тождеством на R.

LaTeX

$$$IsHomLift (Id_R) (DomainUniqueUpToIso p f φ φ').inv$$$

Lean4

instance domainUniqueUpToIso_inv_isHomLift {a' : 𝒳} (φ' : a' ⟶ b) [IsCartesian p f φ'] :
    IsHomLift p (𝟙 R) (domainUniqueUpToIso p f φ φ').hom :=
  domainUniqueUpToIso_hom p f φ φ' ▸ IsCartesian.map_isHomLift p f φ φ'

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