isEmpty_pullback_iff — Mathlib

English

The fiber product X ×_S Y is empty if and only if the images of X and Y in S are disjoint, i.e., the base loci do not meet inside S.

Русский

Распакованное произведение X ×_S Y пусто тогда и только тогда, когда образы X и Y в S не пересекаются, т.е. базовые локации не совпадают внутри S.

LaTeX

$$$IsEmpty \\; \\uparrow(Limits.pullback f g) \\; \\Leftrightarrow \\, Disjoint (Set.range f.base) (Set.range g.base)$$$

Lean4

theorem _root_.AlgebraicGeometry.Scheme.isEmpty_pullback_iff {f : X ⟶ S} {g : Y ⟶ S} :
    IsEmpty ↑(Limits.pullback f g) ↔ Disjoint (Set.range f.base) (Set.range g.base) :=
  by
  refine ⟨?_, Scheme.isEmpty_pullback f g⟩
  rw [Set.disjoint_iff_forall_ne]
  contrapose!
  rintro ⟨_, ⟨x, rfl⟩, _, ⟨y, rfl⟩, e⟩
  obtain ⟨z, -⟩ := exists_preimage_pullback x y e
  exact ⟨z⟩

Похожие утверждения