IntegralSectionChart.lean

The actual integral section in the infinity chart

When the first primitive coordinate is a unit in a reduced coefficient ring, its inverse times the second coordinate gives a concrete affine coordinate. Evaluation at this value, followed by the infinity chart of the integral projective line, has image contained in the original integral section. The reduced-source factorization theorem for closed immersions and the terminal property of Spec ℤ identify these actual scheme morphisms.

This supplies the coordinate description of the original section needed for the local ideal calculation in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The corresponding stalk-ideal and intersection-length comparisons remain separate statements.