Quotients by an arbitrary subset of a regular system of parameters #
[Kol07, Definition 24 (4)] cuts Z out by an unordered subset z_{j_1}, …, z_{j_s} of the local
coordinates; the quotient lemmas of Hironaka.Algebra.Local.RegularSystem are stated for the
initial segments x_0, …, x_{i-1}. This module moves a Finset s of coordinates to the front
through the enumeration of Fin n by s and then sᶜ (finsetEquiv) and transports those lemmas:
R ⧸ (z_l : l ∈ s)is a regular local ring of dimensionn − |s|(isRegularLocalRing_quotient_span_image_finset,ringKrullDim_quotient_span_image_finset);- a coordinate
z_j,j ∉ s, lies neither in(z_l : l ∈ s)nor in𝔪² + (z_l : l ∈ s): the classes of the coordinates form a basis of𝔪/𝔪², soz_jcannot be a combination of the others modulo𝔪²(notMem_sq_sup_span_image,mem_span_image_iff).
Hironaka.Scheme.Snc.HasSncWith sees the quotient through the surjection 𝒪_{X,x} → 𝒪_{Z,w} with
kernel I_{Z,x} = (z_l : l ∈ s), so the last section restates everything for a surjective ring
homomorphism φ : R →+* S with kernel (z_l : l ∈ s): S is regular of dimension n − |s|, the
images of the z_l, l ∉ s, generate 𝔪_S, and for j ∉ s the image φ z_j lies in 𝔪_S ∖ 𝔪_S²
with S ⧸ (φ z_j) regular — the local form of Kollár's remark after Definition 24 that E|_Z is
again a simple normal crossing divisor on Z, whose members E^i ∩ Z are smooth divisors of Z.
Enumerating Fin n with a Finset first #
The enumeration of Fin n by the members of s (in order) and then those of sᶜ.
Equations
- AlgebraicGeometry.finsetPerm s i = Sum.elim (⇑(s.orderEmbOfFin ⋯)) (⇑(sᶜ.orderEmbOfFin ⋯)) (finSumFinEquiv.symm i)
Instances For
The enumeration as an equivalence.
Equations
Instances For
The tail of the enumeration is the complement sᶜ.
Quotients by a subset of the coordinates #
The quotient of a regular local ring by part of a regular system of parameters — an unordered subset of the coordinates — is regular.
dim R ⧸ (z_l : l ∈ s) + |s| = dim R.
dim R ⧸ (z_l : l ∈ s) = n − |s|, as a natural number.
A coordinate outside s is independent of the coordinates in s #
A coordinate z_j, j ∉ s, is not a combination of the z_l, l ∈ s, modulo 𝔪² — the
classes of the coordinates are a basis of 𝔪/𝔪².
z_j ∈ (z_l : l ∈ s) iff j ∈ s.
(z_j) ⊆ (z_l : l ∈ s) iff j ∈ s.
Through a surjection with kernel (z_l : l ∈ s) #
The images of the coordinates outside s span the image of (z_0, …, z_{n-1}).
The kernel of R → S → S ⧸ (φ z_j) is (z_l : l ∈ insert j s).
The target of a surjection with kernel (z_l : l ∈ s) is regular.
dim S = n − |s|.
S ⧸ (φ z_j) is regular — it is R ⧸ (z_l : l ∈ insert j s).
The image of z_j, j ∉ s, lies outside 𝔪_S².
The images of the coordinates outside s generate 𝔪_S.