This file fixes the lightweight local-algebra data used by the one-point inertia theorem. The chart is a proposition, not a typeclass or a structure, so merely carrying it does not enlarge instance search.
The boundary components are explicitly labelled by the first r members of a finite regular system of parameters. Their primality records that the labelled local branches are irreducible. The boundary equation is associated to their product, as in the usual definition of a strict normal-crossings divisor.
The indices of the first r members of a d-element parameter family.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups
open scoped BigOperators
universe udef boundaryIndices (d r : ℕ) : Finset (Fin d)The product of the parameter functions labelling the boundary branches.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups
open scoped BigOperators
universe udef boundaryProduct {R : Type u} [CommMonoid R] {d : ℕ}
(t : Fin d → R) (r : ℕ) : RA finite family is a regular system of parameters when it is a regular sequence and generates the maximal ideal.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups
open scoped BigOperators
universe uabbrev IsRegularSystemOfParameters
{R : Type u} [CommRing R] [IsLocalRing R] {d : ℕ}
(t : Fin d → R) : PropAn explicit split strict-normal-crossings equation in a local ring.
t is the full regular system of parameters, the first r parameters label the irreducible local boundary branches, and f is a local equation of their reduced union. Primality is included as primitive branch data; it is supplied geometrically by the irreducible regular components in a strict chart rather than by a later ramification conclusion. Regularity of each branch quotient is imposed scheme-theoretically, at every specialization of the local chart; this is the algebraic content of saying that the boundary components, rather than only their closed-point local rings, are regular.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace EtaleFundamentalGroups
open scoped BigOperators
universe udef IsSplitStrictNormalCrossingsAt
{R : Type u} [CommRing R] [IsLocalRing R] {d : ℕ}
(f : R) (t : Fin d → R) (r : ℕ) : Prop