Substitution automorphisms of K⟦X₁, …, Xₙ⟧ #
Kollár fixes R = K⟦x₁, …, xₙ⟧ with maximal ideal 𝔪 and describes its automorphisms
xᵢ ↦ gᵢ [Kol07, Notation 93]: they are automorphisms iff the linear parts of the gᵢ are
linearly independent, and the automorphisms of the form 1 + B (B ≤ 𝔪 an ideal) are
those with gᵢ = xᵢ + λᵢ bᵢ, bᵢ ∈ B. Proposition 94 characterizes the ideals invariant
under them (Hironaka/Algebra/Local/Prop94.lean); through the Cohen structure theorem the
characterization applies to the completed local rings of a smooth variety, where it is used in
the study of hypersurfaces of maximal contact (Hironaka/Resolution/Algebraic/MaximalContact/).
This file sets up the vocabulary on Mathlib's MvPowerSeries.substAlgHom:
linearSubst A, the familyXᵢ ↦ ∑ⱼ Aᵢⱼ Xⱼ;linearPart a, the matrix(coeff (single j 1) (a i))ᵢⱼof linear parts;shiftSubst i c, the familyXᵢ ↦ Xᵢ + c,Xⱼ ↦ Xⱼforj ≠ i;IsOnePlus B gandIsInvariantOnePlus I B.
The theorems (continuous endomorphisms are substitutions; unipotent and linear substitutions
are automorphisms; the criterion of Notation 93; the shift automorphisms of the form 1 + B)
follow in this file. The workhorse is the description of the powers of the maximal
ideal, f ∈ 𝔪^k ↔ k ≤ order f (MvPowerSeries.mem_span_range_X_pow_iff_le_order, in
Hironaka/Algebra/Local/PowerSeries.lean).
The linear family Xᵢ ↦ ∑ⱼ Aᵢⱼ Xⱼ attached to a matrix A.
Equations
- IsLocalRing.linearSubst A i = ∑ j : Fin n, A i j • MvPowerSeries.X j
Instances For
The matrix of linear parts (coeff (single j 1) (a i))ᵢⱼ of a family a ("the linear parts
of the gᵢ" of [Kol07, Notation 93]).
Equations
- IsLocalRing.linearPart a = Matrix.of fun (i j : Fin n) => (MvPowerSeries.coeff (Finsupp.single j 1)) (a i)
Instances For
The family Xᵢ ↦ Xᵢ + c, Xⱼ ↦ Xⱼ for j ≠ i (Kollár's "xᵢ ↦ xᵢ + λᵢ bᵢ",
[Kol07, Notation 93]).
Equations
Instances For
An automorphism g of K⟦X⟧ is of the form 1 + B [Kol07, Notation 93] if it is a
substitution automorphism and g (Xᵢ) - Xᵢ ∈ B for every i. Kollár writes these as
xᵢ ↦ xᵢ + λᵢ bᵢ (bᵢ ∈ B); the two descriptions agree (λᵢ = 1, bᵢ = g (Xᵢ) - Xᵢ).
Equations
- One or more equations did not get rendered due to their size.
Instances For
I is invariant under the automorphisms of the form 1 + B (clause (1) of
[Kol07, Proposition 94]) if I.map g ≤ I for every such g. The primitive is ≤, not =
(the set of such g is not obviously closed under inverses; Proposition 94 proves and uses
only ≤).
Equations
- IsLocalRing.IsInvariantOnePlus I B = ∀ (g : MvPowerSeries (Fin n) K ≃ₐ[K] MvPowerSeries (Fin n) K), IsLocalRing.IsOnePlus B g → Ideal.map (↑g) I ≤ I
Instances For
Over a field, a substitutable family has zero constant coefficients.
A substitution maps the maximal ideal into itself.
A substitution maps every power of the maximal ideal into itself.
A substitution maps the maximal ideal into itself, elementwise.
The defect φ(fg) - fg of a substitution φ on a product.
Unipotent substitutions are automorphisms #
Let φ = substAlgHom ha with a i ≡ Xᵢ (mod 𝔪²). The defect φ f - f raises the 𝔪-adic
order: f ∈ 𝔪^k implies φ f - f ∈ 𝔪^(k+1). This is proved by induction on k from the two
base facts φ r - r ∈ 𝔪 (every r) and φ x - x ∈ 𝔪² (x ∈ 𝔪), both by induction over the
generators Xᵢ of 𝔪 using the product formula substAlgHom_mul_sub. Injectivity then
follows because a series killed by φ lies in every 𝔪^k, and K⟦X⟧ is 𝔪-adically
Hausdorff; surjectivity by successive approximation u₀ = 0, uₖ₊₁ = uₖ + (f - φ uₖ), whose
residuals f - φ uₖ lie in 𝔪^k, so that the sequence converges by 𝔪-adic completeness to a
preimage of f.
If the a i are congruent to Xᵢ modulo 𝔪, the substitution changes every series by an
element of 𝔪.
If the a i are congruent to Xᵢ modulo 𝔪², the substitution changes every element of
𝔪 by an element of 𝔪².
The defect of a unipotent substitution raises the 𝔪-adic order by one.
A substitution Xᵢ ↦ a i with a i ≡ Xᵢ (mod 𝔪²) is an automorphism of K⟦X⟧ (one half
of the criterion of [Kol07, Notation 93]).
Linear substitutions #
linearSubst A is the family Xᵢ ↦ ∑ⱼ Aᵢⱼ Xⱼ. Substituting linearSubst B into linearSubst A
gives linearSubst (A * B), so the substitutions by A and A⁻¹ are mutually inverse when A
is invertible (subst_self for linearSubst 1 = X).
The substitution by A⁻¹ undoes the substitution by A.
Continuous endomorphisms are substitutions #
With the coefficientwise topology (K discrete), Mathlib's continuous_subst says a
substitution is continuous, and aeval_unique says a continuous K-algebra endomorphism is the
evaluation at the images of the variables; under the discrete topology "evaluable" and
"substitutable" agree (hasSubst_iff_hasEval_of_discreteTopology).
A K-algebra endomorphism of K⟦X⟧ is continuous iff it is a substitution xᵢ ↦ gᵢ (the
maps of [Kol07, Notation 93]).
The criterion of Notation 93 #
A family a with constantCoeff (a i) = 0 splits as a = φ_b ∘ linearSubst A where
A = linearPart a is the matrix of linear parts and b = A⁻¹ a is unipotent (b j ≡ Xⱼ mod 𝔪²),
so Xᵢ ↦ a i is an automorphism when A is invertible (the two preceding sections).
Conversely, if A is singular, a nonzero linear form ℓ = ∑ vᵢ Xᵢ with v ᵥ* A = 0 is sent
into 𝔪²; an automorphism preserves 𝔪 and hence 𝔪², so ℓ ∈ 𝔪², which is absurd.
Monomials of degree less than two: the constant one and the variables.
A substitutable family differs from its linear part by elements of 𝔪².
The "⇐" of the criterion of [Kol07, Notation 93]: if the linear parts are linearly independent, the substitution is an automorphism.
The "⇒" of the criterion of [Kol07, Notation 93]: an automorphism Xᵢ ↦ a i has linearly
independent linear parts.
The criterion of [Kol07, Notation 93]: Xᵢ ↦ a i is an automorphism iff the matrix of
linear parts is invertible.
The shift automorphisms of the form 1 + B #
The family Xᵢ ↦ Xᵢ + c (other variables fixed) has linear-part matrix 1 + eᵢ βᵀ, β the
vector of linear coefficients of c, whose determinant is 1 + βᵢ (matrix determinant lemma).
With c = q • b, q ∈ ℚ, the determinant 1 + q βᵢ vanishes for at most one q.
For b ∈ B ≤ 𝔪 and all q ∈ ℚ except at most one, Xᵢ ↦ Xᵢ + q b, Xⱼ ↦ Xⱼ (j ≠ i) is
an automorphism of the form 1 + B: Kollár's "xᵢ ↦ xᵢ + λᵢ bᵢ gives an automorphism for
general λᵢ" [Kol07, Notation 93], as used in the proof of [Kol07, Proposition 94].