English
A certain range of a map lies inside the diagonal pullback range; specifically, the range of A.g.base is contained in the diagonal range of the pullback diagram.
Русский
Область значения карты лежит внутри диагонального диапазона в диаграмме тяготы.
LaTeX
$$$\operatorname{range}(A.g.base) \subseteq \mathrm{Scheme}.Pullback.diagonalCoverDiagonalRange(f\,A.\mathcal{U}_S\,A.\mathcal{U}_X)$$$
Lean4
theorem exists_index :
∃ (i' : I) (hii' : i' ⟶ A.i),
((D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)).base ⁻¹'
((Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X : Set <| ↑(pullback f f))ᶜ)) =
∅ :=
by
let W := Scheme.Pullback.diagonalCoverDiagonalRange f A.𝒰S A.𝒰X
by_contra! h
let Z (i' : I) (hii' : i' ⟶ A.i) := (D.map hii' ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb)).base ⁻¹' Wᶜ
have hZ (i') (hii' : i' ⟶ A.i) : IsClosed (Z i' hii') := (W.isOpen.isClosed_compl).preimage <| Scheme.Hom.continuous _
obtain ⟨s, hs⟩ :=
exists_mem_of_isClosed_of_nonempty' D A.c A.hc Z hZ h (fun _ _ ↦ (hZ _ _).isCompact)
(fun i i' hii' hij ↦ by simp [Z, Set.MapsTo])
refine hs A.i (𝟙 A.i) (Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange _ _ _ ?_)
use (A.c.π.app A.i ≫ A.a).base s
have H : A.c.π.app A.i ≫ A.a ≫ pullback.diagonal f = A.c.π.app A.i ≫ pullback.lift A.a A.b (A.ha.symm.trans A.hb) :=
by ext <;> simp [hab]
simp [← Scheme.comp_base_apply, -Scheme.comp_coeBase, H]
