ModuleFiniteSectionNormalCrossings.lean
Nyll.ShimizuYamaguchi26BranchedCoverings.Geometry.FiniteSectionNormalCrossings
5 declarations indexed from sourceView source ↗ Module documentation
Normal crossings in a finite family of rational sections
At the point of the section b over p, the actual kernel ideal of a section c becomes the unit ideal when p does not divide Delta(c,b). This follows from the previously computed actual intersection length. Thus every other factor in a finite product of section ideals disappears from the stalk. A single remaining branch is a regular parameter; two remaining branches whose determinant has valuation one form the previously constructed regular parameter system. In either case the entire finite product has strict normal crossings at this point. The determinant filter selects these cases directly when its cardinality is at most two. The actual support of the product and the section identity then give the same result at every support point lying over p. The existing closed reduction points and intersection comparison also derive these arithmetic hypotheses from closed-point incidence and valuation conditions on the actual special fibre.
These are the local one- and two-branch implications needed in Lemma 2.3 of Ryoji Shimizu and Naganori Yamaguchi, On branched coverings of the projective line over the integers. The full finite-family criterion still needs the converse and comparison with base change to Z_p. Identifying this product with the reduced effective Cartier divisor of the paper is also a separate construction.
Declarations
ShimizuYamaguchi26BranchedCoverings.rationalSectionFamily_isStrictNormalCrossingsAt_of_one_branch
DocumentationA finite product of actual section ideals has strict normal crossings at the point of b over p when every other section is disjoint there.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings
ShimizuYamaguchi26BranchedCoverings.rationalSectionFamily_isStrictNormalCrossingsAt_of_two_branches
DocumentationA finite product of actual section ideals has strict normal crossings at the point of b over p when exactly the selected two branches can meet there and their determinant has valuation one.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings
ShimizuYamaguchi26BranchedCoverings.rationalSectionFamily_isStrictNormalCrossingsAt_of_card_le_two
DocumentationThe determinant incidence count and valuation-one condition imply strict normal crossings at the actual point of a selected section. The selected section itself belongs to the count because its self-determinant is zero.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings
ShimizuYamaguchi26BranchedCoverings.rationalSectionFamily_isStrictNormalCrossingsAt_over_prime
DocumentationThe arithmetic incidence-count conditions give strict normal crossings at every support point over the selected prime. The supporting section is obtained from the actual ideal-sheaf product, and its base point is recovered from the section identity.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings
ShimizuYamaguchi26BranchedCoverings.rationalSectionFamily_isStrictNormalCrossingsAt_of_specialFiber_conditions
DocumentationClosed-point incidence and intersection-valuation conditions on the actual prime special fibre imply strict normal crossings on the integral surface above that prime. The cardinality counts the original rational sections through the point, retaining their labels when reductions collide.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
open AlgebraicGeometry CategoryTheory
open scoped BigOperators
namespace ShimizuYamaguchi26BranchedCoverings