English
The function sigmaLift lifts a family of finite sets f(i) (parametrized by i) to a map on Sigma-objects that, when the base indices agree, yields all combinations in the corresponding γ-set; otherwise it yields empty. It encodes a conditional lifting along the sigma index.
Русский
Функция sigmaLift поднимает семейство конечных множеств f(i) к отображению на сигма-объекты так, что при совпадении базовых индексов получаются все комбинации в соответствующем γ-множество, иначе — пустое множество.
LaTeX
$$$$ \mathrm{sigmaLift}(f)(a,b) = \begin{cases} (f\,(a_2,b_2)) \text{ mapped via } \mathrm{Embedding.sigmaMk}\, a_1, & \text{if } a_1 = b_1, \\ \emptyset, & \text{otherwise}. \end{cases} $$$$
Lean4
/-- Lifts maps `α i → β i → Finset (γ i)` to a map `Σ i, α i → Σ i, β i → Finset (Σ i, γ i)`. -/
def sigmaLift (f : ∀ ⦃i⦄, α i → β i → Finset (γ i)) (a : Sigma α) (b : Sigma β) : Finset (Sigma γ) :=
dite (a.1 = b.1) (fun h => (f (h ▸ a.2) b.2).map <| Embedding.sigmaMk _) fun _ => ∅
