of_commSq — Mathlib

English

If h : CommSq (p.map φ) (eqToHom ha) (eqToHom hb) f, then p.IsHomLift f φ.

Русский

Если h задаёт CommSq для p.map φ, eqToHom ha, eqToHom hb и f, то φ является подъемом.

LaTeX

$$$$ \text{CommSq}(p.map(\varphi), \mathrm{eqToHom}(ha), \mathrm{eqToHom}(hb), f) \Rightarrow p.IsHomLift f \; \varphi $$$$

Lean4

theorem of_commSq {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) (ha : p.obj a = R) (hb : p.obj b = S)
    (h : CommSq (p.map φ) (eqToHom ha) (eqToHom hb) f) : p.IsHomLift f φ :=
  of_commsq p f φ ha hb h.1

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