of_commsq — Mathlib

English

If h : p.map φ ≫ eqToHom hb = eqToHom ha ≫ f holds (i.e., a commutative square), then p.IsHomLift f φ.

Русский

Если выполняется равенство p.map φ ≫ eqToHom hb = eqToHom ha ≫ f (т.е. диаграмма коммутирует), то φ поднимает f.

LaTeX

$$$$ p.map \; \varphi \; \gg \; \mathrm{eqToHom}(hb) = \mathrm{eqToHom}(ha) \; \gg \; 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 : p.map φ ≫ eqToHom hb = (eqToHom ha) ≫ f) : p.IsHomLift f φ :=
  by
  subst ha hb
  obtain rfl : f = p.map φ := by simpa using h.symm
  infer_instance

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