homEquiv — Mathlib

English

Composition with a shifted object mk₀ is compatible: composing mk₀ with another shifted morphism yields mk₀ with the composed morphism, after adjusting indices via the provided equation h.

Русский

Сочетание с mk₀ совместимо: композиция mk₀ с другим сдвиговым морфизмом даёт mk₀ с объединённым морфизмом после корректировки индексов.

LaTeX

$$f.comp (mk₀ m₀ hm₀ g) h = mk₀ c (by rw [← h, hm₀, add_zero]) (f ≫ g) with mk₀$$

Lean4

/-- The bijection `(X ⟶ Y) ≃ ShiftedHom X Y m₀` when `m₀ = 0`. -/
@[simps apply]
noncomputable def homEquiv (m₀ : M) (hm₀ : m₀ = 0) : (X ⟶ Y) ≃ ShiftedHom X Y m₀
    where
  toFun f := mk₀ m₀ hm₀ f
  invFun g := g ≫ (shiftFunctorZero' C m₀ hm₀).hom.app Y
  left_inv f := by simp [mk₀]
  right_inv g := by simp [mk₀]

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