d_eq_unop_d — Mathlib

English

The same identity as in d_eq_unop_d holds after transporting X along the cosimplicialSimplicialEquiv equivalence.

Русский

Та же тождество сохраняется после переноса X по эквивалентности cosimplicialSimplicialEquiv.

LaTeX

$$$\text{objD } X\ n = (\text{AlternatingFaceMapComplex.objD}((\cosimplicialSimplicialEquiv C).\mathrm{functor.obj}(\mathrm{op} X))\ n).\mathrm{unop}$$$

Lean4

theorem d_eq_unop_d (n : ℕ) :
    objD X n = (AlternatingFaceMapComplex.objD ((cosimplicialSimplicialEquiv C).functor.obj (op X)) n).unop :=
  by
  simp only [objD, AlternatingFaceMapComplex.objD, unop_sum, unop_zsmul]
  rfl

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