of_fac' — Mathlib

English

If p.map φ = eqToHom ha ≫ f ≫ eqToHom hb.symm with ha: p.obj a = R and hb: p.obj b = S, then p.IsHomLift f φ.

Русский

Если p.map φ = eqToHom ha ≫ f ≫ eqToHom hb.symm при ha: p.obj a = R и hb: p.obj b = S, тогда φ является подъемом над f.

LaTeX

$$$$ p.map \; \varphi = \mathrm{eqToHom}(ha) \; \gg \; f \; \gg \; \mathrm{eqToHom}(hb^{\mathrm{symm}}) $$ implies $$ p.IsHomLift f \; \varphi $$$$

Lean4

theorem of_fac' {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S)
    (h : p.map φ = eqToHom ha ≫ f ≫ eqToHom hb.symm) : p.IsHomLift f φ :=
  by
  subst ha hb
  obtain rfl : f = p.map φ := by simpa using h.symm
  infer_instance

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