Definitions/Def_AlgebraicGeometry_SchemeFibreEndo.lean

Let f \colon X \to S be a morphism of schemes (in a fixed universe) and let h \colon X \to X satisfy h followed by f equals f, i.e. f \circ h = f, so that h is an endomorphism of X over S. For a point s of S, the fibre of f at s is taken in the form of the pullback of f along the canonical morphism \operatorname{Spec}\kappa(s) \to S from the residue field at s (Mathlib's Scheme.fromSpecResidueField), so X_s = X \times_S \operatorname{Spec}\kappa(s) as a chosen pullback object. The definition schemeFibreEndo produces an endomorphism of this object: it is the morphism into the pullback determined by the pair consisting of the first projection followed by h, and the second projection, the required compatibility being the identity f \circ h = f combined with the defining square of the pullback. Thus schemeFibreEndo f h hcomm s is the map h_s \colon X_s \to X_s induced by h on the fibre over s, recorded as a concrete morphism between the chosen pullback objects rather than as a morphism of an abstractly characterised fibre.

The two accompanying lemmas record its two defining properties, each as a simp lemma: composing h_s with the first projection X_s \to X gives the first projection followed by h, and composing h_s with the second projection X_s \to \operatorname{Spec}\kappa(s) gives the second projection unchanged (so h_s is a morphism over \operatorname{Spec}\kappa(s)). Together they characterise h_s uniquely by the universal property of the pullback.