English
A component of kerAdjunction isomorphisms provides the expected equality in the right adjoint setting.
Русский
Компоненты изоморфизмов кер-адъюнкции дают ожидаемое равенство в правомAdjunction окружении.
LaTeX
$$$\\forall Y, I, ...$ (proof-lemma about kerAdjunction)$$
Lean4
/-- `S` is the disjoint union of `Xᵢ` if the `Xᵢ` are covering, pairwise disjoint open subschemes
of `S`. -/
theorem nonempty_isColimit_cofanMk_of [Small.{u} σ] {X : σ → Scheme.{u}} {S : Scheme.{u}} (f : ∀ i, X i ⟶ S)
[∀ i, IsOpenImmersion (f i)] (hcov : ⨆ i, (f i).opensRange = ⊤)
(hdisj : Pairwise (Disjoint on (f · |>.opensRange))) : Nonempty (IsColimit <| Cofan.mk S f) :=
by
have : IsOpenImmersion (Sigma.desc f) :=
by
refine isOpenImmersion_sigmaDesc _ _ (fun i j hij ↦ ?_)
simpa [Function.onFun_apply, disjoint_iff, Opens.ext_iff] using hdisj hij
simp only [← Cofan.isColimit_iff_isIso_sigmaDesc (Cofan.mk S f), cofan_mk_inj, Cofan.mk_pt]
apply isIso_of_isOpenImmersion_of_opensRange_eq_top
rw [eq_top_iff]
intro x hx
have : x ∈ ⨆ i, (f i).opensRange := by rwa [hcov]
obtain ⟨i, y, rfl⟩ := by simpa only [Opens.iSup_mk, Opens.mem_mk, Set.mem_iUnion] using this
use Sigma.ι X i |>.base y
simp [← Scheme.comp_base_apply]
