extendMap_id — Mathlib

English

The differential in the opposite extension is given by composing the extendXIso with the differential and its inverse, in the opposite direction.

Русский

Дифференциал в противоположном расширении задаётся композицией extendXIso с дифференциалом и его обратной, в противоположном направлении.

LaTeX

$$$(K.op.extend e.op).d i' j' = (K.extendOpIso e).hom.f i' \\circ ((K.extend e).d j' i').op \\circ (K.extendOpIso e).inv.f j'$$$

Lean4

@[simp]
theorem extendMap_id : extendMap (𝟙 K) e = 𝟙 _ := by
  ext i'
  by_cases hi' : ∃ i, e.f i = i'
  · obtain ⟨i, hi⟩ := hi'
    simp [extendMap_f _ e hi]
  · apply (K.isZero_extend_X e i' (fun i hi => hi' ⟨i, hi⟩)).eq_of_src

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