English
Equivalence for Sigma-type data: two extended data (α, hα) are equal iff their first components are equal and all components agree pointwise on indices with the relation c.Rel.
Русский
Эквивалентность для данных типа сигма: два расширенных набора (α, hα) равны тогда и только тогда, когда их первые компоненты равны и все компоненты согласованы точечно по отношению c.Rel.
LaTeX
$$$ x = y \\iff x.1 = y.1 \\land (\\forall i j, c.Rel j i \\Rightarrow x.2.hom i j = y.2.hom i j) $$$
Lean4
theorem descSigma_ext_iff {φ : F ⟶ G} {K : HomologicalComplex C c} (x y : Σ (α : G ⟶ K), Homotopy (φ ≫ α) 0) :
x = y ↔ x.1 = y.1 ∧ (∀ (i j : ι) (_ : c.Rel j i), x.2.hom i j = y.2.hom i j) :=
by
constructor
· rintro rfl
tauto
· obtain ⟨x₁, x₂⟩ := x
obtain ⟨y₁, y₂⟩ := y
rintro ⟨rfl, h⟩
simp only [Sigma.mk.inj_iff, heq_eq_eq, true_and]
ext i j
by_cases hij : c.Rel j i
· exact h _ _ hij
· simp only [Homotopy.zero _ _ _ hij]
