English
There is an isomorphism between the restriction of the cochain complex and the original K in degrees ≥ 0.
Русский
Существуют изоморфизм ограничение коцепного комплекса и исходного K в степенях ≥ 0.
LaTeX
$$restrictionGEIso : h.cochainComplex.restriction (ComplexShape.embeddingUpIntGE 0) ≅ L$$
Lean4
/-- If `h : ConnectData K L`, then `h.cochainComplex` identifies to `K` in degrees `≤ -1`. -/
@[simps!]
def restrictionLEIso : h.cochainComplex.restriction (ComplexShape.embeddingUpIntLE (-1)) ≅ K :=
Hom.isoOfComponents
(fun n ↦
h.cochainComplex.restrictionXIso (ComplexShape.embeddingUpIntLE (-1)) (i := n) (i' := .negSucc n)
(by dsimp; cutsat))
(by
rintro _ n rfl
dsimp only
rw [restriction_d_eq (e := (ComplexShape.embeddingUpIntLE (-1))) _ (i' := Int.negSucc (n + 1)) (j' :=
Int.negSucc n) (by dsimp; cutsat) (by dsimp; cutsat),
cochainComplex_d, d_negSucc]
simp)
