eq_of_isHomLift — Mathlib

English

If φ is a morphism in a fiber p and f: p.obj a ⟶ p.obj b arises as a map with IsHomLift data, then f = p.map φ.

Русский

Если φ — морфизм внутри фибры p, а f является соответствием IsHomLift, то f = p.map φ.

LaTeX

$$$f = p.map\\ φ$$$

Lean4

theorem eq_of_isHomLift {a b : 𝒳} (f : p.obj a ⟶ p.obj b) (φ : a ⟶ b) [p.IsHomLift f φ] : f = p.map φ := by
  simp only [fac p f φ, eqToHom_refl, comp_id, id_comp]

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