isoOfIsoLift_inv_hom_id — Mathlib

English

If f : R ⟶ S and φ : a ≅ b with p.IsHomLift f.hom φ.hom, then the inverse lift through isoOfIsoLift has its left inverse property: (isoOfIsoLift p f φ).inv ≫ f = 1_S.

Русский

Если f : R ⟶ S и φ : a ≅ b с тем, что p.IsHomLift f.hom φ.hom, то через изоморфизм isoOfIsoLift выполняется l (= инверсии): (isoOfIsoLift p f φ).inv ≫ f = 1_S.

LaTeX

$$$\forall {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b)\ [p.IsHomLift f.hom φ.hom],\ (isoOfIsoLift p f φ).inv ≫ f = 𝟙_S$$$

Lean4

@[simp]
theorem isoOfIsoLift_inv_hom_id (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] : (isoOfIsoLift p f φ).inv ≫ f = 𝟙 S :=
  (isoOfIsoLift p f φ).inv_hom_id

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