Underlying points of equalizers of schemes over a base #
Let a b : Y ⟶ W be morphisms of schemes over a base S, and let y : Z ⟶ Y be another
morphism over S. The equalizer of y ≫ a and y ≫ b is the inverse image along y of the
equalizer of a and b. This file records the consequence for underlying points: a point of Z
lies in the image of the equalizer of y ≫ a and y ≫ b exactly when its image under y lies in
the image of the equalizer of a and b. It is the tool for describing the points with values
in a scheme Z that avoid a locus cut out by equalizers, such as the locus where a point of a
group scheme meets the identity section.
For two sections Q and R of a scheme X over S, the image of their equalizer is the set of
points of S at which Q and R take the same value: a section induces an isomorphism on
residue fields, so two sections that agree at a point agree on its residue field. Over a field
K, the base Spec K has a single point, so two K-points have empty equalizer exactly when
they differ.
Main results #
TauCeti.AlgebraicGeometry.range_equalizer_ι_left_comp: the image of the equalizer ofy ≫ aandy ≫ bis the preimage underyof the image of the equalizer ofaandb.TauCeti.AlgebraicGeometry.isEmpty_equalizer_comp_iff: the equalizer ofy ≫ aandy ≫ bis empty exactly when the image ofymisses the equalizer ofaandb.TauCeti.AlgebraicGeometry.isEmpty_equalizer_iff_of_isPullback: viewing points of a base change as points of the original scheme preserves and reflects emptiness of their equalizer.TauCeti.AlgebraicGeometry.range_equalizer_ι_left_of_left_eq_hom_comp: the image of the equalizer of a point and the point given by a section is the set where they agree.TauCeti.AlgebraicGeometry.range_equalizer_ι_left_of_section: the image of the equalizer of two sections is the set of points of the base at which they agree.TauCeti.AlgebraicGeometry.isEmpty_equalizer_iff_forall_ne: two sections have empty equalizer exactly when they agree at no point of the base.TauCeti.AlgebraicGeometry.isEmpty_equalizer_iff_ne: over a field, two points of a scheme have empty equalizer exactly when they are distinct.
The equalizer of a and b is empty exactly when that of a' and b' is, for a = a' and
b = b'. The instance argument of equalizer depends on the two morphisms, so rw cannot
replace them in place inside IsEmpty (equalizer a b).left; this lemma does.
Points of the equalizer of two composites. For morphisms a b : Y ⟶ W and y : Z ⟶ Y of
schemes over S, a point of Z lies in the image of the equalizer of y ≫ a and y ≫ b exactly
when its image under y lies in the image of the equalizer of a and b.
Emptiness of the equalizer of two composites. For morphisms a b : Y ⟶ W and
y : Z ⟶ Y of schemes over S, the equalizer of y ≫ a and y ≫ b is empty exactly when no
point of Z is mapped by y into the equalizer of a and b.
Changing the base of a pullback does not change whether the equalizer of two points
is empty. Here a and b are the images of x and y under the pullback projection,
and e identifies their base map f' with Z.hom ≫ f.
Where a point meets a section. Let x and y be points of a scheme X over S with
values in Z, where y is the point Z ⟶ S ⟶ X given by a section R of X. The image of the
equalizer of x and y is the set of points of Z at which x takes the value of R: a section
induces an isomorphism on residue fields, so x and R agreeing at a point agree on its residue
field.
Where two sections agree. For sections Q and R of a scheme X over S, the image of
their equalizer is the set of points of S at which Q and R take the same value.
Two sections Q and R of a scheme X over S have empty equalizer exactly when they agree
at no point of S.
Equalizers of points over a field. Over a field K, two K-points of a scheme over
Spec K have empty equalizer exactly when they are distinct: Spec K has a single point, and
two sections agreeing there are equal.