English
Relates the equation f φ i' with the appropriate inverses and φ.f i, in the liftExtend construction.
Русский
Связь уравнения f φ i' с соответствующими обратными отображениями и φ.f i в конструировании liftExtend.
LaTeX
$$f φ i' = (K.restrictionXIso e hi).inv ≫ φ.f i ≫ (L.extendXIso e hi).inv$$
Lean4
@[reassoc (attr := simp)]
theorem comm (hφ : e.HasLift φ) (i' j' : ι') : f φ i' ≫ (L.extend e).d i' j' = K.d i' j' ≫ f φ j' :=
by
by_cases hij' : c'.Rel i' j'
· by_cases hi' : ∃ i, e.f i = i'
· obtain ⟨i, hi⟩ := hi'
rw [f_eq φ hi]
by_cases hj' : ∃ j, e.f j = j'
· obtain ⟨j, hj⟩ := hj'
rw [f_eq φ hj, L.extend_d_eq e hi hj]
subst hi hj
simp [HomologicalComplex.restrictionXIso]
· apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt
· have : (L.extend e).d i' j' = 0 := by apply (L.isZero_extend_X e i' (by simpa using hi')).eq_of_src
rw [this, comp_zero]
by_cases hj' : ∃ j, e.f j = j'
· obtain ⟨j, rfl⟩ := hj'
rw [f_eq φ rfl]
dsimp [restrictionXIso]
rw [id_comp, reassoc_of% (hφ j (e.boundaryGE hij' (by simpa using hi')) i' hij'), zero_comp]
· have : f φ j' = 0 := by apply (L.isZero_extend_X e j' (by simpa using hj')).eq_of_tgt
rw [this, comp_zero]
· simp [HomologicalComplex.shape _ _ _ hij']
