extendCone_obj_π_app' — Mathlib

English

Alternative equation for extendCone's π.app: (extendCone.obj c).π.app Y = c.π.app X then mapped by G.

Русский

Альтернативное равенство π.app у extendCone: (extendCone.obj c).π.app Y = c.π.app X затем отображается через G.

LaTeX

$$$(\\mathrm{extendCone.obj}\ c).\\pi_{Y} = c.\\pi_{X} \\; \\circ \\; G( f ).$$$

Lean4

/-- Alternative equational lemma for `(extendCone c).π.app` in case a lift of the object
is given explicitly. -/
theorem extendCone_obj_π_app' (c : Cone (F ⋙ G)) {X : C} {Y : D} (f : F.obj X ⟶ Y) :
    (extendCone.obj c).π.app Y = c.π.app X ≫ G.map f :=
  by
  apply induction (k₀ := f) (z := rfl) F fun Z g => c.π.app Z ≫ G.map g = c.π.app X ≫ G.map f
  · intro _ _ _ _ _ h₁ h₂
    simp [← h₂, ← h₁, ← Functor.comp_map]
  · intro _ _ _ _ _ h₁ h₂
    simp [← h₁, ← Functor.comp_map, h₂]

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