English
Under pairwise disjointness and small-sigma indexing, the Sigma.desc construction yields an open immersion.
Русский
При парном взаимно непересечении и малом индексе сигмы, конструкция Sigma.desc дает открытое вложение.
LaTeX
$$$\\IsOpenImmersion(\\Sigma.desc\\, \\lambda i, \\alpha_i\\ )$$$
Lean4
theorem isOpenImmersion_sigmaDesc [Small.{u} σ] {X : Scheme.{u}} (α : ∀ i, g i ⟶ X) [∀ i, IsOpenImmersion (α i)]
(hα : Pairwise (Disjoint on (Set.range <| α · |>.base))) : IsOpenImmersion (Sigma.desc α) :=
by
obtain ⟨ι, ⟨e⟩⟩ := Small.equiv_small (α := σ)
convert IsOpenImmersion.comp ((Sigma.reindex e.symm g).inv) (Sigma.desc fun i ↦ α _)
· refine Sigma.hom_ext _ _ fun i ↦ ?_
obtain ⟨i, rfl⟩ := e.symm.surjective i
simp
· apply isOpenImmersion_sigmaDesc_aux
intro i j hij
exact hα (fun h ↦ hij (e.symm.injective h))
