eq_d₁₀_comp_inv — Mathlib

English

The two natural ways of transporting the differential d10 through the inverse chains iso commute, giving equality of composites.

Русский

Два естественных способа перенести дифференциал d10 через обратное цепное изоморфизм цепей согласуются, давая равенство композит.

LaTeX

$$$(\text{chainsIso}_1 A)^{-1} \circ (\operatorname{inhomogeneousChains} A).d 1 0 = d_{10} A \circ (\text{chainsIso}_0 A)^{-1}$$$

Lean4

@[reassoc (attr := simp), elementwise (attr := simp)]
theorem eq_d₁₀_comp_inv : (chainsIso₁ A).inv ≫ (inhomogeneousChains A).d 1 0 = d₁₀ A ≫ (chainsIso₀ A).inv :=
  (CommSq.horiz_inv ⟨comp_d₁₀_eq A⟩).w

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