English
Two elements ⟨i,x⟩ and ⟨j,y⟩ of the sigma type are equivalent if they coincide in some common later stage k ≥ i,j after transferring along embeddings.
Русский
Два элемента в Σˣ f эквивалентны, если они становятся равны в некоторой общей более поздней ступени k.
LaTeX
$$$\\exists k\\ge i,j, f_{i,k}(x)=f_{j,k}(y)$$$
Lean4
/-- The directed limit glues together the structures along the embeddings. -/
def setoid [DirectedSystem G fun i j h => f i j h] [IsDirected ι (· ≤ ·)] : Setoid (Σˣ f)
where
r := fun ⟨i, x⟩ ⟨j, y⟩ => ∃ (k : ι) (ik : i ≤ k) (jk : j ≤ k), f i k ik x = f j k jk y
iseqv :=
⟨fun ⟨i, _⟩ => ⟨i, refl i, refl i, rfl⟩, @fun ⟨_, _⟩ ⟨_, _⟩ ⟨k, ik, jk, h⟩ => ⟨k, jk, ik, h.symm⟩,
@fun ⟨i, x⟩ ⟨j, y⟩ ⟨k, z⟩ ⟨ij, hiij, hjij, hij⟩ ⟨jk, hjjk, hkjk, hjk⟩ =>
by
obtain ⟨ijk, hijijk, hjkijk⟩ := directed_of (· ≤ ·) ij jk
refine ⟨ijk, le_trans hiij hijijk, le_trans hkjk hjkijk, ?_⟩
rw [← DirectedSystem.map_map _ hiij hijijk, hij, DirectedSystem.map_map]
rw [← DirectedSystem.map_map _ hkjk hjkijk, ← hjk, DirectedSystem.map_map]⟩
