equiv_mk₀ — Mathlib

English

If m0 = 0, then mk₀ W m0 hm0 f corresponds under the equivalence to L.map f via a simple sketch.

Русский

Если m0 = 0, то mk₀_W m0 hm0 f сопоставляется через эквивалентность с L.map f.

LaTeX

$$$\mathrm{equiv}\,W\,L\big(\mathrm{SmallShiftedHom.mk₀}\,W\,m_0\,hm_0\,f\big) = \mathrm{ShiftedHom.mk₀}\,m_0\,hm_0\,(L.map f)$$$

Lean4

@[simp]
theorem equiv_mk₀ [HasSmallLocalizedShiftedHom.{w} W M X Y] (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) :
    equiv W L (SmallShiftedHom.mk₀ W m₀ hm₀ f) = ShiftedHom.mk₀ m₀ hm₀ (L.map f) :=
  by
  subst hm₀
  dsimp [equiv, mk₀]
  erw [SmallHom.equiv_mk, Iso.homToEquiv_apply, Functor.map_comp]
  dsimp [equiv, mk₀, ShiftedHom.mk₀, shiftFunctorZero']
  simp only [comp_id, L.commShiftIso_zero, Functor.CommShift.isoZero_hom_app, assoc, ← Functor.map_comp_assoc,
    Iso.inv_hom_id_app, Functor.id_obj, Functor.map_id, id_comp]

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