comp_lift_id_left' — Mathlib

English

If b' is a replacement for b (b = b'), then p.IsHomLift f (φ ≫ eqToHom h) holds.

Русский

Если b заменился на b' (b = b'), тогда p.IsHomLift f (φ ≫ eqToHom h) выполняется.

LaTeX

$$$$ p.IsHomLift f (\varphi \gg eqToHom h) $$$$

Lean4

/-- If `φ : a ⟶ b` lifts `𝟙 T` and `ψ : b ⟶ c` lifts `f`, then `φ  ≫ ψ` lifts `f` -/
theorem comp_lift_id_left' {a b c : 𝒳} (R : 𝒮) (φ : a ⟶ b) [p.IsHomLift (𝟙 R) φ] {S T : 𝒮} (f : S ⟶ T) (ψ : b ⟶ c)
    [p.IsHomLift f ψ] : p.IsHomLift f (φ ≫ ψ) :=
  by
  obtain rfl : R = S := by rw [← codomain_eq p (𝟙 R) φ, domain_eq p f ψ]
  infer_instance

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