extendCocone_obj_ι_app' — Mathlib

English

Alternative equational lemma for extendCocone.obj’s ι.app when a lift is given.

Русский

Альтернативная лемма равенств для ι.app extendCocone.obj, когда дан подъём.

LaTeX

$$$$ (\text{extendCocone.obj } c).\iota_{X} = G.map f \circ c.\iota_{Y}. $$$$

Lean4

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

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