The rigidity lemma #
Let X, Y, Z be schemes over a field K, with X proper and geometrically integral, Y
geometrically integral and locally of finite type, and Z separated and locally of finite type.
The rigidity lemma says that a morphism f : X ×_K Y ⟶ Z which collapses one fibre
X × {y₀} over a K-rational point y₀ of Y to a single K-rational point of Z factors
through the projection to Y: for any K-rational point x₀ of X,
f (x, y) = f (x₀, y).
Over an algebraically closed field the proof runs as follows. The morphism
γ = (pr₂, f) : X × Y ⟶ Y × Z is proper over Y, and its fibre over y₀ has a single point
in its image. By Zariski's main theorem, γ has finite image on each fibre X × {y} for y in
an open neighbourhood U of y₀. For a closed point y ∈ U, the fibre X × {y} is
irreducible, so its finite image under γ is a single point; hence f (x, y) = f (x₀, y) on the
closed points of the dense open subset
pr₂⁻¹ U, and so everywhere, since X × Y is reduced and Z is separated. The general case
follows by base change to an algebraic closure, which is faithful on schemes over Spec K.
This is the argument of Mathlib's
AlgebraicGeometry.isCommMonObj_of_isProper_of_isIntegral_tensorObj_of_isAlgClosed (Andrew Yang
and Christian Merten), which proves commutativity of proper group schemes by running it for the
commutator map; here it is carried out for an arbitrary morphism f. The descent to an arbitrary
field follows AlgebraicGeometry.isCommMonObj_of_isProper_of_geometricallyIntegral in the same
Mathlib file (Andrew Yang and Christian Merten).
Main declarations #
TauCeti.AlgebraicGeometry.preimage_snd_left_eq_range_whiskerLeft_left: the fibre ofX × Y ⟶ Yover aK-rational pointyis the image ofX × Y ⟶ X × Y,(x, y') ↦ (x, y);TauCeti.AlgebraicGeometry.exists_forall_finite_image_preimage_of_finite_image_preimage: if a morphism proper over a base has finite image on one fibre, it does so on the fibres over a neighbourhood;TauCeti.AlgebraicGeometry.eq_snd_comp_lift_comp_of_isAlgClosed: the rigidity lemma over an algebraically closed field;TauCeti.AlgebraicGeometry.eq_snd_comp_lift_comp: the rigidity lemma over an arbitrary field.
References #
- D. Mumford, Abelian Varieties, Section 4, the rigidity lemma.
- J. S. Milne, Abelian Varieties, Theorem 1.1.
The fibre of the second projection X × Y ⟶ Y over a K-rational point y of Y is the
range of the map X × Y ⟶ X × Y, (x, y') ↦ (x, y).
Let f : X ⟶ Y and g : Y ⟶ S with f ≫ g proper and g separated and locally of finite
type. If f has finite image on the fibre of f ≫ g over s, then the same holds over every
point of a neighbourhood of s. This is a consequence of Zariski's main theorem.
The rigidity lemma over an algebraically closed field K. Let X be proper over K, Y
locally of finite type over K with X × Y integral, and Z separated and locally of finite
type over K. If f : X × Y ⟶ Z sends the fibre X × {y₀} over a K-point y₀ of Y to a
single K-point z₀ of Z, then f (x, y) = f (x₀, y) for any K-point x₀ of X.
The rigidity lemma. Let X be proper and geometrically integral over a field K, Y
geometrically integral and locally of finite type over K, and Z separated and locally of
finite type over K. If f : X × Y ⟶ Z sends the fibre X × {y₀} over a K-point y₀ of Y
to a single K-point z₀ of Z, then f factors through the projection to Y:
f (x, y) = f (x₀, y) for any K-point x₀ of X.