inlX_desc_f — Mathlib

English

There is a canonical equivalence between pairs (α, hα) with hα a homotopy from φ ≫ α to 0 and morphisms homotopyCofiber φ → K.

Русский

Существует каноническая эквивалентность между парами (α, hα) с гомотопией hα от φ ≫ α к 0 и морфизмами от homotopyCofiber φ к K.

LaTeX

$$$\\text{descEquiv}_{φ}(K) : (\\alpha : G ⟶ K) × Homotopy (φ ∘ α) 0 ≃ (homotopyCofiber φ ⟶ K).$$$

Lean4

@[reassoc (attr := simp)]
theorem inlX_desc_f (i j : ι) (hjk : c.Rel j i) : inlX φ i j hjk ≫ (desc φ α hα).f j = hα.hom i j :=
  by
  obtain rfl := c.next_eq' hjk
  dsimp [desc]
  rw [dif_pos hjk, comp_add, inlX_fstX_assoc, inlX_sndX_assoc, zero_comp, add_zero]

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