English
For i,j in an indexing set and x,y in respective fibers, (Sigma.ι f i).base x = (Sigma.ι f j).base y iff (Sigma.mk i x) = (Sigma.mk j y).
Русский
Для i,j в индексационном множестве и x,y в соответствующих фибрах, имеет место равенство базовых координат морфизмов; эквивалентно равенству сигма-мк.
LaTeX
$$$(\\Sigma.ι f i).\\text{base} x = (\\Sigma.ι f j).\\text{base} y \\;\\Longleftrightarrow\\; (\\Sigma.mk\, i\, x) = (\\Sigma.mk\, j\, y)$$$
Lean4
theorem sigmaι_eq_iff (i j : ι) (x y) :
(Sigma.ι f i).base x = (Sigma.ι f j).base y ↔ (Sigma.mk i x : Σ i, f i) = Sigma.mk j y :=
by
refine (Scheme.IsLocallyDirected.ι_eq_ι_iff _).trans ⟨?_, ?_⟩
· rintro ⟨k, ⟨⟨⟨⟩⟩⟩, ⟨⟨⟨⟩⟩⟩, x, rfl, rfl⟩; simp
· simp only [Discrete.functor_obj_eq_as, Sigma.mk.injEq]
rintro ⟨rfl, e⟩
obtain rfl := (heq_eq_eq x y).mp e
exact ⟨⟨i⟩, 𝟙 _, 𝟙 _, x, by simp⟩
