d₁₀ArrowIso — Mathlib

English

There is an isomorphism of arrows between the arrow G→0 A with differential d10 and the arrow of the inhomogeneous chain differential d10.

Русский

Существует изоморфизм стрел между стрелой G →0 A с дифференциалом d10 и стрелой дифференциала d10 для неоднородных цепей.

LaTeX

$$$\text{d}_{10} \text{ArrowIso} : \big( (G \to\! A)_0 \xrightarrow{d_{10}} A\big) \cong \big( (\mathrm{inhomogeneousChains} A).d\ 1\ 0 \big)$$$

Lean4

/-- The arrow `(G →₀ A) --d₁₀--> A` is isomorphic to the differential
`(inhomogeneousChains A).d 1 0` of the complex of inhomogeneous chains of `A`. -/
@[simps! hom_left hom_right inv_left inv_right]
def d₁₀ArrowIso : Arrow.mk ((inhomogeneousChains A).d 1 0) ≅ Arrow.mk (d₁₀ A) :=
  Arrow.isoMk (chainsIso₁ A) (chainsIso₀ A) (comp_d₁₀_eq A)

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