extendMap_zero — Mathlib

English

Extending op along e preserves the differential structure via a coherent isomorphism to the opposite of extension.

Русский

Расширение противолежащего направления вдоль e сохраняет дифференциал через согласованный изоморфизм к противоположному расширению.

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_zero : extendMap (0 : K ⟶ L) e = 0 := 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

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