eq_d₂₁_comp_inv — Mathlib

English

Dual commuting relation: the inverse of the second chains iso composed with d21 equals d21 composed with the inverse of the second isomorphism.

Русский

Двойственная коммутация: обратное цепное изоморфизм вторичного уровня сочетается с d21 так же, как d21 сочетается с обратным изоморфизмом.

LaTeX

$$$(\text{chainsIso}_2 A)^{-1} \circ (\operatorname{inhomogeneousChains} A).d 2 1 = d_{21} A \circ (\text{chainsIso}_1 A)^{-1}$$$

Lean4

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

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