liftStar_lift_map — Mathlib

English

A compatibility identity between the lift and liftStar constructions holds at x, mirroring the previous lift compatibility statement.

Русский

Сохраняется совместимость между конструкциями lift и liftStar в точке x, аналогично предыдущему утверждению о совместимости.

LaTeX

$$(liftStar F M hM).hom ≫ (starInitial.to (incl.obj x)) = M x ≫ (inclLift F M hM).hom.app x$$

Lean4

theorem liftStar_lift_map {D : Type*} [Category D] {Z : D} (F : C ⥤ D) (M : ∀ x : C, Z ⟶ F.obj x)
    (hM : ∀ (x y : C) (f : x ⟶ y), M x ≫ F.map f = M y) (x : C) :
    (liftStar F M hM).hom ≫ (lift F M hM).map (starInitial.to (incl.obj x)) = M x ≫ (inclLift F M hM).hom.app x :=
  by
  erw [Category.id_comp, Category.comp_id]
  rfl

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