lift_map_liftStar — Mathlib

English

A compatibility equation holds between the lift and liftStar constructions at each object x: the two canonical composites coincide.

Русский

Для каждого объекта x выполняется соотношение совместимости между конструкциями lift и liftStar: два канонических композиции совпадают.

LaTeX

$$$(lift F M hM).map (starTerminal.from (incl.obj x)) \;≫\; (liftStar F M hM).hom = (inclLift F M hM).hom.app x \;≫\; M x$$$

Lean4

theorem lift_map_liftStar {D : Type*} [Category D] {Z : D} (F : C ⥤ D) (M : ∀ x : C, F.obj x ⟶ Z)
    (hM : ∀ (x y : C) (f : x ⟶ y), F.map f ≫ M y = M x) (x : C) :
    (lift F M hM).map (starTerminal.from (incl.obj x)) ≫ (liftStar F M hM).hom = (inclLift F M hM).hom.app x ≫ M x :=
  by
  simp
  rfl

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