nullHomotopicMap'_f — Mathlib

English

The f-component of nullHomotopicMap' h equals the differential composition with h along r₁₀.

Русский

Компонента f у nullHomotopicMap' h равна дифференциалу, композиционному с h по r₁₀.

LaTeX

$$$ (\\mathrm{nullHomotopicMap'} \\; h).f\\; k_1 = C.d_{k_1,k_0} \\circ h_{k_0,k_1}\\, r_{1 0} $$$

Lean4

theorem nullHomotopicMap'_f {k₂ k₁ k₀ : ι} (r₂₁ : c.Rel k₂ k₁) (r₁₀ : c.Rel k₁ k₀)
    (h : ∀ i j, c.Rel j i → (C.X i ⟶ D.X j)) :
    (nullHomotopicMap' h).f k₁ = C.d k₁ k₀ ≫ h k₀ k₁ r₁₀ + h k₁ k₂ r₂₁ ≫ D.d k₂ k₁ :=
  by
  simp only [nullHomotopicMap']
  rw [nullHomotopicMap_f r₂₁ r₁₀]
  split_ifs
  rfl
    -- Cannot be @[simp] because `k₁` cannot be inferred by `simp`.

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