inrCompHomotopy_hom_desc_hom — Mathlib

English

In the cylinder construction, the projection ι₀ applied to K composed with desc φ₀ φ₁ h equals φ₀.

Русский

В цилиндрическом конструировании проекция ι₀ применяемая к K, по композиции с desc φ₀ φ₁ h даёт φ₀.

LaTeX

$$$ ι₀ K \\;\\gg\\; desc φ₀ φ₁ h = φ₀. $$$

Lean4

@[reassoc (attr := simp)]
theorem inrCompHomotopy_hom_desc_hom (hc : ∀ j, ∃ i, c.Rel i j) (i j : ι) :
    (inrCompHomotopy φ hc).hom i j ≫ (desc φ α hα).f j = hα.hom i j :=
  by
  by_cases hij : c.Rel j i
  · dsimp
    simp only [inrCompHomotopy_hom φ hc i j hij, desc_f φ α hα _ _ hij, comp_add, inlX_fstX_assoc, inlX_sndX_assoc,
      zero_comp, add_zero]
  · simp only [Homotopy.zero _ _ _ hij, zero_comp]

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