cylinderHomotopy — Mathlib

Lean4
/-- (Implementation): The homotopy of the morphisms `cylinder f g ⟶ E ⟶ F`. -/
noncomputable def cylinderHomotopy : Homotopy ((cylinderHom f g).comp f) ((cylinderHom f g).comp g)
    where
  H p := p.2
  a p := pullback.snd _ _
  wl
    p := by
    have : F.p₁ p.snd = pullback.lift _ _ (F.w p.2) ≫ pullback.fst _ _ := by simp
    nth_rw 1 [this]
    rw [← pullback.condition_assoc]
    simp
  wr
    p :=
    by
    have : g.h₀ p.fst = pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) (by simp) ≫ pullback.snd (F.f _) (F.f _) := by simp
    dsimp only [cylinder_X, Hom.comp_s₀, cylinder_I₀, Function.comp_apply, cylinderHom_s₀, Hom.comp_h₀, cylinderHom_h₀]
    nth_rw 3 [this]
    rw [pullback.condition_assoc]
    simp
Похожие утверждения